YangMills.lean — FrcMathlib

1import Mathlib2import FrcMathlib.Theme.YangMills3import FrcMathlib.Theme.Gauge4import FrcMathlib.Keys.Chart5import FrcMathlib.Keys.Yangmills67/-!8# 46-yangmills — the readings on Mathlib (8 November 2026)910The paper module of *Yang–Mills and the Mass Gap over Finite Holographic Substrate* (tree `46-yangmills-20261107`) on Mathlib:11every declaration is an alias under the paper's name of a theorem of `FRC.YangMillsML` — in the yangmills theme's12`FrcMathlib/Theme/YangMills.lean` the Casimirs of C4 from the torus exponents for every exponent pair, the Faulhaber identity of C13 for13every `N` and the radial ratio's confrontations of P3 as rational brackets, and in the chart theme's `FrcMathlib/Theme/Gauge.lean` the chart clauses of C10, C11, C12, C21 and P2 over the14reals (the two-loop run as the exact solution of its equation, the one-loop law, the Herbst comparison and the couplings at15the chart's fixed points, the plaquette channel at the chart's cells, the operator family's values, the gap at the classical `π`). Classical (tier 2). The finite16content of the paper is the core's (`FrcCore/Theme/YangMills.lean`, no axioms); the predicates `p46NNN` at the end are17generated by `make_predicates.py`, aliases of the keys of the key files.18-/1920namespace FRC.YangMills2122/-! ## Old names — every declaration of this module is an alias of the themes' (`FRC.YangMillsML`, `Theme/YangMills.lean` and23the chart theme's `Theme/Gauge.lean`) under the paper's name, so that the key files prove the predicates from the themes -/2425open Real26open FRC.YangMillsML (F P3 P5 P7 ratio cellU)2728/-- 46:C4 — `YangMillsML.casimir_exponents_all`: the Casimirs from the frame's torus exponents for every exponent pair, `2((a−b)² + (2a+b)² + (a+2b)²) = 6(a² + b² + (a+b)²)`, so `T_A/T_F = 6` and `C_A/C_F = 9/4` with no lift; the core decides it on the three Subjects. -/29theorem casimir_exponents_all (a b : ℤ) :30    2 * ((a - b) ^ 2 + (2 * a + b) ^ 2 + (a + 2 * b) ^ 2) = 6 * (a ^ 2 + b ^ 2 + (a + b) ^ 2) :=31  FRC.YangMillsML.casimir_exponents_all a b3233/-- 46:C13 — `YangMillsML.faulhaber_third_all`: the Faulhaber identity `3 Σ_{k<N} (N − 2k − 1)² = N (N² − 1)` for every `N`; the core proves it for `N < 400` and as residues on the shell `173`. -/34theorem faulhaber_third_all (N : ℕ) : 3 * FRC.YangMillsML.sq N = (N : ℤ) * ((N : ℤ) ^ 2 - 1) :=35  FRC.YangMillsML.faulhaber_third_all N3637/-- 46:P2 — `YangMillsML.two_loop_tau`: the two-loop run from `α_s(M_Z) = 0.1180` to `m_τ` as the exact solution of the two-loop equation: `α_s(m_b)` in `(0.2235, 0.2237)`, `α_s(m_τ)` in `(0.3132, 0.3134)`. -/38theorem two_loop_tau (a₀ a_b a_τ : ℝ) (h₀ : a₀ = 0.1180 / (4 * π)) (hb : 0 < a_b) (hτ : 0 < a_τ)39    (hFb : F (23 / 3) (116 / 3) a_b = F (23 / 3) (116 / 3) a₀ + log (4.18 / 91.1876))40    (hFτ : F (25 / 3) (154 / 3) a_τ = F (25 / 3) (154 / 3) a_b + log (1.77686 / 4.18)) :41    (0.2235 : ℝ) < 4 * π * a_b ∧ 4 * π * a_b < 0.2237 ∧ (0.3132 : ℝ) < 4 * π * a_τ ∧ 4 * π * a_τ < 0.3134 :=42  FRC.YangMillsML.two_loop_tau a₀ a_b a_τ h₀ hb hτ hFb hFτ4344/-- 46:P2 — `YangMillsML.one_loop_tau`: the one-loop law over `ℝ`: `α_s(m_τ)` in `(0.2785, 0.2795)`, `2.2` standard deviations below `0.312(15)`. -/45theorem one_loop_tau (α : ℝ)46    (h : 1 / α = 1 / 0.1180 + (23 / 3) / (2 * π) * log (4.18 / 91.1876) + (25 / 3) / (2 * π) * log (1.77686 / 4.18)) :47    (0.2785 : ℝ) < α ∧ α < 0.2795 ∧ (2.1 : ℝ) < (0.312 - 0.279) / 0.015 ∧ ((0.312 : ℝ) - 0.279) / 0.015 < 2.3 :=48  FRC.YangMillsML.one_loop_tau α h4950/-- 46:C10 — `YangMillsML.herbst_real`: the declared coupling `2π/(9 ln 2)` in `(1.0065, 1.0075)`, `C = 3α_s` in `(3.015, 3.025)` above `4/π` above `2/π`. -/51theorem herbst_real : (1.0065 : ℝ) < 2 * π / (9 * log 2) ∧ 2 * π / (9 * log 2) < 1.0075 ∧52    (3.015 : ℝ) < 3 * (2 * π / (9 * log 2)) ∧ 3 * (2 * π / (9 * log 2)) < 3.025 ∧53    4 / π < 3 * (2 * π / (9 * log 2)) ∧ 2 / π < 4 / π ∧ 6 * log 2 < π ^ 2 :=54  FRC.YangMillsML.herbst_real5556/-- 46:C10 — `YangMillsML.fixed_point_couplings`: the couplings `2π/(3 ln 2E)` at the chart's fixed points `E = 3.541`, `3.085`, `2.611`, all below `4/π`, the last within `0.5 %`. -/57theorem fixed_point_couplings :58    (1.0698 : ℝ) < 2 * π / (3 * log (2 * 3.541)) ∧ 2 * π / (3 * log (2 * 3.541)) < (1.07 : ℝ) ∧59    (1.1508 : ℝ) < 2 * π / (3 * log (2 * 3.085)) ∧ 2 * π / (3 * log (2 * 3.085)) < (1.1511 : ℝ) ∧60    (1.267 : ℝ) < 2 * π / (3 * log (2 * 2.611)) ∧ 2 * π / (3 * log (2 * 2.611)) < (1.2672 : ℝ) ∧61    2 * π / (3 * log (2 * 2.611)) < 4 / π ∧ 0.995 * (4 / π) < 2 * π / (3 * log (2 * 2.611)) :=62  FRC.YangMillsML.fixed_point_couplings6364/-- 46:C11 — `YangMillsML.plaquette_cells_values`: the plaquette channel's `m/√σ` at the chart's cells over the reals, the cells' stiffness from `π` and `ln 2`, `u` the sum of the computed terms of `c₃` through `ϑ⁷`: `6.9`, `6.2`, `5.6`, `5.1` at `n = 9, 8, 7, 6` with the orders within `1 %`, the orders' disagreement at `n = 3` and at `n = 2`, and `2.95`, `0.45`, `2.82` at channel unity, where `u = 23/54`. -/65theorem plaquette_cells_values :66    (cellU 0 = 23 / 54) ∧67    ((6.93 : ℝ) ≤ ratio (cellU 9) (P3 (cellU 9)) ∧ ratio (cellU 9) (P3 (cellU 9)) ≤ (6.94 : ℝ) ∧ (6.93 : ℝ) ≤ ratio (cellU 9) (P5 (cellU 9)) ∧ ratio (cellU 9) (P5 (cellU 9)) ≤ (6.94 : ℝ) ∧ (6.93 : ℝ) ≤ ratio (cellU 9) (P7 (cellU 9)) ∧ ratio (cellU 9) (P7 (cellU 9)) ≤ (6.94 : ℝ)) ∧68    ((6.16 : ℝ) ≤ ratio (cellU 8) (P3 (cellU 8)) ∧ ratio (cellU 8) (P3 (cellU 8)) ≤ (6.17 : ℝ) ∧ (6.16 : ℝ) ≤ ratio (cellU 8) (P5 (cellU 8)) ∧ ratio (cellU 8) (P5 (cellU 8)) ≤ (6.17 : ℝ) ∧ (6.16 : ℝ) ≤ ratio (cellU 8) (P7 (cellU 8)) ∧ ratio (cellU 8) (P7 (cellU 8)) ≤ (6.17 : ℝ)) ∧69    ((5.59 : ℝ) ≤ ratio (cellU 7) (P3 (cellU 7)) ∧ ratio (cellU 7) (P3 (cellU 7)) ≤ (5.6 : ℝ) ∧ (5.58 : ℝ) ≤ ratio (cellU 7) (P5 (cellU 7)) ∧ ratio (cellU 7) (P5 (cellU 7)) ≤ (5.59 : ℝ) ∧ (5.58 : ℝ) ≤ ratio (cellU 7) (P7 (cellU 7)) ∧ ratio (cellU 7) (P7 (cellU 7)) ≤ (5.59 : ℝ)) ∧70    ((5.11 : ℝ) ≤ ratio (cellU 6) (P3 (cellU 6)) ∧ ratio (cellU 6) (P3 (cellU 6)) ≤ (5.12 : ℝ) ∧ (5.09 : ℝ) ≤ ratio (cellU 6) (P5 (cellU 6)) ∧ ratio (cellU 6) (P5 (cellU 6)) ≤ (5.1 : ℝ) ∧ (5.1 : ℝ) ≤ ratio (cellU 6) (P7 (cellU 6)) ∧ ratio (cellU 6) (P7 (cellU 6)) ≤ (5.11 : ℝ)) ∧71    ((4.32 : ℝ) ≤ ratio (cellU 4) (P3 (cellU 4)) ∧ ratio (cellU 4) (P3 (cellU 4)) ≤ (4.33 : ℝ) ∧ (4.16 : ℝ) ≤ ratio (cellU 4) (P5 (cellU 4)) ∧ ratio (cellU 4) (P5 (cellU 4)) ≤ (4.17 : ℝ) ∧ (4.22 : ℝ) ≤ ratio (cellU 4) (P7 (cellU 4)) ∧ ratio (cellU 4) (P7 (cellU 4)) ≤ (4.23 : ℝ)) ∧72    ((3.97 : ℝ) ≤ ratio (cellU 3) (P3 (cellU 3)) ∧ ratio (cellU 3) (P3 (cellU 3)) ≤ (3.98 : ℝ) ∧ (3.6 : ℝ) ≤ ratio (cellU 3) (P5 (cellU 3)) ∧ ratio (cellU 3) (P5 (cellU 3)) ≤ (3.61 : ℝ) ∧ (3.78 : ℝ) ≤ ratio (cellU 3) (P7 (cellU 3)) ∧ ratio (cellU 3) (P7 (cellU 3)) ≤ (3.79 : ℝ)) ∧73    ((3.64 : ℝ) ≤ ratio (cellU 2) (P3 (cellU 2)) ∧ ratio (cellU 2) (P3 (cellU 2)) ≤ (3.65 : ℝ) ∧ (2.87 : ℝ) ≤ ratio (cellU 2) (P5 (cellU 2)) ∧ ratio (cellU 2) (P5 (cellU 2)) ≤ (2.88 : ℝ) ∧ (3.35 : ℝ) ≤ ratio (cellU 2) (P7 (cellU 2)) ∧ ratio (cellU 2) (P7 (cellU 2)) ≤ (3.37 : ℝ)) ∧74    ((2.95 : ℝ) ≤ ratio (cellU 0) (P3 (cellU 0)) ∧ ratio (cellU 0) (P3 (cellU 0)) ≤ (2.96 : ℝ) ∧ (0.44 : ℝ) ≤ ratio (cellU 0) (P5 (cellU 0)) ∧ ratio (cellU 0) (P5 (cellU 0)) ≤ (0.45 : ℝ) ∧ (2.81 : ℝ) ≤ ratio (cellU 0) (P7 (cellU 0)) ∧ ratio (cellU 0) (P7 (cellU 0)) ≤ (2.82 : ℝ)) ∧75    (|ratio (cellU 9) (P3 (cellU 9)) - ratio (cellU 9) (P7 (cellU 9))| < 0.01 * ratio (cellU 9) (P7 (cellU 9)) ∧ |ratio (cellU 9) (P5 (cellU 9)) - ratio (cellU 9) (P7 (cellU 9))| < 0.01 * ratio (cellU 9) (P7 (cellU 9))) ∧76    (|ratio (cellU 8) (P3 (cellU 8)) - ratio (cellU 8) (P7 (cellU 8))| < 0.01 * ratio (cellU 8) (P7 (cellU 8)) ∧ |ratio (cellU 8) (P5 (cellU 8)) - ratio (cellU 8) (P7 (cellU 8))| < 0.01 * ratio (cellU 8) (P7 (cellU 8))) ∧77    (|ratio (cellU 7) (P3 (cellU 7)) - ratio (cellU 7) (P7 (cellU 7))| < 0.01 * ratio (cellU 7) (P7 (cellU 7)) ∧ |ratio (cellU 7) (P5 (cellU 7)) - ratio (cellU 7) (P7 (cellU 7))| < 0.01 * ratio (cellU 7) (P7 (cellU 7))) ∧78    (|ratio (cellU 6) (P3 (cellU 6)) - ratio (cellU 6) (P7 (cellU 6))| < 0.01 * ratio (cellU 6) (P7 (cellU 6)) ∧ |ratio (cellU 6) (P5 (cellU 6)) - ratio (cellU 6) (P7 (cellU 6))| < 0.01 * ratio (cellU 6) (P7 (cellU 6))) ∧79    ((3.7 : ℝ) < ratio (cellU 4) (P3 (cellU 4)) ∧ (3.7 : ℝ) < ratio (cellU 4) (P5 (cellU 4)) ∧ (3.7 : ℝ) < ratio (cellU 4) (P7 (cellU 4))) ∧80    ((3.4 : ℝ) < ratio (cellU 3) (P5 (cellU 3)) ∧ ratio (cellU 3) (P5 (cellU 3)) < (3.7 : ℝ) ∧ (3.7 : ℝ) < ratio (cellU 3) (P3 (cellU 3)) ∧ (3.7 : ℝ) < ratio (cellU 3) (P7 (cellU 3))) ∧81    ((3.4 : ℝ) < ratio (cellU 2) (P3 (cellU 2)) ∧ ratio (cellU 2) (P3 (cellU 2)) < (3.7 : ℝ) ∧ ratio (cellU 2) (P5 (cellU 2)) < (3.4 : ℝ) ∧ ratio (cellU 2) (P7 (cellU 2)) < (3.4 : ℝ)) :=82  FRC.YangMillsML.plaquette_cells_values8384/-- 46:C21 — `YangMillsML.gap_at_classical_pi`: the gap `1/(2π + 2)` of the transfer tally read at the classical `π`, in `(0.12072, 0.12073)`. -/85theorem gap_at_classical_pi : (0.12072 : ℝ) < 1 / (2 * π + 2) ∧ 1 / (2 * π + 2) < (0.12073 : ℝ) :=86  FRC.YangMillsML.gap_at_classical_pi8788/-- 46:C12 — `YangMillsML.wrap_family_values`: the six family values `√(aϰ) E₀` with `Real.sqrt` from the chart's `E₀ = 2.232`, none inside a determination's error, the nearest `1.7 %` below `3.405`. -/89theorem wrap_family_values (E₀ : ℝ) (hE : E₀ = 2.232) :90    (3.156 : ℝ) < √2 * E₀ ∧ √2 * E₀ < 3.157 ∧ √(9 / 4) * E₀ = 3.348 ∧ √4 * E₀ = 4.464 ∧91    (4.734 : ℝ) < √(9 / 2) * E₀ ∧ √(9 / 2) * E₀ < 4.735 ∧92    E₀ < 3.384 ∧ √2 * E₀ < 3.384 ∧ √(9 / 4) * E₀ < 3.384 ∧ 3.76 < √4 * E₀ ∧ 3.76 < √(9 / 2) * E₀ ∧93    (0.016 : ℝ) < (3.405 - √(9 / 4) * E₀) / 3.405 ∧ (3.405 - √(9 / 4) * E₀) / 3.405 < 0.018 :=94  FRC.YangMillsML.wrap_family_values E₀ hE9596/-- 46:P3 — `YangMillsML.radial_ratio_confrontation`: the radial ratio `1.4915` against `1.544(112)` and `1.720(16)` (by more than `14` of the quoted error, taken as uncorrelated, and by more than `10` of the largest error any correlation allows), the Airy ratio and the nucleon, as rational brackets. -/97theorem radial_ratio_confrontation (r : ℚ) (hr : r = 1.4915) :98    |r - 1.544| < 0.5 * 0.112 ∧ 14 * 0.016 < 1.720 - r ∧ 10 * ((41 : ℚ) / 3405 + 5855 * 21 / 3405 ^ 2) < 5855 / 3405 - r ∧99    |(4.08795 : ℚ) / 2.33811 - 1.720| < 2 * 0.016 ∧100    (1.748 : ℚ) < 4.08795 / 2.33811 ∧ |(1440 : ℚ) / 939 - r| < 0.03 * r :=101  FRC.YangMillsML.radial_ratio_confrontation r hr102103-- Ledger predicates of 46-yangmills (generated by make_predicates.py from docs/46-yangmills/46-yangmills-ledger.json; edit the ledger, not this section)104/-- 46:C4 (p46013) — The Casimir rationals of the unitary frame from its torus exponents (C6): on the fundamental $(a,b,-a-b)$, on the adjoint their differences and two zeros; the second moments are $2$ and $12$ times $a^{2}+ab+b^{2}$, so $T_A/T_F=6$ and, with the chart's normalisation $T_F=\frac12$, $C_F=\frac43$, $C_A=3$, $C_A/C_F=\frac94$; the three-quark singlet's colour factor is $-8$. No lift enters. -/105theorem colour_casimirs : ∀ (a b : ℤ), (2 : ℤ) * ((a - b) ^ (2 : ℕ) + ((2 : ℤ) * a + b) ^ (2 : ℕ) + (a + (2 : ℤ) * b) ^ (2 : ℕ)) = (6 : ℤ) * (a ^ (2 : ℕ) + b ^ (2 : ℕ) + (a + b) ^ (2 : ℕ)) :=106  @FRC.LedgerML.p46013107/-- 46:C10 (p46037) — [chart] The short-range route of the chart fails: with the declared coupling $\alpha_s(\sig)=1.007$ the two-adjoint term has $C=C_A\alpha_s=3.02$, above the Herbst bounds $2/\pi$ and $4/\pi$, so the cutoff cannot be removed; with the coupling run to the bound state's mass, fixed points $3.54$, $3.08$, $2.61$ at $r_c=1$, $\frac12$, $\frac14$ and none found at $\frac18$ (a scan of $149$ energies). -/108theorem short_range_fails : (1.0065 < (2 : ℝ) * Real.pi / ((9 : ℝ) * Real.log (2 : ℝ)) ∧ (2 : ℝ) * Real.pi / ((9 : ℝ) * Real.log (2 : ℝ)) < 1.0075 ∧ 3.015 < (3 : ℝ) * ((2 : ℝ) * Real.pi / ((9 : ℝ) * Real.log (2 : ℝ))) ∧ (3 : ℝ) * ((2 : ℝ) * Real.pi / ((9 : ℝ) * Real.log (2 : ℝ))) < 3.025 ∧ (4 : ℝ) / Real.pi < (3 : ℝ) * ((2 : ℝ) * Real.pi / ((9 : ℝ) * Real.log (2 : ℝ))) ∧ (2 : ℝ) / Real.pi < (4 : ℝ) / Real.pi ∧ (6 : ℝ) * Real.log (2 : ℝ) < Real.pi ^ (2 : ℕ)) ∧ 1.0698 < (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 3.541)) ∧ (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 3.541)) < 1.07 ∧ 1.1508 < (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 3.085)) ∧ (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 3.085)) < 1.1511 ∧ 1.267 < (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 2.611)) ∧ (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 2.611)) < 1.2672 ∧ (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 2.611)) < (4 : ℝ) / Real.pi ∧ 0.995 * ((4 : ℝ) / Real.pi) < (2 : ℝ) * Real.pi / ((3 : ℝ) * Real.log ((2 : ℝ) * 2.611)) :=109  @FRC.LedgerML.p46037110/-- 46:C11 (p46071) — [chart] The plaquette channel of the chart fails: with A11's series and $u$ the sum of $c_3$ through $\stf^{7}$ at B6's cells, $m/\sig=6.9$, $6.2$, $5.6$, $5.1$ for $n=9,\dots,6$, orders $3,5,7$ within $1\,\%$; at $n=3$: $3.98$, $3.60$, $3.79$, the fifth alone in $3.4$--$3.7$; at channel unity, $u=\frac{23}{54}$, $2.95$, $0.45$, $2.82$. -/111theorem plaquette_channel_cells : FRC.YangMillsML.cellU (0 : ℕ) = (23 / 54 : ℝ) ∧ (6.93 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (9 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (9 : ℕ))) ≤ 6.94 ∧ 6.93 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (9 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (9 : ℕ))) ≤ 6.94 ∧ 6.93 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (9 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (9 : ℕ))) ≤ 6.94) ∧ (6.16 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (8 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (8 : ℕ))) ≤ 6.17 ∧ 6.16 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (8 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (8 : ℕ))) ≤ 6.17 ∧ 6.16 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (8 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (8 : ℕ))) ≤ 6.17) ∧ (5.59 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (7 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (7 : ℕ))) ≤ 5.6 ∧ 5.58 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (7 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (7 : ℕ))) ≤ 5.59 ∧ 5.58 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (7 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (7 : ℕ))) ≤ 5.59) ∧ (5.11 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (6 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (6 : ℕ))) ≤ 5.12 ∧ 5.09 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (6 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (6 : ℕ))) ≤ 5.1 ∧ 5.1 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (6 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (6 : ℕ))) ≤ 5.11) ∧ (4.32 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (4 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (4 : ℕ))) ≤ 4.33 ∧ 4.16 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (4 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (4 : ℕ))) ≤ 4.17 ∧ 4.22 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (4 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (4 : ℕ))) ≤ 4.23) ∧ (3.97 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (3 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (3 : ℕ))) ≤ 3.98 ∧ 3.6 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (3 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (3 : ℕ))) ≤ 3.61 ∧ 3.78 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (3 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (3 : ℕ))) ≤ 3.79) ∧ (3.64 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (2 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (2 : ℕ))) ≤ 3.65 ∧ 2.87 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (2 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (2 : ℕ))) ≤ 2.88 ∧ 3.35 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (2 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (2 : ℕ))) ≤ 3.37) ∧ (2.95 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (0 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (0 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (0 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (0 : ℕ))) ≤ 2.96 ∧ 0.44 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (0 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (0 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (0 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (0 : ℕ))) ≤ 0.45 ∧ 2.81 ≤ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (0 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (0 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (0 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (0 : ℕ))) ≤ 2.82) ∧ (|FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (9 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (9 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (9 : ℕ))) ∧ |FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (9 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (9 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (9 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (9 : ℕ)))) ∧ (|FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (8 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (8 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (8 : ℕ))) ∧ |FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (8 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (8 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (8 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (8 : ℕ)))) ∧ (|FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (7 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (7 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (7 : ℕ))) ∧ |FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (7 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (7 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (7 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (7 : ℕ)))) ∧ (|FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (6 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (6 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (6 : ℕ))) ∧ |FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (6 : ℕ))) - FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (6 : ℕ)))| < 1e-2 * FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (6 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (6 : ℕ)))) ∧ (3.7 < FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (4 : ℕ))) ∧ 3.7 < FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (4 : ℕ))) ∧ 3.7 < FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (4 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (4 : ℕ)))) ∧ (3.4 < FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (3 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (3 : ℕ))) < 3.7 ∧ 3.7 < FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (3 : ℕ))) ∧ 3.7 < FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (3 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (3 : ℕ)))) ∧ 3.4 < FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (2 : ℕ))) ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P3 (FRC.YangMillsML.cellU (2 : ℕ))) < 3.7 ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P5 (FRC.YangMillsML.cellU (2 : ℕ))) < 3.4 ∧ FRC.YangMillsML.ratio (FRC.YangMillsML.cellU (2 : ℕ)) (FRC.YangMillsML.P7 (FRC.YangMillsML.cellU (2 : ℕ))) < 3.4 :=112  @FRC.LedgerML.p46071113/-- 46:C12 (p46036) — [chart] The family of C8 against the lattice: $E_0=\sqrt{a\varkappa}\,2.232$ by the dilation symmetry, $2.232$, $3.157$, $3.348$, $3.157$, $4.464$, $4.735$ for $a\in\{1,2\}$, $\varkappa\in\{1,2,\frac94\}$; none inside any determination's error; the nearest, $a=1$, $\varkappa=\frac94$, is $1.7\,\%$ below the direct value. -/114theorem wrap_family_misses : ∀ (E₀ : ℝ), E₀ = 2.232 → 3.156 < √(2 : ℝ) * E₀ ∧ √(2 : ℝ) * E₀ < 3.157 ∧ √(9 / 4 : ℝ) * E₀ = 3.348 ∧ √(4 : ℝ) * E₀ = 4.464 ∧ 4.734 < √(9 / 2 : ℝ) * E₀ ∧ √(9 / 2 : ℝ) * E₀ < 4.735 ∧ E₀ < 3.384 ∧ √(2 : ℝ) * E₀ < 3.384 ∧ √(9 / 4 : ℝ) * E₀ < 3.384 ∧ 3.76 < √(4 : ℝ) * E₀ ∧ 3.76 < √(9 / 2 : ℝ) * E₀ ∧ 16e-3 < (3.405 - √(9 / 4 : ℝ) * E₀) / 3.405 ∧ (3.405 - √(9 / 4 : ℝ) * E₀) / 3.405 < 18e-3 :=115  @FRC.LedgerML.p46036116/-- 46:C13 (p46041) — The two rationals of the one-loop coefficient are the frame's: the spin term $(2s)^{2}=-2\,\mathrm{Tr}_V(J_{12}^{2})$ is $0$, $1$, $4$ on the scalar, the Weyl spinor and the vector; the charge term $\frac13$ is the leading Faulhaber coefficient of the scalar loop's midpoint sum $3\sum_{k<N}(N-2k-1)^{2}=N(N^{2}-1)$, whose complete cycle $N=\p$ vanishes on the shell. With C4 the species sum of A12 is $3b_0=33-2n_f$ (C5). -/117theorem one_loop_rationals : ∀ (N : ℕ), (3 : ℤ) * FRC.YangMillsML.sq N = ↑N * (↑N ^ (2 : ℕ) - (1 : ℤ)) :=118  @FRC.LedgerML.p46041119/-- 46:C21 (p46064) — The spectrum in $2\pi=\p-1$, the shell's phase cycle, certified by $2\pi\equiv-1$ and $\p$-hard: on the three Subjects $d_1=4\pi^{2}+2\pi+1$, $d_2=(2\pi+2)d_1$, $d_3=8\pi(\pi+1)^{2}$, and the gap of the transfer tally is $1/(2\pi+2)$, a pure number, one expression on every Subject, with the residue $1$ on the shell. [chart] $0.1207$ at the classical $\pi$. -/120theorem spectrum_in_two_pi : 0.12072 < (1 : ℝ) / ((2 : ℝ) * Real.pi + (2 : ℝ)) ∧ (1 : ℝ) / ((2 : ℝ) * Real.pi + (2 : ℝ)) < 0.12073 :=121  @FRC.LedgerML.p46064122set_option linter.defProp false in123/-- 46:P2 (p46024) — [chart] Between laboratory scales $1/\alpha_s$ is linear in $\ln(\mu/\mu_0)$ with slope $b_0/2\pi$, $b_0$ the window rational (C5, A4). Falsifier: a measured $1/\alpha_s(\mu)$ off the linear law beyond the imported two-loop correction. Confrontation: one loop gives $\alpha_s(m_\tau)=0.279$ against $0.312(15)$, $2.2$ standard deviations below; with the imported $b_1$ the run gives $0.313$. -/124def running_prediction := @FRC.LedgerML.p46024125/-- 46:P3 (p46043) — [chart] The radial ratio of the operator form: $E_1/E_0\approx1.49$ for every $a$ and $\varkappa$, a property of the form of C8 and of every state the one-body wrap describes. Falsifier: such a state's first radial ratio measured off $1.49$. Confrontation: $1.54(11)$ (1999) agrees; $1.72(2)$ (2020) excludes $1.49$ by ten standard deviations under first-order error propagation at any correlation: the form fails for the glueball. -/126theorem radial_ratio_prediction : ∀ (r : Rat), @Eq Rat r (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 14915) true (nat_lit 4)) → And (@LT.lt Rat Rat.instLT (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) r (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1544) true (nat_lit 3)))) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 5) true (nat_lit 1)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 112) true (nat_lit 3)))) (And (@LT.lt Rat Rat.instLT (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 14) (@Rat.instOfNat (nat_lit 14))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 16) true (nat_lit 3))) (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1720) true (nat_lit 3)) r)) (And (@LT.lt Rat Rat.instLT (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 10) (@Rat.instOfNat (nat_lit 10))) (@HAdd.hAdd Rat Rat Rat (@instHAdd Rat Rat.instAdd) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfNat.ofNat Rat (nat_lit 41) (@Rat.instOfNat (nat_lit 41))) (@OfNat.ofNat Rat (nat_lit 3405) (@Rat.instOfNat (nat_lit 3405)))) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 5855) (@Rat.instOfNat (nat_lit 5855))) (@OfNat.ofNat Rat (nat_lit 21) (@Rat.instOfNat (nat_lit 21)))) (@HPow.hPow Rat Nat Rat (@instHPow Rat Nat (@NPow.toPow Rat (@Monoid.toNPow Rat Rat.monoid))) (@OfNat.ofNat Rat (nat_lit 3405) (@Rat.instOfNat (nat_lit 3405))) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))))) (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfNat.ofNat Rat (nat_lit 5855) (@Rat.instOfNat (nat_lit 5855))) (@OfNat.ofNat Rat (nat_lit 3405) (@Rat.instOfNat (nat_lit 3405)))) r)) (And (@LT.lt Rat Rat.instLT (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 408795) true (nat_lit 5)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 233811) true (nat_lit 5))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1720) true (nat_lit 3)))) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfNat.ofNat Rat (nat_lit 2) (@Rat.instOfNat (nat_lit 2))) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 16) true (nat_lit 3)))) (And (@LT.lt Rat Rat.instLT (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 1748) true (nat_lit 3)) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 408795) true (nat_lit 5)) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 233811) true (nat_lit 5)))) (@LT.lt Rat Rat.instLT (@abs Rat Rat.instLattice Rat.addGroup (@HSub.hSub Rat Rat Rat (@instHSub Rat Rat.instSub) (@HDiv.hDiv Rat Rat Rat (@instHDiv Rat Rat.instDiv) (@OfNat.ofNat Rat (nat_lit 1440) (@Rat.instOfNat (nat_lit 1440))) (@OfNat.ofNat Rat (nat_lit 939) (@Rat.instOfNat (nat_lit 939)))) r)) (@HMul.hMul Rat Rat Rat (@instHMul Rat Rat.instMul) (@OfScientific.ofScientific Rat Rat.instOfScientific (nat_lit 3) true (nat_lit 2)) r)))))) :=127  @FRC.LedgerML.p46043128-- end ledger predicates129130end FRC.YangMills131