The Mathlib module lean/FrcMathlib/Theme/YangMills.lean of the framework's chart theme, the readings against the continuum that the master's rows L1, L3, L8 and P1 stake (ledger migration, task LM30): 4 theorems (1 definitions): 0 with no axioms, 1 at tier 1 (propext, Quot.sound), 3 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (violet, Mathlib; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import Mathlib2import FrcMathlib.Theme.Hadrons34/-!5# FrcMathlib.Theme.YangMills — the yangmills theme's readings on Mathlib (46-yangmills, 8 November 2026)67The two clauses of 46-yangmills that Mathlib states beyond the core without leaving the integers and the rationals: the8Faulhaber identity of the scalar loop for every `N` (46:C13; the core proves it to `N = 400` and as residues on the shell9`173`), and the radial ratio's confrontations as rational brackets (46:P3) with the Airy ratio of the hadrons theme. The10chart clauses of the paper on the reals — the running coupling, the Herbst comparison, the plaquette channel, the operator11family — live in the chart theme's `FrcMathlib/Theme/Gauge.lean` (gate G09: a Mathlib theme outside the chart holds no12reals). The exact content of the paper is the core's (`FrcCore/Theme/YangMills.lean`, no axioms). Classical (tier 2).13-/1415namespace FRC.YangMillsML1617open Finset1819/-! ## 46:C13 — the Faulhaber identity for every `N` -/2021/-- The midpoint sum of the scalar loop, `Σ_{k<N} (N − 2k − 1)²`, as a sum over `Finset.range`. -/22
def sq (N : ℕ) : ℤ := ∑ k ∈ range N, ((N : ℤ) - 2 * (k : ℤ) - 1) ^ 22324/-- The two-step recursion: the terms of `sq (N + 2)` are `(N + 1)²` at `k = 0`, the terms of `sq N` shifted by one, and25`(N + 1)²` at `k = N + 1`. -/26
lemma sq_succ_succ (N : ℕ) : sq (N + 2) = sq N + 2 * ((N : ℤ) + 1) ^ 2 := by27 unfold sq28 rw [sum_range_succ, sum_range_succ']29 push_cast30 have h : ∀ k ∈ range N, ((N : ℤ) + 2 - 2 * ((k : ℤ) + 1) - 1) ^ 2 = ((N : ℤ) - 2 * (k : ℤ) - 1) ^ 2 := by31 intro k _; ring32 rw [sum_congr rfl h]33 ring3435/-- 46:C13 — the Faulhaber identity for every `N`: `3 Σ_{k<N} (N − 2k − 1)² = N (N² − 1)`. -/36theorem faulhaber_third_all (N : ℕ) : 3 * sq N = (N : ℤ) * ((N : ℤ) ^ 2 - 1) := by37 induction N using Nat.twoStepInduction with38 | zero => simp [sq]39 | one => simp [sq]40 | more N ih0 _ =>41 rw [sq_succ_succ, mul_add, ih0]42 push_cast43 ring4445/-- 46:C4 — the Casimir rationals from the frame's torus exponents, for every exponent pair: the second moment of the adjoint's46exponents (the six differences of the fundamental's `(a, b, −a−b)`) is six times the fundamental's, `T_A/T_F = 6`, hence47`C_A/C_F = 9/4` with no lift; the core decides it on the Subjects `13`, `173`, `1549`. -/48theorem casimir_exponents_all (a b : ℤ) :49 2 * ((a - b) ^ 2 + (2 * a + b) ^ 2 + (a + 2 * b) ^ 2) = 6 * (a ^ 2 + b ^ 2 + (a + b) ^ 2) := by50 ring5152/-! ## 46:P3 — the radial ratio's confrontations -/5354/-- 46:P3 [chart] — **the radial ratio against the lattice**, as rational brackets. With the chart's reading55`E₁/E₀ = 1.4915` of the operator form (`chart_yangmills.wrap_spectrum`, the same on every `a`, `ϰ`): it lies within half a56standard deviation of the 1999 ratio `1.544(112)` (`6.50(44)/4.21(11)`, Morningstar–Peardon); the 2020 ratio `1.720(16)`57(`5.855(41)/3.405(21)`, Athenodorou–Teper; its error `0.016` takes the two masses as uncorrelated) excludes it by more than `14`58standard deviations, and by more than `10` of the largest error any correlation allows, the two propagated terms added59(`41/3405 + 5855·21/3405²`, the anticorrelated case); the nonrelativistic Airy ratio `4.08795/2.33811`60(`FRC.HadronsML.airy_ratio`, in `(1.748, 1.7485)`) lies within two of the quoted error; the nucleon's `1440/939` lies within61`3 %` of the reading. -/62theorem radial_ratio_confrontation (r : ℚ) (hr : r = 1.4915) :63 |r - 1.544| < 0.5 * 0.112 ∧ 14 * 0.016 < 1.720 - r ∧ 10 * ((41 : ℚ) / 3405 + 5855 * 21 / 3405 ^ 2) < 5855 / 3405 - r ∧64 |(4.08795 : ℚ) / 2.33811 - 1.720| < 2 * 0.016 ∧65 (1.748 : ℚ) < 4.08795 / 2.33811 ∧ |(1440 : ℚ) / 939 - r| < 0.03 * r := by66 subst hr67 have h := FRC.HadronsML.airy_ratio68 refine ⟨by rw [abs_lt]; constructor <;> norm_num, by norm_num, by norm_num, by rw [abs_lt]; constructor <;> linarith [h.1, h.2], h.1, ?_⟩69 rw [abs_lt]; constructor <;> norm_num7071end FRC.YangMillsML72