Section 10, paragraph 3The verification boundary: external classical inputs, conditional results, empirical runs
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
The boundary of this verification is explicit. Classical complexity results, notably Håstad’s parity hardness and correlation bounds and the Linial–Mansour–Nisan/Tal spectral bounds, remain external inputs (Håstad, 1986, 2014; Linial et al., 1993; Tal, 2015). The single-channel result is checked conditional on a stated negligible parity-correlation theorem, including its application to the readout and its probability calculation. The spectral discussion uses a separate Fourier-tail premise; its connection to the exact conventions of a published tail theorem is not part of the checked development. The conditional implication from a tail bound to small parity correlation is checked. Empirical measurements and training runs are supported by experimental code and saved results, rather than by Lean proofs.
Generated from paper_jmlr.tex, lines 1291–1291.
2 Explain this
The boundary of the verification, in the paper's words:
- External inputs: Håstad's parity hardness and correlation bounds, and the Linial–Mansour–Nisan and Tal spectral bounds, are not proved in Lean.
- Conditional results: the single-channel result is checked conditional on a stated negligible parity-correlation theorem, including its application to the readout and the probability calculation.
- Spectral discussion: the implication from a Fourier-tail bound to small parity correlation is checked; the connection of the tail premise to a published theorem is not.
- Empirical results rest on experimental code and saved results, not Lean proofs.
3 How this is formalised
This paragraph is itself a description of coverage. The corresponding records: the named classical input HastadNegl
(Remark 2.3 (global parity)); the conditional single-channel result (Theorem 5.12 (i));
the tail implication (Equation (6.1)) and the open tail-premise connection
(Section 10, paragraph 3 (open item)); the empirical records of Section 7.
| Paper anchor | sec:development-p3 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 10, paragraph 3 |
| Claim | The verification boundary: external classical inputs, conditional results, empirical runs |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1291–1291; SHA-256 of the normalised block source 8027624b08756a3b… |
| Depends on | Theorem 5.12 (i), Section 10, paragraph 3 (open item) |
| Explanations | explain/c-verification-boundary, formal/c-verification-boundary |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).