Everything here compiles with Lean 4.15.0 and contains no sorry.
./build.sh downloads the toolchain and verifies it in seconds.
No Mathlib. The olean cache CDNs return 403 through this environment's proxy and a source build is hours, so the algebra is developed from scratch. That turned out to be an advantage: S3, S4 and S6 are identities over an arbitrary star-semiring, so proving them here proves them in more generality than a Mathlib proof over ℂ.
| step | statement | status |
|---|---|---|
| S1 | cyclic shifts are mutually orthogonal and sharply transitive | proved |
| S2 | X i j = if j = 0 then S i else 0 |
definition |
| S3 | Xᴴ X is supported on one block, equal to ∑ Sᴴ_i S_i |
proved |
| S4 | (X Xᴴ)_ij = S_i Sᴴ_j |
proved |
| S5 | ‖∑ A i‖ = ‖Xᴴ X‖ = ‖X Xᴴ‖ |
hypothesis hS5 |
| S6 | ∑ k, D k = X Xᴴ |
proved |
| S7 | ‖D k‖ = max_i ‖S_i Sᴴ_{π k i}‖ |
hypothesis hS7 |
| — | assembly: subadditivity over the sum, then the bound | proved |
kittaneh_modulo_S5_S7 is the lemma itself, with only S5 and S7 as hypotheses.
Kittaneh.exists_unique_shift does not depend on any axioms
Kittaneh.blockPartition propext
OpAlg.nrm_bsumf_le Quot.sound
OpAlg.S3, S4, S6, kittaneh_... propext, Quot.sound
propext and Quot.sound are two of Lean's three standard axioms. sorryAx
appears nowhere; CheckAll.lean verifies this and build.sh runs it.
S5 and S7 are the two genuinely analytic steps: they compute the operator norm
of a one-block matrix and of a block permutation matrix. Assembly.lean names
the obligation as a three-field structure NormFacts plus the two hypotheses
hS5, hS7. Porting to Mathlib is therefore: instantiate V := ℝ,
nrm := Matrix.l2_opNorm, and supply those. Nothing else in the lemma is open.
S6Core.lean permutation combinatorics; the partition underlying S6
Algebra.lean star-semiring, finite sums, the single-nonzero-term lemma
Blocks.lean block matrices; S3, S4, S6
Assembly.lean the norm interface and the bound modulo S5, S7
Kittaneh.lean the Mathlib-flavoured target file; `sorry`, NOT compiled
CheckAll.lean axiom audit
build.sh fetch toolchain, compile everything, run the audit