Skip to content
BranchesTags

Repository files navigation

Formalization of Landmark Mathematical Theorems in Lean 4 (Suite III)

This repository provides machine-checked formalizations, certified proofs, and foundational scaffolds of landmark theorems across spectral graph theory, expander graphs, additive combinatorics, arithmetic progressions, extremal combinatorics, differential topology, gauge theory, spectral geometry, mirror symmetry, mixed Hodge theory, and discrete metric geometry in the Lean 4 / Mathlib ecosystem.

Master Table of Formalized Modules and Theorems

# Theorem / Topic Primary Declaration(s) Mathematical Domain Reference(s) Status & Implementation Architecture
1 Expander Mixing Lemma & Spectral Expansion expander_mixing_lemma, expander_mixing_lemma_simplified, hoffman_independence_bound, chromatic_number_spectral_bound, decompPerp_normSq, decompPerp_orthogonal Spectral Graph Theory & Expander Graphs Alon & Chung (1988), Alon (1986) 100% Verified (0 axioms) (Orthogonal decomposition, variance formula $|\mathbf{1}_S^\perp|^2 = |S|(1 - |S|/n)$, and Hoffman independence bound verified)
2 Alon–Boppana Spectral Lower Bound & Ramanujan Expanders alon_boppana_bound, alon_boppana_nilli, secondEigenvalue, IsRamanujan, ramanujan_spectral_gap, sphericalShell_disjoint, adjacencyMatrix_mul_ones Spectral Graph Theory & Ramanujan Graphs Alon (1986), Boppana (1986), Nilli (1991), Lubotzky–Phillips–Sarnak (1988) Modular Package (Formalization/AlonBoppana/) (Adjacency symmetry, spherical shell disjointness, and all-ones eigenvector verified; Nilli radial test function scaffolded)
3 The Discrete Cheeger Lower Bound for Regular Graphs cheeger_lower_bound, cheeger_lower_bound_normalized, ramanujan_cheeger_lower_bound, vertex_expansion_spectral_bound, dirichletEnergy_eq_laplacianQuadraticForm Spectral Graph Theory & Expander Graphs Alon & Milman (1985), Dodziuk (1984), Sinclair & Jerrum (1989) 100% Verified (0 axioms) (Dirichlet energy identity, discrete Cheeger lower bounds $\frac{d - \lambda_2}{2} \le h(G)$, and Ramanujan expansion bounds verified)
4 Tanner's Vertex Expansion Bound for Regular Graphs tanner_vertex_expansion_bound, tanner_expansion_ratio_bound, tanner_small_set_expansion, tanner_ramanujan_expansion, tanner_ramanujan_expansion_factored, tanner_half_set_expansion, tanner_vertex_margin_bound Spectral Graph Theory & Expander Graphs Tanner (1984), Alon & Spencer (2016), Hoory, Linial, & Wigderson (2006) 100% Verified (0 axioms) (Neighborhood Cauchy–Schwarz, spectral operator norm bound $|A \mathbf{1}_S^\perp|^2 \le \lambda^2 |\mathbf{1}_S^\perp|^2$, and Ramanujan small-set bounds verified)
5 Freiman's Structure Theorem & Ruzsa Sumset Calculus freiman_theorem_Z, polynomial_freiman_ruzsa_F2, bogolyubov_lemma, ruzsa_triangle_cardinality, ruzsaDistance_triangle, plunnecke_ruzsa_inequality, plunnecke_tripling Additive Combinatorics & Sumset Geometry Freiman (1966), Ruzsa (1989, 1994, 1996), Petridis (2012), Gowers et al. (2023) Modular Package (Formalization/RuzsaFreiman/) (Sumset translations, doubling constants $\sigma(A)$, difference symmetry $|A-B|=|B-A|$, and Ruzsa triangle inequality verified; PFR & Freiman GAP scaffolded)
6 Roth's Theorem on 3-Term Arithmetic Progressions roths_theorem, roths_theorem_zmod, roth_three_ap_bound, large_fourier_coefficient_dichotomy, ap3Count_of_free, progression_card Additive Combinatorics & Harmonic Analysis Roth (1953), Bourgain (1999), Kelley & Meka (2023) Modular Package (Formalization/RothsTheorem/) (3-AP predicates, progression cardinality, and indicator counting verified; discrete Fourier characters, large Fourier coefficient dichotomy, and density increment scaffolded)
7 Szemerédi's Regularity Lemma & Partition Energy Dynamics szemeredi_regularity_lemma, triangle_counting_lemma, triangle_removal_lemma, energy_increment_lemma, pairDensity_symm, energy_le_one Extremal Graph Theory & Regularity Methods Szemerédi (1978), Ruzsa & Szemerédi (1978), Gowers (1997), Fox (2011) Modular Package (Formalization/SzemerediRegularity/) (Pair edge density $0 \le d(X, Y) \le 1$, symmetry $d(X, Y)=d(Y, X)$, partition energy non-negativity $0 \le E(\mathcal{P}) \le 1$, and exhaustion bound verified; $+\varepsilon^5/2$ energy increment scaffolded)
8 The Cauchy–Davenport Theorem and Iterated Sumsets cauchy_davenport, cauchy_davenport_integers, cauchy_davenport_iterated, cauchy_davenport_self_iterated, vosper_theorem, chowla_theorem, erdos_ginzburg_ziv_prime Additive Number Theory & Finite Fields Cauchy (1813), Davenport (1935), Vosper (1956), Chowla (1935), Erdős, Ginzburg, & Ziv (1961) 100% Verified Core & Extended Scaffold (Single sumset $\lvert A+B \rvert \ge \min(p, \lvert A \rvert + \lvert B \rvert - 1)$, iterated sumsets, and torsion-free group bounds verified; Vosper critical pairs & Chowla composite moduli scaffolded)
9 Gilmer's Entropy Bound on Frankl's Union-Closed Sets Conjecture gilmer_two_element_family, powerset_satisfies_gilmer, binaryEntropy_gilmer_fixed_point, union_prob_gilmer, gilmerConstant, gilmer_constant_sq_relation, gilmer_chain_family Extremal Combinatorics & Information Theory Gilmer (2022), Frankl (1979), Chase & Lovett (2022) 100% Verified (0 axioms) (Golden-ratio constant $c_0 = \frac{3-\sqrt{5}}{2} \approx 0.381966$, coordinate union probability $q(p)=2p-p^2$, binary entropy fixed point $H(2c_0 - c_0^2)=H(c_0)$, and certified concrete families verified; Frankl conjecture target formally declared)
10 Kelley–Meka Density Increment Dynamics & Constant Calibration kelley_meka_density_at_10_6, kelley_meka_dominates_roth_at_scale, kelley_meka_dominates_bourgain_at_scale, cumulative_rank_bound, density_increment_step, bohr_set_card_lower_bound Additive Combinatorics & Harmonic Analysis Kelley & Meka (2023), Bloom & Sisask (2020), Bourgain (1999) 100% Verified (0 axioms) (Bohr set regularity, cumulative rank bounds $\sum \Delta \mathrm{rk} \le O(\log^2(1/\alpha_0))$, density boost accumulation, and certified numerical scales verified)
11 Brieskorn Manifolds, Topological Spheres, and the 28 Exotic 7-Spheres exotic_exponents_isBrieskornSphere, exotic_spheres_generate_all, milnorKervaire_surjective, k_28_is_standard, k_1_to_27_are_exotic, pairwise_coprime_isBrieskornSphere Differential Topology & Singularity Links Brieskorn (1966), Milnor & Kervaire (1963), Hirzebruch (1966), Casson (1985) 100% Verified (0 axioms) (Brieskorn graph sphere criterion, 28 Milnor-Kervaire exotic 7-spheres in $\Theta_7 \cong \mathbb{Z}/28\mathbb{Z}$, standard sphere for $k=28$, and 27 strictly exotic structures verified)
12 Irreducible SU(2) Character Varieties of Brieskorn Homology Spheres and Casson Invariants sphericalAngleTriple_odd_sum, candidateRepFinset_card, frickeVogt_discriminant_identity, frickeVogt_order2_boundary_circle, central_fiber_odd_power, casson_su2_eq_brieskorn_2_3_5 Gauge Theory, Character Varieties & 3-Manifold Invariants Fintushel & Stern (1990), Casson (1985), Brieskorn (1966), Fricke & Klein (1897) 100% Verified (0 axioms) (Diophantine angle conditions for central fiber $h \mapsto -I$, candidate representation search space $(p-1)(q-1)(r-1)$, exact Casson invariant agreements, and Fricke-Vogt trace relations verified)
13 Hyperbolic Orbifold Spectral Zeta, Gauss–Bonnet Area, and the Selberg Trace Formula gauss_bonnet_area, residue_area_product, hyperbolicArea_sig34, hyperbolicArea_sig23, scattering_unitarity_critical_line, trace_identity_with_normalizedArea Spectral Geometry & Automorphic Forms Selberg (1956), Hejhal (1983), Venkov (1990), Buser (1992) 100% Verified (0 axioms) (Orbifold Gauss-Bonnet area $\mathrm{Area}=2\pi(1-1/p-1/q)$, Eisenstein scattering determinant $\phi(s)\phi(1-s)=1$, residue product $\mathrm{Res}\cdot\mathrm{Area}=2\pi$, and Selberg trace formula verified)
14 Order-4 Picard–Fuchs Differential Equations, Monodromy, and Mirror Yukawa Couplings pfSymbol_expansion, sum_alpha_3_4_infty, isInfinitesimalSymplectic_N, isInfinitesimalSymplectic_N_Omega6, symplecticPairing_N_invariant, quintic_instanton_k2, N_sq_eq_zero Mirror Symmetry, Differential Equations & Symplectic Monodromies Candelas et al. (1991), Morrison (1993), Griffiths (1970), Deligne (1970) 100% Verified (0 axioms) (Order-4 Picard-Fuchs operator symbol $\mathcal{L}_4$, Calabi-Yau self-duality sum $\sum \alpha_i = 2$, unipotent cusp monodromy $N = T_0 - I_4 \in \mathrm{Sp}_4(\mathbb{Z})$, Griffiths transversality $N^T J + J N = 0$, and multi-instanton BPS expansions verified)
15 Deligne–Schmid Mixed Hodge Weight Filtration and Symplectic Monodromy DeligneWeightSpace_shift, DeligneWeightSpace_mono, DeligneWeightSpace_top, DeligneWeightSpace_zero, W_MUM_complete_chain, Q_N_u_add_w_strictly_positive, Q_N_symmetric Hodge Theory & Degenerations of Mixed Hodge Structures Deligne (1971), Schmid (1973), Steenbrink (1976), Morrison (1993) 100% Verified (0 axioms) (Universal canonical subspace formula $W_l(N, k) = \bigcup_j (\ker(N^{j+1}) \cap \mathrm{im}(N^{j - l + k}))$, shift property $N(W_l) \subseteq W_{l-2}$, 2-step Type II and 4-step Type III MUM filtrations on $\mathbb{Z}^4$, and Hodge-Riemann polarization positivity verified)
16 Jenrich's 64-Dimensional Counterexample to Borsuk's Conjecture not_borsuk_conjecture_64, dist_eq_d1_of_diam_lt, isClique_of_diam_lt, card_le_mul_card_cover, carrier_card_eq, reduction_vector_ortho_carrier, reduction_vector_nonortho_B2, jenrich_partition_lower_bound, almost_counterexample_63, reduction_vector_q_zero_iff_mem_C, no_vertex_augmentation_in_W63 Discrete Geometry & Metric Embeddings Jenrich & Brouwer (2014), Bondarenko (2013, 2014), Borsuk (1933) 100% Verified (0 axioms) (Fundamental two-distance clique-diameter lemma, $G_2(4)$ Euclidean representation, Jenrich reduction vector $p \in \mathbb{R}^{416}$ orthogonal to 352 points of $S_{64} = C \cup B_1$, codimension drop to $\le 64$, and Borsuk refutation $\lceil 352 / 5 \rceil = 71 > 65$ verified; 63D almost-counterexample $64 = 63 + 1$ and 63D vertex augmentation obstruction $\ker(q) \cap V = C$ verified)
17 Vitushkin's Refutation of Engel's 1955 2D Jacobian Paper jacobian_canonical, jacobian_antisymm, jacobian_shear_general_X, jacobian_shear_general_Y, vitushkin_cross_term_jacobian, vitushkin_jacobian_ne_one Affine Algebraic Geometry & Jacobian Conjecture Engel (1955), Vitushkin (1975), Bass, Connell, & Wright (1982) 100% Verified (0 axioms) (Canonical symplectic Jacobian form, polynomial shear invariance, Vitushkin defect formula $J(X+cXY, Y) = 1+cY$, cross-term defect $1-4XY \ne 1$, and failure of triangular degree reduction verified)
18 Gaoyong Zhang's 1994/1999 Busemann–Petty $\mathbb{R}^4$ Resolution & Audit lutwak_intersection_body_comparison, intersection_body_4d_universal, busemann_petty_dim_4, zhang_1994_counterexample_refuted, busemann_petty_dim_4_contrapositive, busemann_petty_dim_3, busemann_petty_counterexample_dim_ge_5 Convex Geometry & Geometric Tomography Busemann & Petty (1956), Lutwak (1988), Gardner (1994), Zhang (1994, 1999) 100% Verified (0 axioms) (Spherical Radon transform $\mathcal{R}$, self-adjointness, Lutwak intersection body duality comparison, universal 4D intersection body theorem, affirmative resolution in dimension 4, refutation of Zhang's 1994 counterexample, and counterexample existence for $n \ge 5$ verified)
19 Shitov's Counterexample to Hedetniemi's Conjecture chromaticNumber_le_of_hom, chromaticNumber_tensorProduct_le_min, colorable_tensorProduct_of_left, colorable_exponentialProduct, shitov_pair_strict_inequality, not_hedetniemi_conjecture Graph Theory & Chromatic Numbers Hedetniemi (1966), Shitov (2019), Tardif & Zhu (2019), El-Zahar & Sauer (1985) 100% Verified (0 axioms) (Categorical tensor product $G \times H$, projection homomorphisms, exponential graphs $\mathcal{E}_c(H)$, evaluation colorings, Shitov pair strict inequality $\chi(G \times H) < \min(\chi(G), \chi(H))$, and full refutation of Hedetniemi's conjecture verified)
20 The 7D Keller Cube-Tiling Bridge coordinateBlock_independent, keller_clique_card_le, liftedSet_cubesDisjoint, liftedSet_isFaceshareFree, keller_conjecture_false_of_max_clique, keller_conjecture_seven_of_sat_certificate, keller_conjecture_eight_false_of_mackey_clique, embed_clique, keller_conjecture_nine_false_of_mackey_and_lifting Discrete Geometry & Cube Tilings Keller (1930), Perron (1940), Corrádi & Szabó (1990), Lagarias & Shor (1992), Mackey (2002), Kisielewicz (2017), Brakensiek et al. (2022) 100% Verified (0 axioms) (Discrete Keller graph $G_{d, s}$, $2^d$ coordinate block partition, universal clique bound $\omega(G_{d, s}) \le 2^d$, Corrádi–Szabó bridge theorem, Mackey 8D/9D disproofs, and 7D affirmative resolution theorem from BHMN SAT certificates verified)
21 The Erdős–Gyárfás Conjecture and Girth Hunter Scaffold IsPowerOfTwoCycleLength, HasPowerOfTwoCycle, ErdosGyarfasConjecture, CounterexampleCertificate, disprove_erdos_gyarfas, K33_hasPowerOfTwoCycle, K33_cannot_be_counterexample Extremal Graph Theory & Cycle Spectra Erdős (1975), Royle & Kauers (2011) 100% Verified (0 axioms) (Power-of-two cycle predicate, constructive counterexample certificate infrastructure, soundness meta-theorem, and $K_{3,3}$ cycle spectrum obstruction certifying 4-cycle containment and counterexample rejection verified)
22 The Lonely Runner Conjecture at $k = 8$ and Obstruction Analysis IsFarFromInt, IsLonely, lonelyThreshold_eight, LonelyRunnerConjecture8, CounterexampleCertificate8, disprove_lonely_runner_8, canonicalSpeeds8_lonely_at_one_ninth, canonicalSpeeds8_cannot_be_counterexample Diophantine Approximation & View-Obstruction Wills (1967), Cusick (1974), Rosenfeld (2025) 100% Verified (0 axioms) (Real integer distance, runner loneliness, canonical threshold $1/(k+1)=1/9$, general and specialized conjectures, constructive certificate infrastructure, soundness meta-theorem, and canonical consecutive speeds $(1, \dots, 8)$ certifying simultaneous loneliness at $t = 1/9$ verified)

Detailed Formalization Writeups

1. The Expander Mixing Lemma & Spectral Expansion

  • Module: Formalization/ExpanderMixing.lean
  • Primary Declarations: expander_mixing_lemma, expander_mixing_lemma_simplified, hoffman_independence_bound, chromatic_number_spectral_bound, decompPerp_normSq, decompPerp_orthogonal, positive_edge_density_of_large_sets
  • Mathematical Overview: Let $G = (V, E)$ be a $d$-regular graph on $n = |V|$ vertices with adjacency matrix $A$ having eigenvalues $d = \lambda_1 \ge \lambda_2 \ge \dots \ge \lambda_n \ge -d$. Let $\lambda(G) = \max_{i \ge 2} |\lambda_i|$ denote the absolute second eigenvalue (spectral expansion parameter). For any vertex subsets $S, T \subseteq V$, the number of directed edges between $S$ and $T$ is $e(S, T) = \mathbf{1}_S^T A \mathbf{1}_T$. The Expander Mixing Lemma (Alon & Chung 1988) bounds the discrepancy from the expected random edge density: $$\left| e(S, T) - \frac{d |S| |T|}{n} \right| \le \lambda(G) \sqrt{|S| \left(1 - \frac{|S|}{n}\right) |T| \left(1 - \frac{|T|}{n}\right)} \le \lambda(G) \sqrt{|S| |T|}$$
  • Formalization Highlights:
    • Machine-verified orthogonal decomposition $\mathbf{1}_S = \mathbf{1}_S^\parallel + \mathbf{1}_S^\perp$ where $\mathbf{1}_S^\parallel = \frac{|S|}{n} \mathbf{1}$ and $\mathbf{1}_S^\perp \in \mathbf{1}^\perp$ (decompPerp_orthogonal).
    • Machine-verified exact variance norm formula $|\mathbf{1}_S^\perp|^2 = |S| \left(1 - \frac{|S|}{n}\right)$ (decompPerp_normSq).
    • Formalization of the Hoffman–Alon bound on the independence number $\alpha(G) \le \frac{\lambda}{d + \lambda} n$ and the chromatic lower bound $\chi(G) \ge 1 + \frac{d}{\lambda}$.

2. The Alon–Boppana Spectral Lower Bound & Ramanujan Expanders

  • Root Module: Formalization/AlonBoppana.lean
  • Submodules:
    • Formalization/AlonBoppana/Basic.lean: Adjacency matrix $A \in M_{V \times V}(\mathbb{R})$, $d$-regularity, symmetry $A^T = A$, all-ones eigenvector $A \mathbf{1} = d \mathbf{1}$, and Euclidean inner product spaces.
    • Formalization/AlonBoppana/SphericalShell.lean: Spherical shells $S_k(x_0) = {v \in V : \mathrm{dist}(x_0, v) = k}$, pairwise disjointness $S_j \cap S_k = \emptyset$, and backward/forward neighbor partition bounds.
    • Formalization/AlonBoppana/NilliProfile.lean: Nilli's radial geometric test function $g(k) = (d-1)^{-k/2}$, step product recurrence $g(k)g(k+1) = \sqrt{d-1} g(k+1)^2$, orthogonal linear combinations, and variational Rayleigh quotient bounds.
    • Formalization/AlonBoppana/SpectralBound.lean: Variational Courant–Fischer definition of $\lambda_2(G)$, non-asymptotic Alon–Boppana bound $\lambda_2(G) \ge 2\sqrt{d-1}(1 - 2/D) - O(1)/D$, Nilli's diameter bound $\lambda_2(G) \ge 2\sqrt{d-1} - \frac{2\sqrt{d-1}-1}{\lfloor D/2 \rfloor}$, and Ramanujan graph predicate with certified spectral gap $d - \lambda_2 \ge d - 2\sqrt{d-1}$.

3. The Discrete Cheeger Lower Bound for Regular Graphs

  • Module: Formalization/DiscreteCheeger.lean
  • Primary Declarations: cheeger_lower_bound, cheeger_lower_bound_normalized, ramanujan_cheeger_lower_bound, vertex_expansion_spectral_bound, dirichletEnergy_eq_laplacianQuadraticForm
  • Mathematical Overview: For a connected $d$-regular graph $G$, the Cheeger isoperimetric constant $h(G) = \min_{0 < |S| \le n/2} \frac{e(S, S^c)}{|S|}$ characterizes edge expansion. The Discrete Cheeger Lower Bound (Alon & Milman 1985; Dodziuk 1984) establishes the fundamental lower bound on $h(G)$ via the spectral gap $\Delta = d - \lambda_2(G)$: $$\frac{d - \lambda_2(G)}{2} \le h(G)$$ In normalized form with $\gamma = 1 - \lambda_2/d$: $\frac{\gamma}{2} \le \frac{h(G)}{d}$.
  • Formalization Highlights:
    • Machine-verified Dirichlet energy identity $\mathcal{E}(f) = \frac{1}{2}\sum_{u, v} A_{uv}(f(u)-f(v))^2 = \langle f, L f \rangle$ (dirichletEnergy_eq_laplacianQuadraticForm).
    • Machine-checked Ramanujan expansion lower bound $h(G) \ge \frac{d - 2\sqrt{d-1}}{2}$.
    • Spectral lower bound on vertex boundary expansion: $\frac{|\partial_V S|}{|S|} \ge \frac{h(G)}{d} \ge \frac{\gamma}{2}$.

4. Tanner's Vertex Expansion Bound for Regular Graphs

  • Module: Formalization/TannerExpansion.lean
  • Primary Declarations: tanner_vertex_expansion_bound, tanner_expansion_ratio_bound, tanner_small_set_expansion, tanner_ramanujan_expansion, tanner_ramanujan_expansion_factored, tanner_half_set_expansion, tanner_half_set_expansion_ratio, tanner_vertex_margin_bound, tanner_ramanujan_half_set_expansion, spectral_operator_norm_bound
  • Mathematical Overview: For any non-empty subset $S \subseteq V$ in a $d$-regular graph $G$ on $n$ vertices, Tanner's Theorem (1984) establishes: $$|N(S)| \ge \frac{d^2 |S|}{\frac{d^2 - \lambda^2}{n} |S| + \lambda^2}$$ where $\lambda = \lambda(G)$ is the spectral expansion parameter.
  • Formalization Highlights:
    • Cauchy–Schwarz on the neighborhood: $(d |S|)^2 = (\sum_{u \in N(S)} A \mathbf{1}_S(u))^2 \le |N(S)| \cdot |A \mathbf{1}_S|^2$.
    • Exact spectral decomposition: $|A \mathbf{1}_S|^2 = \frac{d^2 |S|^2}{n} + |A \mathbf{1}_S^\perp|^2 \le |S|(\frac{d^2 - \lambda^2}{n}|S| + \lambda^2)$.
    • Small-set expansion: for $|S| \le \alpha n$, $|N(S)| \ge \frac{d^2}{\alpha(d^2-\lambda^2)+\lambda^2}|S|$.
    • Half-set bound: for $|S| \le n/2$, $|N(S)| \ge \frac{2d^2}{d^2+\lambda^2}|S|$ and $|N(S)| - |S| \ge \frac{d^2-\lambda^2}{d^2+\lambda^2}|S|$.
    • Ramanujan bound: $|N(S)| \ge \frac{d^2 |S|}{\frac{(d-2)^2}{n}|S| + 4(d-1)}$.

5. Freiman's Structure Theorem & Ruzsa Sumset Calculus

  • Root Module: Formalization/RuzsaFreiman.lean
  • Submodules:
    • Formalization/RuzsaFreiman/Basic.lean: Sumsets $A + B$, difference sets $A - B$, doubling constants $\sigma(A) = |A+A|/|A|$, difference constants $\delta(A) = |A-A|/|A|$, and translation bijections (add_singleton_eq_image).
    • Formalization/RuzsaFreiman/RuzsaDistance.lean: Ruzsa distance $d_R(A, B) = \log \frac{|A - B|}{\sqrt{|A| |B|}}$, symmetry via verified reflection bijection $|A - B| = |B - A|$, and the Ruzsa Triangle Inequality: $$|B| \cdot |A - C| \le |A - B| \cdot |B - C| \implies d_R(A, C) \le d_R(A, B) + d_R(B, C)$$
    • Formalization/RuzsaFreiman/PlunneckeRuzsa.lean: The Plünnecke–Ruzsa Inequality $|k B - \ell B| \le K^{k + \ell} |A|$ whenever $|A + B| \le K |A|$, Petridis minimal magnification subsets, and tripling bounds $|3A| \le K^3 |A|$.
    • Formalization/RuzsaFreiman/FreimanTheorem.lean: Multi-dimensional Generalized Arithmetic Progressions (GAPs), Freiman homomorphisms of order $k$, Freiman's Theorem in $\mathbb{Z}$, Bogolyubov's lemma on $2A - 2A$, and the Polynomial Freiman–Ruzsa (PFR) Theorem in $\mathbb{F}_2^n$ (Gowers, Green, Manners, Tao 2023): $$A \subseteq \bigcup_{i=1}^{2 K^{12}} (x_i + H), \quad |H| \le |A|$$

6. Roth's Theorem on 3-Term Arithmetic Progressions

  • Root Module: Formalization/RothsTheorem.lean
  • Submodules:
    • Formalization/RothsTheorem/ThreeAP.lean: 3-AP predicate $x + z = 2y$, progression-free sets IsThreeAPFree, the normalized counting functional $\Lambda(f_1, f_2, f_3) = \frac{1}{|G|^2} \sum_{x, d} f_1(x) f_2(x+d) f_3(x+2d)$, and trivial progression count $\Lambda(1_A, 1_A, 1_A) = |A| / |G|^2$.
    • Formalization/RothsTheorem/FourierAnalysis.lean: Complex additive characters $\mathrm{AddChar}(G)$, discrete Fourier transform $\widehat{f}(\chi) = \sum_x f(x) \overline{\chi(x)}$, Plancherel identity $\sum_\chi |\widehat{f}(\chi)|^2 = |G| \sum_x |f(x)|^2$, Fourier inversion, and Roth's Large Fourier Coefficient Dichotomy: $$\exists \chi \ne 1, \quad |\widehat{\mathbf{1}_A}(\chi)| \ge \frac{\alpha^2}{2} |G|$$
    • Formalization/RothsTheorem/DensityIncrement.lean: Arithmetic progression structure in $\mathbb{Z}$ with verified cardinality (progression_card), relative density $\frac{|A \cap P|}{|P|}$, Dirichlet approximation, the Density Increment Lemma ($\frac{|A \cap P|}{|P|} \ge \alpha + \alpha^2/16$), and the quantitative Roth bound $r_3(N) \le C \frac{N}{\log \log N}$.

7. Szemerédi's Regularity Lemma & Partition Energy Dynamics

  • Root Module: Formalization/SzemerediRegularity.lean
  • Submodules:
    • Formalization/SzemerediRegularity/PairDensity.lean: Bipartite edge count $e(X, Y)$, pair edge density $d(X, Y) = \frac{e(X, Y)}{|X| |Y|}$, verified density bounds $0 \le d(X, Y) \le 1$, verified density symmetry $d(X, Y) = d(Y, X)$, and the formal definition of $\varepsilon$-regular pairs: $$\forall A \subseteq X, B \subseteq Y, \quad |A| \ge \varepsilon |X|, |B| \ge \varepsilon |Y| \implies |d(A, B) - d(X, Y)| \le \varepsilon$$
    • Formalization/SzemerediRegularity/EnergyIncrement.lean: Graph partitions GraphPartition, normalized quadratic partition energy $E(\mathcal{P}) = \sum_{X, Y \in \mathcal{P}} \frac{|X||Y|}{n^2} d(X, Y)^2$, verified energy bounds $0 \le E(\mathcal{P}) \le 1$ (energy_le_one), Cauchy–Schwarz refinement monotonicity $E(\mathcal{P}') \ge E(\mathcal{P})$, the Energy Exhaustion Principle, and the quantitative iteration bound $k \le 2 / \varepsilon^5$.
    • Formalization/SzemerediRegularity/RegularityLemma.lean: Szemerédi's Regularity Lemma $(m \le |\mathcal{P}| \le M(\varepsilon, m))$, the Triangle Counting Lemma $(N_\triangle \ge (1 - 2\varepsilon) d_{12} d_{23} d_{31} |V_1| |V_2| |V_3|)$, the Triangle Removal Lemma (Ruzsa & Szemerédi 1978), and the graph-theoretic deduction of Roth's theorem.

8. The Cauchy–Davenport Theorem and Iterated Sumsets

9. Gilmer's Entropy Bound on Frankl's Union-Closed Sets Conjecture

  • Module: Formalization/GilmerUnionClosed.lean
  • Primary Declarations: gilmer_two_element_family, powerset_satisfies_gilmer, binaryEntropy_gilmer_fixed_point, union_prob_gilmer, gilmerConstant, gilmer_constant_sq_relation, gilmer_chain_family, gilmer_singleton_family
  • Mathematical Overview: For finite union-closed families $\mathcal{F} \subseteq \mathcal{P}(U)$ with $|\mathcal{F}| \ge 2$, Gilmer (2022) introduced an information-theoretic approach to Frankl's conjecture ($c = 1/2$) by proving the existence of an element with frequency at least: $$p_u \ge c_0 = \frac{3 - \sqrt{5}}{2} \approx 0.381966$$
  • Formalization Highlights:
    • Golden-ratio quadratic identity $c_0^2 = 3c_0 - 1$ and numerical bounds $0.38 < c_0 < 0.39$.
    • Coordinate Bernoulli union operator $q(p) = 2p - p^2$ and interval domination $2p - p^2 \le 1 - p$ on $[0, c_0]$.
    • Machine-verified binary entropy fixed point identity: $$2 c_0 - c_0^2 = 1 - c_0 \implies H(2 c_0 - c_0^2) = H(c_0)$$
    • Full machine proofs for standard extremal families: power sets $\mathcal{P}(X)$, chains, and singletons.
    • The overarching Frankl conjecture is formally specified as a target Prop predicate.

10. Kelley–Meka Density Increment Dynamics & Constant Calibration

  • Module: Formalization/KelleyMeka.lean
  • Primary Declarations: kelley_meka_density_at_10_6, kelley_meka_dominates_roth_at_scale, kelley_meka_dominates_bourgain_at_scale, cumulative_rank_bound, density_increment_step, kelley_meka_density_at_10_9, kelley_meka_density_at_10_12, kelley_meka_density_at_2_64, kelley_meka_density_at_10_100
  • Mathematical Overview: Kelley & Meka (2023) established the breakthrough quasi-polynomial density increment strategy for 3-AP free subsets in $\mathbb{Z}/N\mathbb{Z}$, overcoming the polynomial Fourier barrier.
  • Formalization Highlights:
    • Structured character Bohr sets $B(\Gamma, \rho)$ with spectral concentration on low-dimensional duals and relative density lower bounds.
    • Multiplicative and additive density boost accumulation $\alpha_{i+1} \ge \alpha_i + c \alpha_i^2$ with bounded rank growth $\Delta \mathrm{rk} \le O(\log(1/\alpha_i))$.
    • Cumulative rank control $\sum \Delta \mathrm{rk} \le O(\log^2(1/\alpha_0))$ and finite step termination bounds.
    • Certified proofs that the Kelley–Meka rate asymptotically dominates Roth's ($1/\log \log N$) and Bourgain's ($\sqrt{\log \log N / \log N}$) bounds.
    • Machine proofs of explicit numerical constants and scale calibrations at $N = 10^6, 10^9, 10^{12}, 2^{64}, 10^{100}$.

11. Brieskorn Manifolds, Topological Spheres, and the 28 Exotic 7-Spheres

  • Module: Formalization/BrieskornManifolds.lean
  • Primary Declarations: exotic_exponents_isBrieskornSphere, exotic_spheres_generate_all, milnor_kervaire_invariant_surjective, signature_2_3_5, signature_2_3_7, signature_2_3_11, signature_2_5_7, casson_2_3_5, casson_2_3_7, casson_2_3_11, casson_2_5_7, isBrieskornSphere
  • Mathematical Overview: For exponents $a = (a_0, \dots, a_{n-1}) \in \mathbb{N}^n$, the Brieskorn manifold $\Sigma(a)$ is the singularity link $f_a^{-1}(0) \cap S^{2n-1} \subset \mathbb{C}^n$ where $f_a(z) = \sum z_j^{a_j}$.
  • Formalization Highlights:
    • Machine-verified Brieskorn–Hirzebruch Sphere Criterion (1966) via the divisibility graph $G(a)$.
    • Construction of the infinite family $\Sigma(2, 2, 2, 3, 6k-1)$ in $\mathbb{C}^5$, yielding topological 7-spheres $S^7$.
    • The Milnor–Kervaire signature invariant $\kappa(k) \equiv k \pmod{28}$ surjectively generates all 28 distinct smooth structures in $b P_8 \cong \Theta_7 \cong \mathbb{Z}/28\mathbb{Z}$.
    • Exact Milnor fiber signature and Casson invariant formula $\lambda(\Sigma(p, q, r)) = \frac{1}{8} |\sigma(p, q, r)|$, certified for $\Sigma(2,3,5), \Sigma(2,3,7), \Sigma(2,3,11), \Sigma(2,5,7)$.

12. Irreducible SU(2) Character Varieties of Brieskorn Homology Spheres and Casson Invariants

  • Module: Formalization/BrieskornSU2CharacterVariety.lean
  • Primary Declarations: IsSphericalAngleTriple, card_irred_su2_2_3_5, card_irred_su2_2_3_7, card_irred_su2_2_3_11, card_irred_su2_2_5_7, casson_su2_eq_brieskorn_2_3_5, casson_su2_eq_brieskorn_2_3_7, casson_su2_eq_brieskorn_2_3_11, casson_su2_eq_brieskorn_2_5_7, frickeVogt_discriminant_identity, frickeVogt_hypersurface_vanishing
  • Mathematical Overview: For Brieskorn homology 3-spheres $\Sigma(p, q, r)$, irreducible $SU(2)$ representations $\rho : \pi_1(\Sigma(p,q,r)) \to SU(2)$ map the central fiber $h \mapsto -I$.
  • Formalization Highlights:
    • Reduction of irreducible representations to strict spherical triangle angle inequalities on rotation parameters $(a/p, b/q, c/r) \in (0, 1)^3$.
    • Certified representation counts: $#\mathcal{R}^(\Sigma(2,3,5)) = 2, #\mathcal{R}^(\Sigma(2,3,7)) = 2, #\mathcal{R}^(\Sigma(2,3,11)) = 4, #\mathcal{R}^(\Sigma(2,5,7)) = 4$.
    • Machine-verified identity $\lambda_{SU(2)}(\Sigma(p, q, r)) = \frac{1}{2} #\mathcal{R}^*(\Sigma(p, q, r)) = \lambda_{\mathrm{Brieskorn}}(\Sigma(p, q, r))$.
    • Formalization of the Fricke–Vogt trace variety $t_x^2 + t_y^2 + t_z^2 + t_x t_y t_z - 4 = 0$.

13. Hyperbolic Orbifold Spectral Zeta, Gauss–Bonnet Area, and the Selberg Trace Formula

  • Module: Formalization/OrbifoldSpectralZeta.lean
  • Primary Declarations: gauss_bonnet_area, residue_area_product, hyperbolicArea_sig34, hyperbolicArea_sig23, hyperbolicArea_sig25, hyperbolicArea_sig35, scattering_unitarity_critical_line, trace_identity_with_normalizedArea, scattering_determinant_functional_equation, chiOrb_sig34
  • Mathematical Overview: Spectral geometry of 1-cusped hyperbolic 2-orbifolds $\mathcal{O}(p, q, \infty) = \Delta(p, q, \infty) \backslash \mathbb{H}$ with $1/p + 1/q < 1$.
  • Formalization Highlights:
    • Rational orbifold Euler characteristic $\chi_{\text{orb}} = \frac{1}{p} + \frac{1}{q} - 1 < 0$ and Gauss–Bonnet area $\mathrm{Area}(\mathcal{O}) = 2\pi(1 - 1/p - 1/q)$.
    • Certified exact areas: $\mathrm{Area}(\mathcal{O}(3,4,\infty)) = 5\pi/6$, $\mathrm{Area}(\mathcal{O}(2,3,\infty)) = \pi/3$, $\mathrm{Area}(\mathcal{O}(2,5,\infty)) = 3\pi/5$, $\mathrm{Area}(\mathcal{O}(3,5,\infty)) = 14\pi/15$.
    • Eisenstein scattering determinant functional equation $\phi(s)\phi(1-s) = 1$ and critical line unitarity $|\phi(1/2 + ir)|^2 = 1$.
    • Residue-area product formula $\mathrm{Res}_{s=1} \phi(s) \cdot \mathrm{Area} = 2\pi$.
    • Orbifold Selberg trace formula decomposing discrete cusp forms, Eisenstein scattering, elliptic cone point contributions, and closed geodesics.

14. Order-4 Picard–Fuchs Differential Equations, Monodromy, and Mirror Yukawa Couplings

  • Module: Formalization/PicardFuchsMirrorMonodromy.lean
  • Primary Declarations: pfSymbol_expansion, sum_alpha_3_4_infty, sum_alpha_3_4_mod, sum_alpha_2_3_mod, isInfinitesimalSymplectic_N, isInfinitesimalSymplectic_N_Omega6, symplecticPairing_N_invariant, isSymplecticMatrix_T0, N_sq_eq_zero, quintic_instanton_k2, yukawa_bps_k1
  • Mathematical Overview: Analytical structures of order-4 Picard–Fuchs ODEs $\mathcal{L}4 = \theta^4 - z \prod{i=1}^4 (\theta + \alpha_i)$ for modular families $\Delta(3,4,\infty)$ and $\Delta(2,3,\infty)$.
  • Formalization Highlights:
    • Operator symbol expansion $\mathcal{L}_4 = (1-z)\theta^4 - z(e_1\theta^3 + e_2\theta^2 + e_3\theta + e_4)$.
    • Calabi–Yau self-duality sum condition $\sum_{i=1}^4 \alpha_i = 2$.
    • Unipotent cusp monodromy $N = T_0 - I_4 \in \mathrm{Sp}_4(\mathbb{Z})$ ($N^2 = 0$ Type II, $N^4 = 0$ Type III MUM).
    • Infinitesimal symplectic Lie algebra invariance $N^T J + J N = 0$ (Griffiths transversality).
    • Classical Yukawa couplings $C_{zzz}(z) = \frac{\kappa_0}{z^3 (1 - \mu z)}$ and multi-instanton BPS expansion $C_{ttt}(q) = K_0 + \sum_{d=1}^M \frac{d^3 n_d q^d}{1 - q^d}$.

15. Deligne–Schmid Mixed Hodge Weight Filtration and Symplectic Monodromy

  • Module: Formalization/UniversalMonodromyWeightFiltration.lean
  • Primary Declarations: DeligneWeightSpace_shift, DeligneWeightSpace_mono, DeligneWeightSpace_mono_le, DeligneWeightSpace_top, DeligneWeightSpace_zero, W_MUM_complete_chain, W_MUM_shift_inclusion, W_mod_shift_inclusion, Q_N_u_add_w_strictly_positive, Q_N_gamma_add_delta_strictly_positive, Q_N_symmetric
  • Mathematical Overview: Deligne's canonical weight filtration formula for nilpotent monodromy operators $N$: $$W_l(N, k) = \sum_{j=0}^k \left( \ker(N^{j+1}) \cap \mathrm{im}(N^{j - l + k}) \right)$$
  • Formalization Highlights:
    • Universal filtration properties: monotonicity $W_l \subseteq W_{l+1}$, shift property $N(W_l) \subseteq W_{l-2}$, and extremal spaces $W_{2k} = V$.
    • Explicit 2-step Type II weight filtration on $\mathbb{Z}^4$: $W_0 = {0} \subset W_1 = \mathrm{im}(N) \subset W_2 = \mathbb{Z}^4$.
    • Explicit 4-step Type III MUM filtration: $W_0 \subset W_1 \subset W_2 \subset W_3 \subset W_4 = \mathbb{Z}^4$.
    • Hodge–Riemann polarized bilinear form $Q_N(v, w) = \langle v, N w \rangle_J$ with machine-checked symmetry and strict positivity on primitive generators $Q_N(u+w, u+w) = 2 > 0$.

16. Jenrich & Brouwer's 64-Dimensional Counterexample to Borsuk's Conjecture

  • Module: Formalization/JenrichBorsuk64.lean
  • Primary Declarations: not_borsuk_conjecture_64, dist_eq_d1_of_diam_lt, isClique_of_diam_lt, card_le_mul_card_cover, dist_sq_of_adj, dist_sq_of_not_adj, carrier_card_eq, reduction_vector_ortho_carrier, reduction_vector_nonortho_B2, jenrich_partition_lower_bound, reduction_vector_q_ortho_C, reduction_vector_q_nonortho_B1, reduction_vector_q_nonortho_B2, reduction_vector_q_nonortho_B3, reduction_vector_q_zero_iff_mem_C, no_vertex_augmentation_in_W63, almost_counterexample_63
  • Mathematical Overview: In 1933, Karol Borsuk asked whether every bounded set $S \subset \mathbb{R}^n$ can be partitioned into at most $n+1$ subsets of strictly smaller diameter. Jeff Kahn & Gil Kalai (1993) disproved the conjecture in high dimensions ($n \ge 2014$). Andriy V. Bondarenko (2013) dramatically lowered this bound to $n = 65$ via a 416-point two-distance set from the strongly regular graph $G_2(4) = \mathrm{srg}(416, 100, 36, 20)$. Shortly thereafter, Thomas Jenrich and Andries E. Brouwer (2014) constructed a 64-dimensional subset of 352 points, refuting Borsuk's conjecture in dimension 64.
  • Formalization Highlights:
    • Metric Foundations & Clique Reduction: In any two-distance metric set with distances $d_1 < d_2$, any subset of diameter strictly less than $d_2$ contains no pairs at distance $d_2$, hence induces a clique in the distance-$d_1$ graph (isClique_of_diam_lt).
    • Pigeonhole Partition Bound: Any cover of a finite set $S$ by parts of maximum clique size $\omega(G) \le m$ requires at least $\lceil |S| / m \rceil$ parts (card_le_mul_card_cover).
    • $G_2(4)$ Euclidean Representation: The shifted Gram matrix $Y = A + 4I$ yields squared distances $|y_i - y_j|^2 \in {144, 192}$ ($d_1 = 12, d_2 = \sqrt{192}$), with centered vectors spanning the $f=65$ dimensional eigenspace $F$ with $\omega(G_2(4)) \le 5$. Bondarenko's full set requires $\lceil 416 / 5 \rceil = 84 > 66$ parts.
    • Jenrich's Codimension Reduction: The vertex partition $V = B_1 \cup B_2 \cup B_3 \cup C$ ($|B_h| = 32, |C| = 320$) and the reduction vector $p = \mathbf{1}{B_2} - \mathbf{1}{B_3}$ satisfy $\langle p, y_i \rangle = 0$ for all 352 points of $S_{64} = C \cup B_1$, while $\langle p, y_j \rangle = 24 \ne 0$ on $B_2$, proving the span of $S_{64}$ has dimension at most $65 - 1 = 64$.
    • Main Impossibility Theorem: Covering $S_{64}$ requires at least $\lceil 352 / 5 \rceil = 71$ parts of smaller diameter. Since $71 > 64 + 1 = 65$, Borsuk's conjecture is false in $\mathbb{R}^{64}$ (not_borsuk_conjecture_64).
    • 63D Almost-Counterexample: Secondary reduction vector $q = 2\mathbf{1}{B_1} - \mathbf{1}{B_2} - \mathbf{1}_{B_3}$ reduces $C$ ($|C| = 320$) to $\le 63$ dimensions, where $\lceil 320 / 5 \rceil = 64 = 63 + 1$ (almost_counterexample_63).
    • 63D Vertex Augmentation Obstruction & Maximal Subspace Theorem: Proves that every vertex outside $C$ has strictly non-zero inner product with $q$ ($\langle q, y_j \rangle = 48$ on $B_1$, $-24$ on $B_2 \cup B_3$). Thus $\ker(q) \cap V = C$ (reduction_vector_q_zero_iff_mem_C), certifying that no vertex $v \in V \setminus C$ can be added to $C$ while staying in the 63-dimensional subspace $W_{63} = \ker(p) \cap \ker(q) \cap \ker(\mathbf{1})$ (no_vertex_augmentation_in_W63).

17. Vitushkin's Refutation of Engel's 1955 2D Jacobian Paper

  • Module: palomar/engel_jacobian_refutation/Solution.lean
  • Primary Declarations: jacobian_canonical, jacobian_antisymm, jacobian_shear_general_X, jacobian_shear_general_Y, vitushkin_cross_term_jacobian, vitushkin_jacobian_ne_one
  • Mathematical Overview: In 1955, Wolfgang Engel published a paper claiming to construct an explicit counterexample of degree 8 to the two-variable Jacobian conjecture. In 1975, A. G. Vitushkin recalculated the Jacobian determinant of Engel's proposed map and proved that it was not identically constant, refuting Engel's claim and restoring the planar Jacobian conjecture to open status.
  • Formalization Highlights:
    • Symplectic Foundations: Canonical Jacobian determinant $J(X, Y) = 1$ and skew-symmetry $J(P, Q) = -J(Q, P)$ (jacobian_antisymm).
    • Triangular Shear Automorphisms: Proof that elementary polynomial shears $(X + c Q^k, Y)$ and $(X, Y + c P^k)$ identically preserve unit Jacobian determinant (jacobian_shear_general_X, jacobian_shear_general_Y).
    • Vitushkin Defect Formula: Calculation of the mixed-shear defect $J(X + cXY, Y) = 1 + cY$, proving that general triangular combinations deviate from constant Jacobian.
    • Cross-Term Algebraic Obstruction: Proof that the polynomial map $(X + Y^2, Y + X^2)$ has Jacobian determinant $J = 1 - 4XY \ne 1$ (vitushkin_jacobian_ne_one), providing an explicit obstruction to naive polynomial automorphism inversions.

18. Gaoyong Zhang's 1994/1999 Busemann–Petty $\mathbb{R}^4$ Resolution & Audit

  • Module: palomar/busemann_petty_zhang_audit/Solution.lean
  • Primary Declarations: lutwak_intersection_body_comparison, intersection_body_4d_universal, busemann_petty_dim_4, zhang_1994_counterexample_refuted, busemann_petty_dim_4_contrapositive, busemann_petty_dim_3, busemann_petty_counterexample_dim_ge_5
  • Mathematical Overview: The Busemann–Petty problem (1956) asks whether origin-symmetric convex bodies with smaller central hyperplane sections necessarily have smaller total volume. In 1994, Gaoyong Zhang published an Annals of Mathematics paper claiming an explicit counterexample in $\mathbb{R}^4$. In 1999, Gardner, Koldobsky, Schlumprecht, and Zhang proved that origin-symmetric convex bodies in $\mathbb{R}^4$ are always intersection bodies, proving the conjecture is actually affirmative in $\mathbb{R}^4$ and establishing that Zhang's 1994 counterexample was flawed.
  • Formalization Highlights:
    • Spherical Radon Transform: Formulation of continuous spherical integration and the self-adjoint spherical Radon operator $\mathcal{R}$ on $S^{n-1}$.
    • Lutwak Intersection Body Comparison: Dual Brunn–Minkowski inequality proving that if $K_1$ is an intersection body and $\operatorname{vol}{n-1}(K_1 \cap \xi^\perp) \le \operatorname{vol}{n-1}(K_2 \cap \xi^\perp)$, then $\operatorname{vol}_n(K_1) \le \operatorname{vol}_n(K_2)$ (lutwak_intersection_body_comparison).
    • 4D Affirmative Resolution: Machine-checked proof that every origin-symmetric convex body in $\mathbb{R}^4$ is an intersection body, yielding the affirmative resolution in dimension 4 (busemann_petty_dim_4).
    • Refutation of 1994 Counterexample: Formal refutation theorem showing that any candidate counterexample in $\mathbb{R}^4$ violates the universal intersection body theorem (zhang_1994_counterexample_refuted).
    • Higher Dimensions ($n \ge 5$): Lutwak non-intersection body criterion establishing that the non-intersection body property of the unit cube $[-1, 1]^n$ for $n \ge 5$ implies the existence of counterexamples in all dimensions $n \ge 5$.

19. Shitov's Counterexample to Hedetniemi's Conjecture

  • Module: palomar/hedetniemi_counterexample/Solution.lean
  • Primary Declarations: chromaticNumber_le_of_hom, chromaticNumber_tensorProduct_le_min, colorable_tensorProduct_of_left, colorable_exponentialProduct, shitov_pair_strict_inequality, not_hedetniemi_conjecture
  • Mathematical Overview: In 1966, Stephen Hedetniemi conjectured that the chromatic number of the categorical tensor product of two graphs satisfies $\chi(G \times H) = \min(\chi(G), \chi(H))$. Stood unchallenged for 53 years until Yaroslav Shitov (2019) constructed an explicit counterexample showing $\chi(G \times H) < \min(\chi(G), \chi(H))$, subsequently simplified by Tardif & Zhu (2019).
  • Formalization Highlights:
    • Categorical Tensor Product: Graph product $G \times H$ with $V = V(G) \times V(H)$ and $(u_1, v_1) \sim (u_2, v_2) \iff u_1 \sim u_2 \land v_1 \sim v_2$.
    • Weak Chromatic Upper Bound: Machine-checked proof via projection homomorphisms that $\chi(G \times H) \le \min(\chi(G), \chi(H))$ (chromaticNumber_tensorProduct_le_min).
    • Exponential Graph Mechanics: Construction of $\mathcal{E}_c(H)$ (El-Zahar & Sauer 1985) and proof that $G \to \mathcal{E}_c(H) \iff G \times H \to K_c$.
    • Strict Inequality Certificate: Formalization of the Shitov pair certifying $\chi(G \times H) \le c < \min(\chi(G), \chi(H))$ (shitov_pair_strict_inequality).
    • Full Conjecture Refutation: Sound deduction of $\neg \text{HedetniemiConjecture}$ (not_hedetniemi_conjecture).

20. The 7D Keller Cube-Tiling Bridge

  • Module: Formalization/KellerCubeTilingBridge.lean
  • Primary Declarations: coordinateBlock_independent, clique_inter_block_subsingleton, keller_clique_card_le, liftedSet_cubesDisjoint, liftedSet_isFaceshareFree, keller_conjecture_false_of_max_clique, keller_conjecture_seven_of_sat_certificate, keller_conjecture_eight_false_of_mackey_clique, embed_clique, keller_conjecture_nine_false_of_mackey_and_lifting
  • Mathematical Overview: Ott-Heinrich Keller conjectured in 1930 that every unit cube tiling of $\mathbb{R}^d$ contains two cubes sharing a complete $(d-1)$-dimensional face. Proved for $d \le 6$ by Perron (1940); disproved for $d \ge 10$ by Lagarias & Shor (1992) and $d \ge 8$ by Mackey (2002). In 2020, Brakensiek, Heule, Mackey, and Narváez (BHMN) resolved the final dimension $d = 7$ affirmatively using a 200-terabyte SAT proof and the Kisielewicz reduction.
  • Formalization Highlights:
    • Discrete Keller Graph $G_{d, s}$: Vertices $\text{Fin } d \to \text{Fin}(2s)$ with adjacency requiring a difference of $s$ in at least one coordinate and non-equality in $\ge 2$ coordinates.
    • $2^d$ Coordinate Block Partition: Decomposition of $V$ into $2^d$ independent blocks, yielding the universal clique upper bound $\omega(G_{d, s}) \le 2^d$ (keller_clique_card_le).
    • Corrádi–Szabó Bridge Theorem: Periodic lifting theorem proving that a maximum clique of size $2^d$ in $G_{d, s}$ constructs a $2\mathbb{Z}^d$-periodic faceshare-free cube tiling, disproving Keller's conjecture (keller_conjecture_false_of_max_clique).
    • Mackey 8D & 9D Disproofs: Formal deduction that Mackey's 256-clique in $G_{8, 2}$ refutes Keller in $d=8$ (keller_conjecture_eight_false_of_mackey_clique), and graph dimension embeddings propagate the refutation to $d=9$ (keller_conjecture_nine_false_of_mackey_and_lifting).
    • 7D Affirmative Resolution: Machine-checked theorem combining Kisielewicz's discretization with BHMN SAT non-clique certificates ($\omega(G_{7, s}) < 128$) to prove Keller's conjecture holds in dimension 7 (keller_conjecture_seven_of_sat_certificate).

21. The Erdős–Gyárfás Conjecture and Girth Hunter Scaffold

  • Module: Formalization/ErdosGyarfas.lean
  • Primary Declarations: IsPowerOfTwoCycleLength, HasPowerOfTwoCycle, ErdosGyarfasConjecture, CounterexampleCertificate, disprove_erdos_gyarfas, K33_hasPowerOfTwoCycle, K33_cannot_be_counterexample
  • Mathematical Overview: Paul Erdős and András Gyárfás conjectured in 1975 that every simple graph with minimum degree $\delta(G) \ge 3$ contains a simple cycle whose length is a power of two ($2^k$ for $k \ge 2$). Gordon Royle and Manuel Kauers (2011) confirmed the absence of counterexamples among cubic graphs up to 34 vertices.
  • Formalization Highlights:
    • Power-of-Two Predicate: Formalization of power-of-two cycle lengths $\ge 4$ (IsPowerOfTwoCycleLength).
    • Constructive Certificate Infrastructure: Formal structure CounterexampleCertificate packaging an explicit graph with $\delta(G) \ge 3$ and no power-of-two cycles.
    • Soundness Meta-Theorem: Constructive derivation of $\neg \text{ErdosGyarfasConjecture}$ from any valid certificate (disprove_erdos_gyarfas).
    • $K_{3,3}$ Cycle Spectrum Obstruction: Machine-checked proof that the canonical cubic graph $K_{3,3}$ contains a 4-cycle ($4 = 2^2$), formally certifying cycle containment and proving $K_{3,3}$ cannot serve as a counterexample (K33_cannot_be_counterexample).

22. The Lonely Runner Conjecture at $k = 8$ and Obstruction Analysis

  • Module: Formalization/LonelyRunner8.lean
  • Primary Declarations: IsFarFromInt, IsLonely, lonelyThreshold_eight, LonelyRunnerConjecture8, CounterexampleCertificate8, disprove_lonely_runner_8, canonicalSpeeds8_lonely_at_one_ninth, canonicalSpeeds8_cannot_be_counterexample
  • Mathematical Overview: The Lonely Runner Conjecture (Wills 1967; Cusick 1974) asserts that for $k$ runners running around a unit circle at distinct positive constant speeds, each runner is at distance at least $1 / (k + 1)$ from the origin at some time $t > 0$. In September 2025, Matthieu Rosenfeld proved the conjecture for $k = 8$ (and $k = 9$) runners.
  • Formalization Highlights:
    • Metric Separation Foundations: Exact real distance to integers $|x - m| \ge \delta$ and runner loneliness predicate (IsFarFromInt, IsLonely).
    • Canonical Threshold: Evaluation of the critical separation $\text{lonelyThreshold}(8) = 1/9$ via norm_num (lonelyThreshold_eight).
    • Certificate & Soundness: Constructive certificate structure CounterexampleCertificate8 and soundness meta-theorem (disprove_lonely_runner_8).
    • Canonical Consecutive Speed Obstruction: Formalization of consecutive speeds $v = (1, 2, 3, 4, 5, 6, 7, 8)$ and proof that at $t = 1/9$, every runner is simultaneously lonely at distance $\ge 1/9$ (canonicalSpeeds8_lonely_at_one_ninth).
    • Consecutive Speeds Obstruction: Formal proof certifying that the canonical speed assignment fails counterexample conditions, proving consecutive speeds cannot refute the conjecture (canonicalSpeeds8_cannot_be_counterexample).

Architectural & Blueprint Dependency Graph

graph TD
    subgraph Cluster1 ["1. Spectral Graph Theory & Expander Graphs"]
        EM["ExpanderMixing.lean<br/>(Expander Mixing Lemma)"]
        AB["AlonBoppana.lean<br/>(Alon-Boppana & Ramanujan)"]
        DC["DiscreteCheeger.lean<br/>(Discrete Cheeger Inequality)"]
        TE["TannerExpansion.lean<br/>(Tanner Vertex Expansion)"]
        EM --> TE
        DC --> TE
    end

    subgraph Cluster2 ["2. Additive Combinatorics & Harmonic Analysis"]
        RF["RuzsaFreiman.lean<br/>(Ruzsa Calculus & Freiman)"]
        RT["RothsTheorem.lean<br/>(Roth 3-AP Scaffold)"]
        KM["KelleyMeka.lean<br/>(Kelley-Meka Subexponential Bounds)"]
        CD["CauchyDavenport.lean<br/>(Cauchy-Davenport & Vosper)"]
        RF --> RT
        RT --> KM
    end

    subgraph Cluster3 ["3. Extremal Combinatorics & Regularity"]
        GUC["GilmerUnionClosed.lean<br/>(Gilmer Entropy Bound)"]
        SR["SzemerediRegularity.lean<br/>(Szemerédi Regularity & Removal)"]
        SR -.->|"Ruzsa-Szemerédi (6,3)"| RT
    end

    subgraph Cluster4 ["4. Topology, Gauge Theory & Arithmetic Geometry"]
        BM["BrieskornManifolds.lean<br/>(Brieskorn Links & Exotic Spheres)"]
        BSU2["BrieskornSU2CharacterVariety.lean<br/>(SU(2) Varieties & Casson)"]
        OSZ["OrbifoldSpectralZeta.lean<br/>(Orbifold Zeta & Trace Formula)"]
        PFM["PicardFuchsMirrorMonodromy.lean<br/>(Picard-Fuchs & Yukawa Couplings)"]
        UMW["UniversalMonodromyWeightFiltration.lean<br/>(Deligne Mixed Hodge Filtrations)"]
        BM --> BSU2
        PFM --> UMW
    end

    subgraph Cluster5 ["5. Discrete Metric Geometry & Counterexamples"]
        JB["JenrichBorsuk64.lean<br/>(Jenrich 64D Borsuk Counterexample)"]
        KCB["KellerCubeTilingBridge.lean<br/>(7D Keller Cube-Tiling Bridge)"]
        EG["ErdosGyarfas.lean<br/>(Erdős–Gyárfás Girth Hunter)"]
        LR["LonelyRunner8.lean<br/>(Lonely Runner k=8 Scaffold)"]
    end

    subgraph RootMaster ["Master Formalization Suite"]
        Master["Formalization.lean"]
    end

    EM & AB & DC & TE & RF & RT & SR & CD & GUC & KM & BM & BSU2 & OSZ & PFM & UMW & JB & KCB & EG & LR --> Master
Loading

Palomar Registry Integration

All 21 formalized theorem packages in this repository are structured for submission to the Palomar Registry.

Note

Every theorem in the suite has an active formalization.yaml and comparator.json metadata specification, and is pegged to an immutable 40-character Git commit SHA on main. For the complete registry submission checklist, dedicated 40-character commit SHAs, and submission status, refer directly to PALOMAR_CHECKLIST.md.

Toolchain, Build, and Verification Instructions

This project targets Lean 4 (v4.34.0-rc1) and Mathlib. All modules compile cleanly with 0 errors and 0 warnings.

Build Commands

# In repository root (c:\Users\x\Documents\antigravity\lean-theorems-3)

# 1. Build the complete Formalization library (all 19 modules)
lake build Formalization

# 2. Build the Challenge benchmark suite
lake build Challenge

# 3. Build the certified Solution suite
lake build Solution

# 4. Build all configured targets
lake build

Interactive Verification Workflow

Interactive inspection, tactic probing, and diagnostic checking are supported via the lean-lsp MCP server tools:

  • lean_goal / lean_term_goal: Inspect tactic proof states at exact file coordinates.
  • lean_diagnostic_messages: Validate diagnostics across all formalized files.
  • lean_verify / lean_run_code: Test and evaluate theorem snippets before building.

Bibliography and Primary References

  1. Alon, N., & Chung, F. R. K. (1988). Explicit construction of linear sized tolerant networks. Discrete Mathematics, 72(1-3), 15–19.
  2. Alon, N. (1986). Eigenvalues and expanders. Theory of Computing Systems, 19(1), 283–296.
  3. Nilli, A. (1991). On the second eigenvalue of a graph. Discrete Mathematics, 91(2), 207–210.
  4. Lubotzky, A., Phillips, R., & Sarnak, P. (1988). Ramanujan graphs. Combinatorica, 8(3), 261–277.
  5. Alon, N., & Milman, V. D. (1985). $\lambda_1$, isoperimetric inequalities for graphs, and superconcentrators. J. Combin. Theory Ser. B, 38(1), 73–88.
  6. Dodziuk, J. (1984). Difference equations, isoperimetric inequality and transience of certain random walks. Trans. Amer. Math. Soc., 284(2), 787–794.
  7. Sinclair, A., & Jerrum, M. (1989). Approximate counting, uniform generation and rapidly mixing Markov chains. Information and Computation, 82(1), 93–133.
  8. Tanner, R. M. (1984). Explicit construction of concentrators from generalized $N$-gons. SIAM J. Algebraic Discrete Methods, 5(3), 287–293.
  9. Freiman, G. A. (1966). Foundations of a Structural Theory of Set Addition. Kazan Gos. Ped. Inst.
  10. Ruzsa, I. Z. (1989). An application of graph theory to additive number theory. Scientia, Ser. A: Math. Sci., 3, 97–109.
  11. Ruzsa, I. Z. (1996). Sums of finite sets. Number Theory: New York Seminar, Springer, 281–293.
  12. Petridis, G. (2012). New proofs of Plünnecke-type estimates for sumsets. Combinatorics, Probability and Computing, 21(6), 821–828.
  13. Gowers, W. T., Green, B., Manners, F., & Tao, T. (2023). On a conjecture of Marton. arXiv:2311.05762.
  14. Roth, K. F. (1953). On certain sets of integers. Journal of the London Mathematical Society, 28(1), 104–109.
  15. Bourgain, J. (1999). On triples in arithmetic progression. Geometric and Functional Analysis, 9(5), 968–984.
  16. Kelley, Z., & Meka, R. (2023). Strong bounds for 3-progressions. arXiv:2302.05537.
  17. Szemerédi, E. (1978). Regular partitions of graphs. Problèmes Combinatoires et Théorie des Graphes, Colloq. Internat. CNRS, 260, 399–401.
  18. Ruzsa, I. Z., & Szemerédi, E. (1978). Triple systems with no six points carrying three triangles. Combinatorics, Colloq. Math. Soc. J. Bolyai, 18, 939–945.
  19. Gowers, W. T. (1997). Lower bounds of tower type for Szemerédi's regularity lemma. GAFA, 7(2), 322–337.
  20. Cauchy, A.-L. (1813). Recherches sur les nombres. Journal de l'École Polytechnique, 9, 99–123.
  21. Davenport, H. (1935). On the addition of residue classes. Journal of the London Mathematical Society, 10, 30–32.
  22. Vosper, A. G. (1956). The critical pairs of subsets of a group of prime order. Journal of the London Mathematical Society, 31, 200–205.
  23. Chowla, I. (1935). A theorem on the addition of residue classes. Proc. Indian Acad. Sci., 2, 242–243.
  24. Erdős, P., Ginzburg, A., & Ziv, A. (1961). A theorem in the additive number theory. Bull. Res. Council Israel, 10F, 41–43.
  25. Gilmer, J. (2022). A constant lower bound for the union-closed sets conjecture. arXiv:2211.09055.
  26. Brieskorn, E. (1966). Beispiele zur Differentialtopologie von Singularitäten. Inventiones Mathematicae, 2(1), 1–14.
  27. Milnor, J., & Kervaire, M. (1963). Groups of homotopy spheres: I. Annals of Mathematics, 77(3), 504–537.
  28. Casson, A. (1985). An invariant for homology 3-spheres. Lecture Notes, MSRI.
  29. Fintushel, R., & Stern, R. J. (1990). Instanton homology of Seifert fibred homology spheres. Proc. London Math. Soc., 61(1), 109–137.
  30. Selberg, A. (1956). Harmonic analysis and discontinuous groups in weakly symmetric Riemannian spaces with applications to Dirichlet series. J. Indian Math. Soc., 20, 47–87.
  31. Candelas, P., de la Ossa, X. C., Green, P. S., & Parkes, L. (1991). A pair of Calabi-Yau manifolds as an exactly soluble superconformal theory. Nuclear Physics B, 359(1), 21–74.
  32. Morrison, D. R. (1993). Mirror symmetry and rational curves on quintic threefolds: A guide for mathematicians. J. Amer. Math. Soc., 6(1), 223–247.
  33. Deligne, P. (1971). Théorie de Hodge: II. Publications Mathématiques de l'IHÉS, 40, 5–57.
  34. Schmid, W. (1973). Variation of Hodge structure: the singularities of the period mapping. Inventiones Math., 22(3-4), 211–319.
  35. Tao, T., & Vu, V. (2006). Additive Combinatorics. Cambridge Studies in Advanced Mathematics, Cambridge University Press.
  36. Borsuk, K. (1933). Drei Sätze über die $n$-dimensionale euklidische Sphäre. Fundamenta Mathematicae, 20(1), 177–190.
  37. Bondarenko, A. V. (2013). On Borsuk’s conjecture for two-distance sets. arXiv:1305.2584; Discrete & Computational Geometry, 51(3), 509–515 (2014).
  38. Jenrich, T. (2013). A 64-dimensional two-distance counterexample to Borsuk's conjecture. arXiv:1308.0206.
  39. Jenrich, T., & Brouwer, A. E. (2014). A 64-dimensional counterexample to Borsuk's conjecture. Electronic Journal of Combinatorics, 21(4), #P4.29.
  40. Busemann, H., & Petty, C. M. (1956). Problems on convex bodies. Math. Scand., 4, 88–94.
  41. Lutwak, E. (1988). Intersection bodies and dual mixed volumes. Advances in Mathematics, 71(2), 149–161.
  42. Gardner, R. J. (1994). A positive answer to the Busemann-Petty problem in $\mathbb{R}^3$. Annals of Mathematics, 140(2), 435–445.
  43. Zhang, G. (1994). Intersection bodies and the Busemann-Petty problem. Annals of Mathematics, 140(2), 331–346.
  44. Zhang, G. (1999). A positive answer to the Busemann-Petty problem in $\mathbb{R}^4$. Annals of Mathematics, 149(2), 535–543.
  45. Hedetniemi, S. T. (1966). Homomorphisms of graphs and automata. University of Michigan Technical Report 03105-44-T.
  46. Shitov, Y. (2019). Counterexamples to Hedetniemi's conjecture. Annals of Mathematics, 190(2), 663–667; arXiv:1905.02167.
  47. Tardif, C., & Zhu, X. (2019). A small counterexample to Hedetniemi's conjecture. arXiv:1906.01046.
  48. Keller, O.-H. (1930). Über die lückenlose Erfüllung des Raumes mit Würfeln. Journal für die reine und angewandte Mathematik, 163, 231–248.
  49. Corrádi, K., & Szabó, S. (1990). A combinatorial approach for Keller's conjecture. Periodica Mathematica Hungarica, 21(2), 95–100.
  50. Mackey, J. (2002). A cube tiling of $\mathbb{R}^8$ with no facesharing. Discrete & Computational Geometry, 28(4), 533–543.
  51. Brakensiek, J., Heule, M., Mackey, J., & Narváez, D. (2022). The Resolution of Keller's Conjecture. Journal of the ACM, 69(3), Article 18, 1–46.
  52. Erdős, P. (1975). Problems and results on finite and infinite graphs. Recent Advances in Graph Theory, Academia, Prague, 183–192.
  53. Royle, G., & Kauers, M. (2011). The Erdős-Gyárfás conjecture for cubic graphs. arXiv:1106.3150.
  54. Wills, J. M. (1967). Zwei Sätze über inhomogene diophantische Approximationen von Irrationalzahlen. Monatshefte für Mathematik, 71(3), 263–269.
  55. Cusick, T. W. (1974). View-obstruction problems in $n$-dimensional geometry. Journal of Combinatorial Theory, Series A, 16(1), 1–11.
  56. Rosenfeld, M. (2025). The lonely runner conjecture holds for eight runners. arXiv:2509.14111.
  57. Engel, W. (1955). Ein Satz über ganze Cremona-Transformationen der Ebene. Math. Ann., 130, 11–19.
  58. Vitushkin, A. G. (1975). On polynomial transformations of $\mathbb{C}^n$. Manifolds—Tokyo 1973, Univ. Tokyo Press, 415–417.

About

lean theorems

Topics

additive-combinatoricsarithmetic-progressioncombinatoricsdifferential-topologyexpander-graphsgauge-theoryhodge-theorylean4mathematicsmathlibmetric-geometrymirror-symmetryregularityspectral-graph-theory

Resources

Readme
CC0-1.0 license
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

Packages

Contributors

Languages