Section 10, paragraph 3 (open item)The Fourier-tail premise is not connected to a precise LMN/Tal statement with reconciled conventions
Open or deferred item Explicitly left open, deferred or not yet connected.
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 spectral discussion uses a hypothesis of the form "every bounded-depth, bounded-size formula has small Fourier mass above degree ". Results of this kind are classical (Linial–Mansour–Nisan; Tal), but their exact statements use particular conventions for size, depth and normalisation. Matching the Lean premise to one specific published statement, with those conventions reconciled, has not been done.
The main results do not depend on this: the single-channel bound uses Håstad's correlation input instead.
3 How this is formalised
Status: open. Fourier.TailPremise is an explicit, unproved hypothesis of the auxiliary conditional
application Fourier.nimBit_corr_of_tail; the principal results do not depend on it. The checked
implication from band-limitation to small correlation is RealFourier.bandLimited_corr_real.
| Paper anchor | sec:development-p3 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 10, paragraph 3 (open item) |
| Claim | The Fourier-tail premise is not connected to a precise LMN/Tal statement with reconciled conventions |
| Coverage category | Open or deferred item |
| Statement source | paper_jmlr.tex lines 1291–1291; SHA-256 of the normalised block source 8027624b08756a3b… |
| Depends on | Equation (6.1) |
| Explanations | explain/c-tailpremise-open, formal/c-tailpremise-open |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This item is explicitly open or deferred.
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).