Sixth-edition extension: 21 precise formalization targets

Proved

BookSixth.sixthEditionExtension

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

This project goal is the conjunction of the 21 explicitly stated results in the sixth-edition extension: spectral diagonalization and its off-diagonal reduction; Hadamard bound, equality, order restriction and powers-of-two construction; a strict determinant lower bound and the mean-square determinant identity; pairwise unlinked round circles forming an unlink; polynomial zero and interpolation bounds and finite Kakeya; the permanent bound and Latin-square bounds and asymptotic; hypergraph two-colorability, the real-exponent Ramsey bound, high-girth/high-chromatic graphs and the good-drawing crossing lemma; and the two explicit Fox-coloring calculations. Every component retains the exact binders and boundary conditions of its linked child. This is a collection-completion goal, not a claim that every theorem or every proof in the book is covered. The full diagram-to-topology bridge remains an explicitly unlinked milestone outside this conjunction.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.sixthEditionExtension :
    (∀ {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian),
      ∃ Q : Matrix.unitaryGroup (Fin n) ℝ, ∃ d : Fin n → ℝ,
      star (Q : Matrix (Fin n) (Fin n) ℝ) * A * (Q : Matrix (Fin n) (Fin n) ℝ) = Matrix.diagonal d) ∧
    (∀ {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian) (h : 0 < offDiagonalMass A),
      ∃ Q : Matrix.unitaryGroup (Fin n) ℝ,
      offDiagonalMass (star (Q : Matrix (Fin n) (Fin n) ℝ) * A * (Q : Matrix (Fin n) (Fin n) ℝ)) < offDiagonalMass A) ∧
    (∀ {n : ℕ} (hn : 0 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A),
      |A.det| ≤ (n : ℝ) ^ ((n : ℝ) / 2)) ∧
    (∀ {n : ℕ} (hn : 0 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A),
      (|A.det| = (n : ℝ) ^ ((n : ℝ) / 2)) ↔
      ∀ i j, i ≠ j → (∑ k, A k i * A k j) = 0) ∧
    (∀ {n : ℕ} (hn : 2 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A) (horth : A.transpose * A = (n : ℝ) • (1 : Matrix (Fin n) (Fin n) ℝ)),
      4 ∣ n) ∧
    (∀ (m : ℕ),
      ∃ A : Matrix (Fin (2^m)) (Fin (2^m)) ℝ, SignMatrix A ∧
      A.transpose * A = ((2^m : ℕ) : ℝ) • (1 : Matrix (Fin (2^m)) (Fin (2^m)) ℝ)) ∧
    (∀ (n : ℕ) (hn : 2 ≤ n),
      ∃ A : Matrix (Fin n) (Fin n) ℝ, SignMatrix A ∧ Real.sqrt (n.factorial : ℝ) < A.det) ∧
    (∀ {m : ℕ} (C : Fin m → Set Space3) (hround : ∀ i, RoundCircle (C i)) (hdisjoint : ∀ i j, i ≠ j → Disjoint (C i) (C j)) (hpairs : ∀ i j, i ≠ j → IsUnlink (![C i, C j] : Fin 2 → Set Space3)),
      IsUnlink C) ∧
    (∀ {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (hn : 0 < n) (p : MvPolynomial (Fin n) F) (hp : p ≠ 0),
      (Finset.univ.filter (fun x : Fin n → F => MvPolynomial.eval x p = 0)).card ≤
      p.totalDegree * Fintype.card F ^ (n-1)) ∧
    (∀ {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} (E : Finset (Fin n → F)) (hE : E.card < Nat.choose (n+d) d),
      ∃ p : MvPolynomial (Fin n) F, p ≠ 0 ∧ p.totalDegree ≤ d ∧
      ∀ x ∈ E, MvPolynomial.eval x p = 0) ∧
    (∀ {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (hn : 0 < n) (K : Finset (Fin n → F)) (hK : Kakeya K),
      Nat.choose (Fintype.card F + n - 1) n ≤ K.card ∧
      Fintype.card F ^ n ≤ n.factorial * K.card) ∧
    (∀ {n : ℕ} (A : Matrix (Fin n) (Fin n) ℕ) (hA : ∀ i j, A i j ≤ 1) (hrows : ∀ i, 0 < ∑ j, A i j),
      (permanent A : ℝ) ≤ ∏ i, ((Nat.factorial (∑ j, A i j) : ℕ) : ℝ) ^
      (1 / ((∑ j, A i j : ℕ) : ℝ))) ∧
    (∀ (n : ℕ) (hn : 0 < n),
      ((n.factorial : ℝ) ^ (2*n) / (n : ℝ) ^ (n*n) ≤ latinCount n) ∧
      ((latinCount n : ℝ) ≤ ∏ k ∈ Finset.Icc 1 n,
        (k.factorial : ℝ) ^ ((n : ℝ) / (k : ℝ)))) ∧
    (Filter.Tendsto (fun n : ℕ => (latinCount n : ℝ) ^ (1 / (n : ℝ)^2) / (n : ℝ))
      Filter.atTop (nhds (Real.exp (-2)))) ∧
    (∀ {N d : ℕ} (hd : 2 ≤ d) (A : Finset (Finset (Fin N))) (hsize : ∀ S ∈ A, S.card = d) (hcard : A.card ≤ 2^(d-1)),
      ∃ c : Fin N → Bool, ∀ S ∈ A, ∃ u ∈ S, ∃ v ∈ S, c u ≠ c v) ∧
    (∀ (k N : ℕ) (hk : 2 ≤ k) (hN : (N : ℝ) < (2 : ℝ)^((k : ℝ)/2)),
      ∃ G : SimpleGraph (Fin N), NoMono k G) ∧
    (∀ (k : ℕ) (hk : 2 ≤ k),
      ∃ N : ℕ, ∃ G : SimpleGraph (Fin N), ¬ HasColoring G k ∧
      ∀ l : ℕ, l ≤ k → ¬ HasCycle G l) ∧
    (∀ {N M : ℕ} (hN : 0 < N) (hM : 4*N ≤ M) (D : PlaneDrawing N M),
      M^3 ≤ 64 * N^2 * D.crossings.card) ∧
    (∀ (n : ℕ),
      (∑ B : Fin n → Fin n → Bool, (Matrix.det (fun i j => if B i j then (1 : ℝ) else -1))^2) = (2 : ℝ)^(n*n) * (n.factorial : ℝ)) ∧
    (∀ (n : ℕ) (hn : 3 ≤ n) (hodd : Odd n) (a b c : ZMod n),
      BorromeanFox a b c ↔ a = b ∧ b = c) ∧
    (∀ (a : Fin 6 → ZMod 5),
      TaitFox a ↔ a 0 = a 2 ∧ a 2 = a 4 ∧ a 1 = a 3 ∧ a 3 = a 5) := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), selected results of Chapters 7, 15, 35, 37 and 45. This goal is their explicit conjunction, not an additional theorem attributed to the book. https://doi.org/10.1007/978-3-662-57265-8

View graph