What was already known
Burkholder and Bourgain established the equivalence with quadratic bounds; whether either direction admitted a uniform linear comparison remained open.
AI involvement
The authors credit Astra with finding both example families. Lorist and van Neerven framed the problem, wrote and explained the constructions, and report reviewing every proof.
Astra found the central example families; humans framed the longstanding problem, wrote and reviewed the final argument.
Importance
The examples resolve both directions of this longstanding quantitative problem.
Limitations
The reported Lean proof covers Theorem 1.1 at p=2, not the paper’s broader Corollary 1.3.
Technical verification
The authors report full manual review and a Lean 4 proof of Theorem 1.1 at p=2. The repository reports comparator/axiom checks and independent kernel replay; no local rerun was made.
Formal checking
Author review of all final statements and proofs
- Checker
- Lorist and van Neerven
- Scope
- Theorem 1.1 sharpness examples and final proofs
- Basis
- Reported by the linked checker
Formal checking
Formal proof, comparator alignment and axiom audit
- Checker
- Lean 4, NanoDa and con-ron, as reported by the authors
- Scope
- Theorem 1.1: all eight inequalities for X_n and Y_n over real and complex scalars
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The human authors explain the dyadic block norms, matrices and why the two families force both quadratic dependencies.
Correction and publication history
The examples resolve both directions of this longstanding quantitative problem.
Read this published revision