What was already known
A general quartic upper bound was known, but no superquadratic separation for block sensitivity versus spectral sensitivity had been established.
AI involvement
GPT-5.6 Sol proposed the central gated-tournament construction. Alexander Meiburg explained the mechanism and reduced and optimized the finite witness.
The disclosed model-origin gated-tournament idea survives as the core of the separation; the compact witness and exposition are Meiburg’s work.
Importance
The construction answers a named query-complexity question negatively.
Limitations
The Lean theorem checks the stated finite separation; the optimal exponent remains open.
Technical verification
The paper reports Lean verification of Theorem 6.1, the stated finite separation.
Independent checking
Formal proof and minimal Comparator certificate reported in §7 and Appendix B
- Checker
- Lean 4, through the paper’s Aristotle-assisted formalization
- Scope
- Theorem 6.1: a total function with block sensitivity at least 14,011 and spectral sensitivity at most 89.0162
- Basis
- Reported by the linked checker
Human understanding
Meiburg explains why gated tournament subcubes force high block sensitivity while controlling the sensitivity-graph eigenvalue and records his parameter optimization.
Correction and publication history
The construction answers a named query-complexity question negatively.
Read this published revision