YangMills.lean — FrcCore

1import FrcCore.Theme.YangMills2import FrcCore.Keys.Yangmills34/-!5# FrcCore.YangMills — 46-yangmills' paper module (8 November 2026)67The predicate declarations of *Yang–Mills and the Mass Gap over Finite Holographic Substrate* (46-yangmills),8`FRC.YangMills.<name>` (named by their rows' declared names, the key in each docstring), one per witnessed row with a Lean9cell, each the conjunction of the theorems its ledger row cites in the yangmills theme's `Theme/YangMills.lean` (the10norm-one torus without a shell eigenvalue, the split torus's fixed lines, the arithmetic of the centre's order formula, the11singlet-multiplicity identities of the glueball and the adjoint wrap, the Casimir and one-loop rationals, the drive exponent).12The declarations are generated by `lean/make_predicates.py` from the paper's ledger; the theorems live in the theme file.13-/1415namespace FRC.YangMills1617-- Ledger predicates of 46-yangmills (generated by make_predicates.py from docs/46-yangmills/46-yangmills-ledger.json; edit the ledger, not this section)18/-- 46:A9 (p46034) — The frame's multiplicities, for $q$ a power of a prime $\p$ of the totality: $\mathrm{SL}_3(\F_{q^{2}})$ fixes the kernel modulo $\p$ of the matrix $D$, of dimension at least the compact count $C(a,b)$; for $\p>3$ and $q^{2}>a+b+\min(a,b)$ the pairing-and-determinant tensors span the vectors it fixes, of dimension $C(a,b)$; for $a+b+2\le\p$ the frame fixes the same vectors (to degree $9$ on Subjects above $11$). -/19theorem frame_multiplicities : (FRC.YangMills.rootFacts (FRC.YangMills.planePoint (13 : Nat) (1 : FRC.Shell (13 : Nat)) (0 : FRC.Shell (13 : Nat))) (FRC.YangMills.planePoint (13 : Nat) (6 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat))) = true ∧ FRC.YangMills.rootFacts (FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat))) (FRC.YangMills.planePoint (13 : Nat) (1 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat))) = true) ∧ (FRC.YangMills.rootFacts (FRC.YangMills.planePoint (173 : Nat) (1 : FRC.Shell (173 : Nat)) (0 : FRC.Shell (173 : Nat))) (FRC.YangMills.planePoint (173 : Nat) (86 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat))) = true ∧ FRC.YangMills.rootFacts (FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat))) (FRC.YangMills.planePoint (173 : Nat) (1 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat))) = true) ∧ (FRC.YangMills.rootFacts (FRC.YangMills.planePoint (1549 : Nat) (1 : FRC.Shell (1549 : Nat)) (0 : FRC.Shell (1549 : Nat))) (FRC.YangMills.planePoint (1549 : Nat) (774 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat))) = true ∧ FRC.YangMills.rootFacts (FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat))) (FRC.YangMills.planePoint (1549 : Nat) (1 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat))) = true) ∧ ((6 : FRC.Shell (13 : Nat)) * (11 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ (6 : FRC.Shell (173 : Nat)) * (29 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) ∧ (6 : FRC.Shell (1549 : Nat)) * (1291 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat))) ∧ ((25 : Nat) + (12 : Nat) < (13 : Nat) * (13 : Nat) ∧ (345 : Nat) + (172 : Nat) < (173 : Nat) * (173 : Nat) ∧ (3097 : Nat) + (1548 : Nat) < (1549 : Nat) * (1549 : Nat)) ∧ (9 : Nat) + (2 : Nat) ≤ (13 : Nat) :=20  @FRC.Ledger.p4603421/-- 46:C1 (p46010) — The norm-one cycle has no shell eigenvalue. For every frame of the totality a norm-one element $a+b\sqrt\nu$ with $b\neq0$ has no eigenvalue in $\Fp$ (its discriminant $4\nu b^{2}$ is a nonsquare), so no line of the plane is mapped to itself by every element of the cycle; the split torus fixes exactly two lines. -/22theorem no_residue_zero_registration : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν a b r : FRC.Shell p}, ¬FRC.Shell.Frame.IsSquare ν → a * a + -(ν * (b * b)) = (1 : FRC.Shell p) → b ≠ (0 : FRC.Shell p) → r * r + -((a + a) * r) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → False) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν a b : FRC.Shell p}, a * a + -(ν * (b * b)) = (1 : FRC.Shell p) → b = (0 : FRC.Shell p) → a = (1 : FRC.Shell p) ∨ a = (-1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {x y s : FRC.Shell p}, g * s = (1 : FRC.Shell p) → (g * x * y = x * (s * y) ↔ x * y = (0 : FRC.Shell p)) :=23  @FRC.Ledger.p4601024/-- 46:C2 (p46011) — The centre of the unitary frame: its order $\gcdop(3,q+1)$ is $3$ exactly when $q\equiv2\pmod3$. Among the Subjects $173$ has it, $13$ and $1549$ do not, and $12$ of $21$ shells below $200$ do; on $\SU(3,\F_2)$ it is found by enumeration. The three Carriers are $5$ modulo $12$ (A18). The Lean cell is the arithmetic of the order formula. -/25theorem triality_centre : (∀ (q : Nat), q < (200 : Nat) → (q % (12 : Nat) = (5 : Nat) → Nat.gcd (3 : Nat) (q + (1 : Nat)) = (3 : Nat)) ∧ (q % (12 : Nat) = (1 : Nat) → Nat.gcd (3 : Nat) (q + (1 : Nat)) = (1 : Nat)) ∧ (q % (12 : Nat) = (5 : Nat) ↔ q % (4 : Nat) = (1 : Nat) ∧ q % (3 : Nat) = (2 : Nat))) ∧ (Nat.gcd (3 : Nat) ((13 : Nat) + (1 : Nat)) = (1 : Nat) ∧ Nat.gcd (3 : Nat) ((173 : Nat) + (1 : Nat)) = (3 : Nat) ∧ Nat.gcd (3 : Nat) ((1549 : Nat) + (1 : Nat)) = (1 : Nat) ∧ (13 : Nat) % (12 : Nat) = (1 : Nat) ∧ (173 : Nat) % (12 : Nat) = (5 : Nat) ∧ (1549 : Nat) % (12 : Nat) = (1 : Nat)) ∧ (([(5 : Nat), (17 : Nat), (29 : Nat), (41 : Nat), (53 : Nat), (89 : Nat), (101 : Nat), (113 : Nat), (137 : Nat), (149 : Nat), (173 : Nat), (197 : Nat)].all fun q => q % (12 : Nat) == (5 : Nat) && Nat.gcd (3 : Nat) (q + (1 : Nat)) == (3 : Nat)) = true ∧ ([(13 : Nat), (37 : Nat), (61 : Nat), (73 : Nat), (97 : Nat), (109 : Nat), (157 : Nat), (181 : Nat), (193 : Nat)].all fun q => q % (12 : Nat) == (1 : Nat) && Nat.gcd (3 : Nat) (q + (1 : Nat)) == (1 : Nat)) = true ∧ [(5 : Nat), (17 : Nat), (29 : Nat), (41 : Nat), (53 : Nat), (89 : Nat), (101 : Nat), (113 : Nat), (137 : Nat), (149 : Nat), (173 : Nat), (197 : Nat)].length + [(13 : Nat), (37 : Nat), (61 : Nat), (73 : Nat), (97 : Nat), (109 : Nat), (157 : Nat), (181 : Nat), (193 : Nat)].length = (21 : Nat)) ∧ (233 : Nat) % (12 : Nat) = (5 : Nat) ∧ (30089 : Nat) % (12 : Nat) = (5 : Nat) ∧ (2408561 : Nat) % (12 : Nat) = (5 : Nat) ∧ ((233 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat) ∧ ((30089 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat) ∧ ((2408561 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat) ∧ ((233 : Nat) - (1 : Nat)) % (3 : Nat) = (1 : Nat) ∧ ((30089 : Nat) - (1 : Nat)) % (3 : Nat) = (1 : Nat) ∧ ((2408561 : Nat) - (1 : Nat)) % (3 : Nat) = (1 : Nat) ∧ ((0 : Int) * (0 : Int) - (0 : Int) * (1 : Int) + (1 : Int) * (1 : Int) = (1 : Int) ∧ (-1 : Int) * (-1 : Int) - (-1 : Int) * (-1 : Int) + (-1 : Int) * (-1 : Int) = (1 : Int)) ∧ ((0 : Int) * (0 : Int) - (1 : Int) * (1 : Int) = (-1 : Int) ∧ (0 : Int) * (1 : Int) + (1 : Int) * (0 : Int) - (1 : Int) * (1 : Int) = (-1 : Int)) ∧ (0 : Int) * (-1 : Int) - (1 : Int) * (-1 : Int) = (1 : Int) ∧ (0 : Int) * (-1 : Int) + (1 : Int) * (-1 : Int) - (1 : Int) * (-1 : Int) = (0 : Int) :=26  @FRC.Ledger.p4601127/-- 46:C3 (p46012) — The residue series on the instance. On the $216$ elements of $\SU(3,\F_2)$ over $\F_4$ (no nontrivial character over $\F_4$) the adjoint action fixes no nonzero traceless matrix (gluon $0$), the determinant is the one invariant of $\Lambda^{3}$ (baryon $1$), and the commutants of the fundamental and the adjoint are one-dimensional (meson $1$, glueball $1$). -/28theorem residue_series_glueball : FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) - (6 : Int) = (0 : Int) ∧ FRC.Hadrons.moment6 (3 : Nat) (0 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (2 : Nat) - (2 : Int) * FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) + (6 : Int) = (6 : Int) * (1 : Int) :=29  @FRC.Ledger.p4601230/-- 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. -/31theorem colour_casimirs : ((3 : Int) * (3 : Int) - (1 : Int) = (8 : Int) ∧ (6 : Nat) * (4 : Nat) = (3 : Nat) * (8 : Nat) ∧ (2 : Int) * (3 : Int) * (3 : Int) = (18 : Int) ∧ (8 : Nat) * (9 : Nat) = (4 : Nat) * (18 : Nat) ∧ (2 : Nat) * (1 : Nat) = (2 : Nat)) ∧ ((List.range (168 : Nat)).all fun n => (2 : Nat) * (((11 : Nat) * n) ^ (2 : Nat) + ((14 : Nat) * n) ^ (2 : Nat) + ((25 : Nat) * n) ^ (2 : Nat)) == (6 : Nat) * (n ^ (2 : Nat) + ((12 : Nat) * n) ^ (2 : Nat) + ((13 : Nat) * n) ^ (2 : Nat))) = true ∧ (2 : Nat) * ((171 : Nat) ^ (2 : Nat) + (174 : Nat) ^ (2 : Nat) + (345 : Nat) ^ (2 : Nat)) = (6 : Nat) * ((1 : Nat) + (172 : Nat) ^ (2 : Nat) + (173 : Nat) ^ (2 : Nat)) ∧ (2 : Nat) * ((1547 : Nat) ^ (2 : Nat) + (1550 : Nat) ^ (2 : Nat) + (3097 : Nat) ^ (2 : Nat)) = (6 : Nat) * ((1 : Nat) + (1548 : Nat) ^ (2 : Nat) + (1549 : Nat) ^ (2 : Nat)) :=32  @FRC.Ledger.p4601333/-- 46:C5 (p46014) — The window rational: $b_0=11-\frac23n_f$ takes the values $9$, $\frac{25}{3}$, $\frac{23}{3}$, $7$ for $n_f=3,4,5,6$, is positive for every $n_f\le16$ and negative for every $n_f$ from $17$ to $200$. -/34theorem window_rational_b0 : (FRC.YangMills.threeB0 (3 : Nat) = (27 : Int) ∧ FRC.YangMills.threeB0 (4 : Nat) = (25 : Int) ∧ FRC.YangMills.threeB0 (5 : Nat) = (23 : Int) ∧ FRC.YangMills.threeB0 (6 : Nat) = (21 : Int)) ∧ (∀ (nf : Nat), nf < (17 : Nat) → (0 : Int) < FRC.YangMills.threeB0 nf) ∧ FRC.YangMills.threeB0 (17 : Nat) = (-1 : Int) ∧ ∀ (nf : Nat), nf < (201 : Nat) → (17 : Nat) ≤ nf → FRC.YangMills.threeB0 nf < (0 : Int) :=35  @FRC.Ledger.p4601436/-- 46:C6 (p46015) — The drive exponent. On every shell of the totality the powers of the drive permute the nonzero elements: each winding rate has one exponent below $\p-1$, and exponents add modulo $\p-1$ --- the discrete logarithm on the shell. The ledger file decides it on the Subjects and the sweep. -/37theorem drive_exponent_permutes : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {w : FRC.Shell p}, w ≠ (0 : FRC.Shell p) → ∃ n, n < p - (1 : Nat) ∧ g ^ n = w) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {m n : Nat}, m < p - (1 : Nat) → n < p - (1 : Nat) → g ^ m = g ^ n → m = n) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (m n : Nat), g ^ m * g ^ n = g ^ ((m + n) % (p - (1 : Nat))) :=38  @FRC.Ledger.p4601539/-- 46:C7 (p46016) — The tension's coefficient to order $\stf^{7}$: the fundamental plaquette coefficient of $\SU(3)$ in the stiffness (A16) is $c_3=\stf/3+\stf^{2}/6-5\stf^{4}/72-\dots$ modulo $\stf^{8}$, every coefficient a rational built from the singlet multiplicities, the frame's in the degrees used (A9); the computed terms sum to $\frac{23}{54}$ at channel unity. The instance $2T$ agrees with $\SU(2)$'s series through $\stf^{3}$, first differing at $\stf^{5}$. -/40theorem tension_coefficient_series : (List.map FRC.YangMills.ex (List.range (8 : Nat)) = [(1 : Nat), (0 : Nat), (2 : Nat), (2 : Nat), (12 : Nat), (30 : Nat), (130 : Nat), (462 : Nat)] ∧ List.map FRC.YangMills.exc (List.range (8 : Nat)) = [(0 : Nat), (1 : Nat), (1 : Nat), (6 : Nat), (15 : Nat), (65 : Nat), (231 : Nat), (973 : Nat)]) ∧ FRC.YangMills.c3WF [(1 : Nat), (0 : Nat), (2 : Nat), (2 : Nat), (12 : Nat), (30 : Nat), (130 : Nat), (462 : Nat)] [(0 : Nat), (1 : Nat), (1 : Nat), (6 : Nat), (15 : Nat), (65 : Nat), (231 : Nat), (973 : Nat)] (8 : Nat) = [((0 : Int), (1 : Nat)), FRC.YangMills.WF.frac (1 : Int) (3 : Nat), FRC.YangMills.WF.frac (1 : Int) ((2 : Nat) * (3 : Nat)), ((0 : Int), (1 : Nat)), FRC.YangMills.WF.frac (-5 : Int) ((2 : Nat) ^ (3 : Nat) * (3 : Nat) ^ (2 : Nat)), FRC.YangMills.WF.frac (-1 : Int) ((2 : Nat) ^ (3 : Nat) * (3 : Nat)), FRC.YangMills.WF.frac (7 : Int) ((2 : Nat) ^ (4 : Nat) * (3 : Nat) ^ (2 : Nat) * (5 : Nat)), FRC.YangMills.WF.frac (59 : Int) ((2 : Nat) ^ (4 : Nat) * (3 : Nat) ^ (3 : Nat) * (5 : Nat))] ∧ (FRC.YangMills.c3Check (13 : Nat) = true ∧ FRC.YangMills.c3Check (173 : Nat) = true ∧ FRC.YangMills.c3Check (1549 : Nat) = true ∧ [(13 : Nat), (17 : Nat), (29 : Nat), (37 : Nat), (41 : Nat), (53 : Nat), (61 : Nat), (73 : Nat), (89 : Nat), (97 : Nat), (101 : Nat), (109 : Nat), (113 : Nat), (137 : Nat), (149 : Nat), (157 : Nat), (173 : Nat), (181 : Nat), (193 : Nat), (197 : Nat)].all FRC.YangMills.c3Check = true ∧ (2 : FRC.Shell (5 : Nat)) ^ (4 : Nat) * (3 : FRC.Shell (5 : Nat)) ^ (2 : Nat) * (5 : FRC.Shell (5 : Nat)) = (0 : FRC.Shell (5 : Nat))) ∧ FRC.YangMills.c2Check (13 : Nat) = true ∧ FRC.YangMills.c2Check (173 : Nat) = true ∧ FRC.YangMills.c2Check (1549 : Nat) = true :=41  @FRC.Ledger.p4601642/-- 46:C9 (p46030) — The adjoint wrap: the adjoint plaquette coefficient has $\stf^{1}$ coefficient $0$ and $\stf^{2}$ coefficient $\frac18=\frac98(\frac13)^{2}$, both identities holding on $\SU(3,\F_2)$ by enumeration; modulo $\stf^{6}$, $c_8=\frac98c_3^{2}(1-\stf/3+\stf^{2}/12+\stf^{3}/12)$: twice the fundamental string tension at leading order. -/43theorem adjoint_wrap_two_sheets : FRC.Hadrons.moment6 (2 : Nat) (1 : Nat) + FRC.Hadrons.moment6 (1 : Nat) (2 : Nat) - FRC.Hadrons.moment6 (1 : Nat) (0 : Nat) - FRC.Hadrons.moment6 (0 : Nat) (1 : Nat) = (0 : Int) ∧ FRC.Hadrons.moment6 (3 : Nat) (1 : Nat) + (2 : Int) * FRC.Hadrons.moment6 (2 : Nat) (2 : Nat) + FRC.Hadrons.moment6 (1 : Nat) (3 : Nat) - FRC.Hadrons.moment6 (2 : Nat) (0 : Nat) - (2 : Int) * FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) - FRC.Hadrons.moment6 (0 : Nat) (2 : Nat) = (6 : Int) * (2 : Int) :=44  @FRC.Ledger.p4603045/-- 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). -/46theorem short_range_fails : FRC.YangMills.alphaDeclared.within (FRC.YangMills.WF.frac (10065 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (10075 : Int) (10000 : Nat)) = true ∧ FRC.YangMills.couplingC.within (FRC.YangMills.WF.frac (3015 : Int) (1000 : Nat)) (FRC.YangMills.WF.frac (3025 : Int) (1000 : Nat)) = true ∧ FRC.YangMills.herbstOne.within (FRC.YangMills.WF.frac (636 : Int) (1000 : Nat)) (FRC.YangMills.WF.frac (637 : Int) (1000 : Nat)) = true ∧ FRC.YangMills.herbstTwo.within (FRC.YangMills.WF.frac (1273 : Int) (1000 : Nat)) (FRC.YangMills.WF.frac (1274 : Int) (1000 : Nat)) = true ∧ FRC.YangMills.herbstTwo.snd.lt FRC.YangMills.couplingC.fst = true ∧ FRC.YangMills.herbstOne.snd.lt FRC.YangMills.couplingC.fst = true ∧ ((FRC.YangMills.WF.ofNat (6 : Nat)).mul (FRC.YangMills.lnBr (FRC.YangMills.WF.ofNat (2 : Nat)) (12 : Nat)).snd).lt (FRC.YangMills.piBr.fst.mul FRC.YangMills.piBr.fst) = true :=47  @FRC.Ledger.p4603748/-- 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$. -/49theorem plaquette_channel_cells : FRC.YangMills.ratioWithin (7 : Nat) (FRC.YangMills.WF.frac (465 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (685 : Int) (100 : Nat)) (FRC.YangMills.WF.frac (695 : Int) (100 : Nat)) = true ∧ FRC.YangMills.ratioWithin (7 : Nat) (FRC.YangMills.WF.frac (842 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (615 : Int) (100 : Nat)) (FRC.YangMills.WF.frac (625 : Int) (100 : Nat)) = true ∧ FRC.YangMills.ratioWithin (7 : Nat) (FRC.YangMills.WF.frac (1246 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (555 : Int) (100 : Nat)) (FRC.YangMills.WF.frac (565 : Int) (100 : Nat)) = true ∧ FRC.YangMills.ratioWithin (7 : Nat) (FRC.YangMills.WF.frac (1671 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (505 : Int) (100 : Nat)) (FRC.YangMills.WF.frac (515 : Int) (100 : Nat)) = true ∧ ([FRC.YangMills.WF.frac (465 : Int) (10000 : Nat), FRC.YangMills.WF.frac (842 : Int) (10000 : Nat), FRC.YangMills.WF.frac (1246 : Int) (10000 : Nat), FRC.YangMills.WF.frac (1671 : Int) (10000 : Nat)].all fun u => (FRC.YangMills.spreadHi u).lt (FRC.YangMills.WF.frac (1 : Int) (100 : Nat))) = true ∧ ([(3 : Nat), (5 : Nat), (7 : Nat)].all fun o => FRC.YangMills.ratioWithin o (FRC.YangMills.WF.frac (2553 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (37 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (5 : Int) (1 : Nat))) = true ∧ FRC.YangMills.ratioWithin (3 : Nat) (FRC.YangMills.WF.frac (2994 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (37 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (41 : Int) (10 : Nat)) = true ∧ FRC.YangMills.ratioWithin (5 : Nat) (FRC.YangMills.WF.frac (2994 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (34 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (37 : Int) (10 : Nat)) = true ∧ FRC.YangMills.ratioWithin (7 : Nat) (FRC.YangMills.WF.frac (2994 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (37 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (4 : Int) (1 : Nat)) = true ∧ FRC.YangMills.ratioWithin (3 : Nat) (FRC.YangMills.WF.frac (3425 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (34 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (37 : Int) (10 : Nat)) = true ∧ FRC.YangMills.ratioWithin (5 : Nat) (FRC.YangMills.WF.frac (3425 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (25 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (34 : Int) (10 : Nat)) = true ∧ FRC.YangMills.ratioWithin (7 : Nat) (FRC.YangMills.WF.frac (3425 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (3 : Int) (1 : Nat)) (FRC.YangMills.WF.frac (34 : Int) (10 : Nat)) = true ∧ FRC.YangMills.uAtUnity = FRC.YangMills.WF.frac (23 : Int) (54 : Nat) ∧ FRC.YangMills.ratioWithin (3 : Nat) (FRC.YangMills.WF.frac (23 : Int) (54 : Nat)) (FRC.YangMills.WF.frac (29 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (3 : Int) (1 : Nat)) = true ∧ FRC.YangMills.ratioWithin (5 : Nat) (FRC.YangMills.WF.frac (23 : Int) (54 : Nat)) (FRC.YangMills.WF.frac (4 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (5 : Int) (10 : Nat)) = true ∧ FRC.YangMills.ratioWithin (7 : Nat) (FRC.YangMills.WF.frac (23 : Int) (54 : Nat)) (FRC.YangMills.WF.frac (28 : Int) (10 : Nat)) (FRC.YangMills.WF.frac (29 : Int) (10 : Nat)) = true :=50  @FRC.Ledger.p4607151/-- 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. -/52theorem wrap_family_misses : ((FRC.YangMills.family.zip [(2232 : Nat), (3157 : Nat), (3348 : Nat), (3157 : Nat), (4464 : Nat), (4735 : Nat)]).all fun x => decide (((2 : Nat) * x.snd - (1 : Nat)) ^ (2 : Nat) < FRC.YangMills.famSq x.fst.fst x.fst.snd ∧ FRC.YangMills.famSq x.fst.fst x.fst.snd < ((2 : Nat) * x.snd + (1 : Nat)) ^ (2 : Nat))) = true ∧ (FRC.YangMills.family.all fun m => FRC.YangMills.determinations.all fun d => decide (FRC.YangMills.famSq m.fst m.snd < (4 : Nat) * (d.fst - d.snd) ^ (2 : Nat) ∨ (4 : Nat) * (d.fst + d.snd) ^ (2 : Nat) < FRC.YangMills.famSq m.fst m.snd)) = true ∧ (FRC.YangMills.family.all fun m => FRC.YangMills.determinations.all fun d => decide (FRC.YangMills.famSq m.fst m.snd ≤ (4 : Nat) * (d.fst - (57 : Nat)) ^ (2 : Nat) ∨ (4 : Nat) * (d.fst + (57 : Nat)) ^ (2 : Nat) ≤ FRC.YangMills.famSq m.fst m.snd)) = true ∧ FRC.YangMills.famSq (1 : Nat) (9 : Nat) = ((2 : Nat) * (3348 : Nat)) ^ (2 : Nat) ∧ (3348 : Nat) + (57 : Nat) = (3405 : Nat) ∧ (165 : Nat) * (3405 : Nat) < (57 : Nat) * (10000 : Nat) ∧ (57 : Nat) * (10000 : Nat) < (175 : Nat) * (3405 : Nat) :=53  @FRC.Ledger.p4603654/-- 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). -/55theorem one_loop_rationals : ((-((2 : FRC.Shell (13 : Nat)) * FRC.YangMills.tr (FRC.YangMills.mmul FRC.YangMills.jVec FRC.YangMills.jVec)) = (4 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ -FRC.YangMills.tr (FRC.YangMills.mmul (FRC.YangMills.jWeyl (5 : FRC.Shell (13 : Nat))) (FRC.YangMills.jWeyl (5 : FRC.Shell (13 : Nat)))) = (2 : FRC.Shell (13 : Nat))) ∧ (-((2 : FRC.Shell (173 : Nat)) * FRC.YangMills.tr (FRC.YangMills.mmul FRC.YangMills.jVec FRC.YangMills.jVec)) = (4 : FRC.Shell (173 : Nat)) ∧ (80 : FRC.Shell (173 : Nat)) * (80 : FRC.Shell (173 : Nat)) = (-1 : FRC.Shell (173 : Nat)) ∧ -FRC.YangMills.tr (FRC.YangMills.mmul (FRC.YangMills.jWeyl (80 : FRC.Shell (173 : Nat))) (FRC.YangMills.jWeyl (80 : FRC.Shell (173 : Nat)))) = (2 : FRC.Shell (173 : Nat))) ∧ (-((2 : FRC.Shell (1549 : Nat)) * FRC.YangMills.tr (FRC.YangMills.mmul FRC.YangMills.jVec FRC.YangMills.jVec)) = (4 : FRC.Shell (1549 : Nat)) ∧ (88 : FRC.Shell (1549 : Nat)) * (88 : FRC.Shell (1549 : Nat)) = (-1 : FRC.Shell (1549 : Nat)) ∧ -FRC.YangMills.tr (FRC.YangMills.mmul (FRC.YangMills.jWeyl (88 : FRC.Shell (1549 : Nat))) (FRC.YangMills.jWeyl (88 : FRC.Shell (1549 : Nat)))) = (2 : FRC.Shell (1549 : Nat))) ∧ FRC.YangMills.tr (FRC.YangMills.mmul [[(0 : FRC.Shell (13 : Nat))]] [[(0 : FRC.Shell (13 : Nat))]]) = (0 : FRC.Shell (13 : Nat))) ∧ (∀ (N : Nat), N < (400 : Nat) → (3 : Int) * FRC.YangMills.sq N = ↑N * (↑N ^ (2 : Nat) - (1 : Int))) ∧ (∀ (N : Nat), N < (173 : Nat) → FRC.YangMills.sqS N = FRC.Shell.ofNat N * (FRC.Shell.ofNat N ^ (2 : Nat) + (-1 : FRC.Shell (173 : Nat))) * FRC.YangMills.invS (3 : FRC.Shell (173 : Nat))) ∧ (FRC.YangMills.sqS (13 : Nat) = (0 : FRC.Shell (13 : Nat)) ∧ FRC.YangMills.sqS (173 : Nat) = (0 : FRC.Shell (173 : Nat)) ∧ FRC.YangMills.sqS (1549 : Nat) = (0 : FRC.Shell (1549 : Nat)) ∧ FRC.YangMills.sqS (10 : Nat) = (330 : FRC.Shell (173 : Nat))) ∧ ∀ (nf : Nat), nf < (201 : Nat) → FRC.YangMills.threeB0 nf = (3 : Int) * ((3 : Int) * (4 : Int) - (1 : Int)) - ↑nf * (1 : Int) * ((3 : Int) * (1 : Int) - (1 : Int)) :=56  @FRC.Ledger.p4604157/-- 46:C14 (p46051) — The series' window: the $\stf^{k}$ coefficient of $c_3$ uses the invariant counts of degree $\le k+1$, that of $c_8$ degree $\le k+2$, so the frame's coefficients are built from the compact counts through $\stf^{\p-3}$, $\stf^{\p-4}$ by A9 and $\stf^{2\p-2}$, $\stf^{2\p-3}$ by C15; on the instance $M(4,1)=4$ against $3$ puts $c_3$'s $\stf^{4}$ at $0$ and $c_8$'s $\stf^{3}$ at $1/8$. -/58theorem series_window_corollary : ((13 : Nat) - (3 : Nat) = (10 : Nat) ∧ (7 : Nat) ≤ (13 : Nat) - (3 : Nat) ∧ (7 : Nat) ≤ (173 : Nat) - (3 : Nat) ∧ (7 : Nat) ≤ (1549 : Nat) - (3 : Nat) ∧ (7 : Nat) ≤ (13 : Nat) - (4 : Nat)) ∧ FRC.YangMills.windowCheck = true :=59  @FRC.Ledger.p4605160/-- 46:C15 (p46053) — The frame's window and first departure $d_*$: for odd $\p$ the frame's invariants in $\mathbf3^{\otimes a}\otimes\bar{\mathbf3}^{\otimes b}$ are the compact ones through degree $2\p-1$ (the coordinate $\SU(2)$ subgroups, A13; the count, A9, at $\p=3$ computed), and the Frobenius tensor $v_\p$ at $(4\p-4,1)$ lies beyond them, so $2\p\le d_*\le4\p-3$: $[26,49]$ on $\F_{13}$, $[346,689]$ on $\F_{173}$; $d_*=5$, $9$ on $\F_2$, $\F_3$. -/61theorem frame_window_theorem : FRC.YangMills.binomRow (13 : Nat) (11 : Nat) (25 : Nat) = FRC.YangMills.expectedRow (13 : Nat) (11 : Nat) (25 : Nat) ∧ FRC.YangMills.binomRow (13 : Nat) (12 : Nat) (25 : Nat) = FRC.YangMills.expectedRow (13 : Nat) (12 : Nat) (25 : Nat) ∧ FRC.YangMills.binomRow (13 : Nat) (24 : Nat) (12 : Nat) = FRC.YangMills.expectedRow (13 : Nat) (24 : Nat) (12 : Nat) ∧ FRC.YangMills.binomRow (13 : Nat) (25 : Nat) (12 : Nat) = FRC.YangMills.expectedRow (13 : Nat) (25 : Nat) (12 : Nat) ∧ ((2 : Nat) * (13 : Nat) - (1 : Nat) ≠ (13 : Nat) - (2 : Nat) ∧ (2 : Nat) * (13 : Nat) - (1 : Nat) - ((13 : Nat) - (2 : Nat)) = (13 : Nat) + (1 : Nat)) ∧ ((2 : Nat) * (13 : Nat) = (26 : Nat) ∧ (4 : Nat) * (13 : Nat) - (3 : Nat) = (49 : Nat) ∧ (2 : Nat) * (173 : Nat) = (346 : Nat) ∧ (4 : Nat) * (173 : Nat) - (3 : Nat) = (689 : Nat) ∧ (2 : Nat) * (1549 : Nat) = (3098 : Nat) ∧ (4 : Nat) * (1549 : Nat) - (3 : Nat) = (6193 : Nat)) ∧ ((2 : Nat) * (13 : Nat) - (2 : Nat) = (24 : Nat) ∧ (2 : Nat) * (13 : Nat) - (3 : Nat) = (23 : Nat) ∧ (7 : Nat) < (2 : Nat) * (13 : Nat) - (3 : Nat)) ∧ (4 : Nat) * (2 : Nat) - (3 : Nat) = (5 : Nat) ∧ (4 : Nat) * (3 : Nat) - (3 : Nat) = (9 : Nat) :=62  @FRC.Ledger.p4605363/-- 46:C16 (p46056) — The amplitude's finite properties: $U_s$ has three eigenvalues in $\F_{q^{2}}$, or none and an order dividing $q^{2}-q+1$; $w$ is a class function, $w(U^{-1})=\overline{w(U)}$, $w(zU)=\iota(z)w(U)$ for central $z$, and reduces to $\operatorname{Tr}U$; if $\p$ divides the order of $U$ then $U_s$ has eigenvalues $(\lambda,\lambda,\lambda^{-2})$, $\lambda^{q+1}=1$, so $w(U)=2\eta+\eta^{-2}$ and every unipotent has $w=3$; if $3\mid q+1$ then $\langle w\rangle=0$ (B3). -/64theorem spectral_amplitude_theorem : (((13 : Nat) * (13 : Nat) - (1 : Nat) = (168 : Nat) ∧ (173 : Nat) * (173 : Nat) - (1 : Nat) = (29928 : Nat) ∧ (1549 : Nat) * (1549 : Nat) - (1 : Nat) = (2399400 : Nat)) ∧ (Nat.gcd (168 : Nat) (232 : Nat) = (8 : Nat) ∧ Nat.gcd (29928 : Nat) (30088 : Nat) = (8 : Nat) ∧ Nat.gcd (2399400 : Nat) (2408560 : Nat) = (40 : Nat)) ∧ ((13 : Nat) * (13 : Nat) - (13 : Nat) + (1 : Nat) = (157 : Nat) ∧ Nat.gcd (157 : Nat) (232 : Nat) = (1 : Nat) ∧ ((173 : Nat) * (173 : Nat) - (173 : Nat) + (1 : Nat)).gcd (30088 : Nat) = (1 : Nat) ∧ ((1549 : Nat) * (1549 : Nat) - (1549 : Nat) + (1 : Nat)).gcd (2408560 : Nat) = (1 : Nat)) ∧ (((13 : Nat) + (1 : Nat)) % (3 : Nat) ≠ (0 : Nat) ∧ ((173 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat) ∧ ((1549 : Nat) + (1 : Nat)) % (3 : Nat) ≠ (0 : Nat) ∧ ((2 : Nat) + (1 : Nat)) % (3 : Nat) = (0 : Nat)) ∧ (FRC.YangMills.z3Mul ((0 : Int), (1 : Int)) ((0 : Int), (1 : Int)) = ((-1 : Int), (-1 : Int)) ∧ FRC.YangMills.z3Mul (FRC.YangMills.z3Mul ((0 : Int), (1 : Int)) ((0 : Int), (1 : Int))) ((0 : Int), (1 : Int)) = ((1 : Int), (0 : Int)) ∧ FRC.YangMills.z3Conj ((0 : Int), (1 : Int)) = ((-1 : Int), (-1 : Int))) ∧ (((0 : Int), (1 : Int)) ≠ ((1 : Int), (0 : Int)) ∧ (1 : Int) + (0 : Int) + (-1 : Int) = (0 : Int) ∧ (0 : Int) + (1 : Int) + (-1 : Int) = (0 : Int)) ∧ FRC.YangMills.z3Mul ((2 : Int), (0 : Int)) ((0 : Int), (1 : Int)) = ((0 : Int), (2 : Int)) ∧ FRC.YangMills.z3Mul ((0 : Int), (2 : Int)) ((0 : Int), (1 : Int)) = ((-2 : Int), (-2 : Int)) ∧ ((0 : Nat), (2 : Nat)).fst + ((0 : Nat), (1 : Nat)).fst = ((0 : Nat), (3 : Nat)).fst ∧ ((0 : Nat), (2 : Nat)).snd + ((0 : Nat), (1 : Nat)).snd = ((0 : Nat), (3 : Nat)).snd ∧ ((-2 : Int), (-2 : Int)).fst + ((-1 : Int), (-1 : Int)).fst = ((-3 : Int), (-3 : Int)).fst ∧ ((-2 : Int), (-2 : Int)).snd + ((-1 : Int), (-1 : Int)).snd = ((-3 : Int), (-3 : Int)).snd) ∧ (FRC.YangMills.cycleFacts (13 : Nat) (9 : FRC.Shell (13 : Nat)) (4 : FRC.Shell (13 : Nat)) (157 : Nat) = true ∧ FRC.YangMills.cycleMat (13 : Nat) (9 : FRC.Shell (13 : Nat)) (4 : FRC.Shell (13 : Nat)) ≠ FRC.YangMills.pmScal (1 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat)))) ∧ (FRC.YangMills.cycleFacts (173 : Nat) (166 : FRC.Shell (173 : Nat)) (160 : FRC.Shell (173 : Nat)) (29757 : Nat) = true ∧ FRC.YangMills.pmPow (64 : Nat) (FRC.YangMills.cycleMat (173 : Nat) (166 : FRC.Shell (173 : Nat)) (160 : FRC.Shell (173 : Nat))) (9919 : Nat) = FRC.YangMills.pmScal (FRC.YangMills.planePoint (173 : Nat) (86 : FRC.Shell (173 : Nat)) (155 : FRC.Shell (173 : Nat))) ∧ FRC.YangMills.planePoint (173 : Nat) (86 : FRC.Shell (173 : Nat)) (155 : FRC.Shell (173 : Nat)) ≠ (1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ FRC.YangMills.planePoint (173 : Nat) (86 : FRC.Shell (173 : Nat)) (155 : FRC.Shell (173 : Nat)) * FRC.YangMills.planePoint (173 : Nat) (86 : FRC.Shell (173 : Nat)) (155 : FRC.Shell (173 : Nat)) * FRC.YangMills.planePoint (173 : Nat) (86 : FRC.Shell (173 : Nat)) (155 : FRC.Shell (173 : Nat)) = (1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ FRC.YangMills.pmPow (64 : Nat) (FRC.YangMills.cycleMat (173 : Nat) (166 : FRC.Shell (173 : Nat)) (160 : FRC.Shell (173 : Nat))) (4251 : Nat) ≠ FRC.YangMills.pmScal (1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ FRC.YangMills.pmPow (64 : Nat) (FRC.YangMills.cycleMat (173 : Nat) (166 : FRC.Shell (173 : Nat)) (160 : FRC.Shell (173 : Nat))) (2289 : Nat) ≠ FRC.YangMills.pmScal (1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ FRC.YangMills.pmPow (64 : Nat) (FRC.YangMills.cycleMat (173 : Nat) (166 : FRC.Shell (173 : Nat)) (160 : FRC.Shell (173 : Nat))) (273 : Nat) ≠ FRC.YangMills.pmScal (1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat)))) ∧ FRC.YangMills.cycleFacts (1549 : Nat) (1275 : FRC.Shell (1549 : Nat)) (523 : FRC.Shell (1549 : Nat)) (2397853 : Nat) = true ∧ FRC.YangMills.cycleMat (1549 : Nat) (1275 : FRC.Shell (1549 : Nat)) (523 : FRC.Shell (1549 : Nat)) ≠ FRC.YangMills.pmScal (1 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) :=65  @FRC.Ledger.p4605666/-- 46:C17 (p46057) — The amplitude on $\SU(3,\F_2)$ takes the values $3$, $3\zeta_3$, $3\zeta_3^{2}$ on $64$ elements each and $0$ on $24$; the moments $\frac1{216}\sum w^{a}\bar w^{b}$ at $(1,1)$, $(3,0)$, $(2,2)$ are $8$, $24$, $72$, not the invariant counts $1$, $1$, $2$ (C3); two involutions with $w=3$ have a product with $w=0$: $w$ is no character over $\Q(\zeta_3)$. -/67theorem instance_amplitude_theorem : ((64 : Int) * ((3 : Int) + (0 : Int) + (-3 : Int)) = (0 : Int) ∧ (64 : Int) * ((0 : Int) + (3 : Int) + (-3 : Int)) = (0 : Int)) ∧ (FRC.YangMills.z3Norm ((3 : Int), (0 : Int)) = (9 : Int) ∧ FRC.YangMills.z3Norm ((0 : Int), (3 : Int)) = (9 : Int) ∧ FRC.YangMills.z3Norm ((-3 : Int), (-3 : Int)) = (9 : Int) ∧ FRC.YangMills.z3Norm ((0 : Int), (0 : Int)) = (0 : Int)) ∧ (FRC.YangMills.z3Mul (FRC.YangMills.z3Mul ((0 : Int), (3 : Int)) ((0 : Int), (3 : Int))) ((0 : Int), (3 : Int)) = ((27 : Int), (0 : Int)) ∧ FRC.YangMills.z3Mul (FRC.YangMills.z3Mul ((-3 : Int), (-3 : Int)) ((-3 : Int), (-3 : Int))) ((-3 : Int), (-3 : Int)) = ((27 : Int), (0 : Int))) ∧ ((192 : Nat) * (9 : Nat) = (8 : Nat) * (216 : Nat) ∧ (192 : Nat) * (27 : Nat) = (24 : Nat) * (216 : Nat) ∧ (192 : Nat) * (81 : Nat) = (72 : Nat) * (216 : Nat) ∧ (64 : Nat) + (64 : Nat) + (64 : Nat) + (24 : Nat) = (216 : Nat)) ∧ (8 : Nat) ≠ (1 : Nat) ∧ (24 : Nat) ≠ (1 : Nat) ∧ (72 : Nat) ≠ (2 : Nat) :=68  @FRC.Ledger.p4605769/-- 46:C18 (p46058) — The transfer tally on the instance: on $\SU(3,\F_2)$ the step of one plaquette, $(Kf)(x)=\langle w(x^{-1}y)f(y)\rangle_y$ (B3), has the eigenvalues $\frac23$, $\frac16$, $0$, $-\frac13$ with multiplicities $9$, $36$, $144$, $27$ ($K(3K+1)(6K-1)(3K-2)=0$, $\operatorname{tr}K=3$); the trivial channel is annihilated, $K\mathbf1=0$ (C16), so the tally has no ratio to it; with the eigenvalue $-\frac13$ it is not a positive operator. -/70theorem instance_transfer_theorem : (9 : Nat) + (36 : Nat) + (144 : Nat) + (27 : Nat) = (216 : Nat) ∧ ((2 : Nat) * (216 : Nat) = (3 : Nat) * (144 : Nat) ∧ (1 : Nat) * (216 : Nat) = (6 : Nat) * (36 : Nat) ∧ (-1 : Int) * (216 : Int) = (3 : Int) * (-72 : Int)) ∧ (4 : Int) * (9 : Int) + (1 : Int) * (36 : Int) + (0 : Int) * (144 : Int) + (-2 : Int) * (27 : Int) = (6 : Int) * (3 : Int) ∧ ((4 : Int) * (4 : Int) * (9 : Int) + (1 : Int) * (1 : Int) * (36 : Int) + (0 : Int) + (2 : Int) * (2 : Int) * (27 : Int) = (36 : Int) * (8 : Int) ∧ (8 : Nat) * (216 : Nat) = (192 : Nat) * (9 : Nat)) ∧ ((3 : Int) * (6 : Int) * (3 : Int) = (54 : Int) ∧ (3 : Int) * (6 : Int) * (-2 : Int) + (3 : Int) * (-1 : Int) * (3 : Int) + (1 : Int) * (6 : Int) * (3 : Int) = (-27 : Int) ∧ (3 : Int) * (-1 : Int) * (-2 : Int) + (1 : Int) * (6 : Int) * (-2 : Int) + (1 : Int) * (-1 : Int) * (3 : Int) = (-9 : Int) ∧ (1 : Int) * (-1 : Int) * (-2 : Int) = (2 : Int)) ∧ (-2 : Int) < (0 : Int) ∧ (-2 : Int) < (1 : Int) ∧ (1 : Int) < (4 : Int) :=71  @FRC.Ledger.p4605872/-- 46:C19 (p46061) — The transfer tally on the Subjects: for every prime power $q\ge3$, on each class type of A15, $w=\chi_{q^2-q+1}+\chi_{q^3+1}-\chi_{(q+1)^2(q-1)}$ (first members of the three families, A15), so the step $K$ (B3) has the eigenvalues $\frac1{q^2-q+1}$, $\frac1{q^3+1}$, $-\frac1{(q+1)^2(q-1)}$, $0$ with multiplicities the squared degrees; the frame's mean of $w$ is $0$, moment $3$; $K$ not positive. -/73theorem subject_spectrum_theorem : ((FRC.YangMills.su3Order (13 : Nat) = (811273008 : Int) ∧ FRC.YangMills.su3Order (173 : Nat) = (802332524681473968 : Int) ∧ FRC.YangMills.su3Order (1549 : Nat) = (33144476289365359469790000 : Int)) ∧ (FRC.YangMills.degs (13 : Nat) = ((157 : Int), (2198 : Int), (2352 : Int)) ∧ FRC.YangMills.degs (173 : Nat) = ((29757 : Int), (5177718 : Int), (5207472 : Int)) ∧ FRC.YangMills.degs (1549 : Nat) = ((2397853 : Int), (3716672150 : Int), (3719070000 : Int))) ∧ FRC.YangMills.spectrumOK (13 : Nat) = true ∧ FRC.YangMills.spectrumOK (173 : Nat) = true ∧ FRC.YangMills.spectrumOK (1549 : Nat) = true) ∧ FRC.YangMills.degreeSweep (2000 : Nat) = true :=74  @FRC.Ledger.p4606175/-- 46:C20 (p46062) — On C19's frames the ring's tally sums three characters' terms $\chi(h_1)\chi(h_2^{-1})$ on the boundary classes; one plaquette multiplies each by its eigenvalue; the largest, one character's, is $q+1$ times the next: the transfer tally's gap $1/(q+1)$. Modulo $\p$ the eigenvalues are $1$ and at fixed classes the reduced tally is the same for every length; the paired weight reduces to a residue of the shell. -/76theorem ring_gap_theorem : ((FRC.YangMills.gapOK (3 : Nat) = true ∧ FRC.YangMills.gapOK (4 : Nat) = true ∧ FRC.YangMills.gapOK (5 : Nat) = true ∧ FRC.YangMills.gapOK (7 : Nat) = true ∧ FRC.YangMills.gapOK (13 : Nat) = true ∧ FRC.YangMills.gapOK (173 : Nat) = true ∧ FRC.YangMills.gapOK (1549 : Nat) = true) ∧ (FRC.YangMills.degs (13 : Nat)).snd.fst = (14 : Int) * (FRC.YangMills.degs (13 : Nat)).fst ∧ (FRC.YangMills.degs (173 : Nat)).snd.fst = (174 : Int) * (FRC.YangMills.degs (173 : Nat)).fst ∧ (FRC.YangMills.degs (1549 : Nat)).snd.fst = (1550 : Int) * (FRC.YangMills.degs (1549 : Nat)).fst) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a1 a2 a3 b1 b2 b3 : FRC.Extension.Ext p ν), (FRC.YangMills.planeTally a1 a2 a3 b1 b2 b3).conj = FRC.YangMills.planeTally a1.conj a2.conj a3.conj b1.conj b2.conj b3.conj ∧ FRC.YangMills.planeTally a1 a2 a3 b1 b2 b3 * FRC.YangMills.planeTally a1.conj a2.conj a3.conj b1.conj b2.conj b3.conj = FRC.Extension.Ext.ofShell (FRC.YangMills.planeTally a1 a2 a3 b1 b2 b3).norm) ∧ ((2 : FRC.Shell (13 : Nat)) ^ (6 : Nat) + (1 : FRC.Shell (13 : Nat)) = (0 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (173 : Nat)) ^ (86 : Nat) + (1 : FRC.Shell (173 : Nat)) = (0 : FRC.Shell (173 : Nat)) ∧ (2 : FRC.Shell (1549 : Nat)) ^ (774 : Nat) + (1 : FRC.Shell (1549 : Nat)) = (0 : FRC.Shell (1549 : Nat))) ∧ ((2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (173 : Nat)) * (87 : FRC.Shell (173 : Nat)) = (1 : FRC.Shell (173 : Nat)) ∧ (2 : FRC.Shell (1549 : Nat)) * (775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Shell (1549 : Nat))) ∧ ((FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) * FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (-7 : FRC.Shell (13 : Nat)) * FRC.YangMills.planePoint (13 : Nat) (-1 : FRC.Shell (13 : Nat)) (0 : FRC.Shell (13 : Nat)) = (1 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ (FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat))).conj * FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (-7 : FRC.Shell (13 : Nat)) = (1 : FRC.Extension.Ext (13 : Nat) (2 : FRC.Shell (13 : Nat))) ∧ FRC.YangMills.planePoint (13 : Nat) (-1 : FRC.Shell (13 : Nat)) (0 : FRC.Shell (13 : Nat)) * FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) = (FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat))).conj ∧ FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (1 : FRC.Shell (13 : Nat)) + FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (-7 : FRC.Shell (13 : Nat)) = FRC.YangMills.planePoint (13 : Nat) (0 : FRC.Shell (13 : Nat)) (7 : FRC.Shell (13 : Nat))) ∧ (FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) * FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (-87 : FRC.Shell (173 : Nat)) * FRC.YangMills.planePoint (173 : Nat) (-1 : FRC.Shell (173 : Nat)) (0 : FRC.Shell (173 : Nat)) = (1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ (FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat))).conj * FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (-87 : FRC.Shell (173 : Nat)) = (1 : FRC.Extension.Ext (173 : Nat) (2 : FRC.Shell (173 : Nat))) ∧ FRC.YangMills.planePoint (173 : Nat) (-1 : FRC.Shell (173 : Nat)) (0 : FRC.Shell (173 : Nat)) * FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) = (FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat))).conj ∧ FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (1 : FRC.Shell (173 : Nat)) + FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (-87 : FRC.Shell (173 : Nat)) = FRC.YangMills.planePoint (173 : Nat) (0 : FRC.Shell (173 : Nat)) (87 : FRC.Shell (173 : Nat))) ∧ FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) * FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (-775 : FRC.Shell (1549 : Nat)) * FRC.YangMills.planePoint (1549 : Nat) (-1 : FRC.Shell (1549 : Nat)) (0 : FRC.Shell (1549 : Nat)) = (1 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) ∧ (FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat))).conj * FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (-775 : FRC.Shell (1549 : Nat)) = (1 : FRC.Extension.Ext (1549 : Nat) (2 : FRC.Shell (1549 : Nat))) ∧ FRC.YangMills.planePoint (1549 : Nat) (-1 : FRC.Shell (1549 : Nat)) (0 : FRC.Shell (1549 : Nat)) * FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) = (FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat))).conj ∧ FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (1 : FRC.Shell (1549 : Nat)) + FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (-775 : FRC.Shell (1549 : Nat)) = FRC.YangMills.planePoint (1549 : Nat) (0 : FRC.Shell (1549 : Nat)) (775 : FRC.Shell (1549 : Nat))) ∧ (FRC.YangMills.planeExample (13 : Nat) (7 : FRC.Shell (13 : Nat)) = FRC.YangMills.planePoint (13 : Nat) (12 : FRC.Shell (13 : Nat)) (2 : FRC.Shell (13 : Nat)) ∧ FRC.YangMills.planeExample (173 : Nat) (87 : FRC.Shell (173 : Nat)) = FRC.YangMills.planePoint (173 : Nat) (172 : FRC.Shell (173 : Nat)) (42 : FRC.Shell (173 : Nat)) ∧ FRC.YangMills.planeExample (1549 : Nat) (775 : FRC.Shell (1549 : Nat)) = FRC.YangMills.planePoint (1549 : Nat) (1548 : FRC.Shell (1549 : Nat)) (386 : FRC.Shell (1549 : Nat))) ∧ ((FRC.YangMills.planeExample (13 : Nat) (7 : FRC.Shell (13 : Nat))).im ≠ (0 : FRC.Shell (13 : Nat)) ∧ (FRC.YangMills.planeExample (173 : Nat) (87 : FRC.Shell (173 : Nat))).im ≠ (0 : FRC.Shell (173 : Nat)) ∧ (FRC.YangMills.planeExample (1549 : Nat) (775 : FRC.Shell (1549 : Nat))).im ≠ (0 : FRC.Shell (1549 : Nat))) ∧ ((4 : FRC.Shell (13 : Nat)) * (2 : FRC.Shell (13 : Nat)) + (5 : FRC.Shell (13 : Nat)) = (0 : FRC.Shell (13 : Nat)) ∧ (4 : FRC.Shell (173 : Nat)) * (42 : FRC.Shell (173 : Nat)) + (5 : FRC.Shell (173 : Nat)) = (0 : FRC.Shell (173 : Nat)) ∧ (4 : FRC.Shell (1549 : Nat)) * (386 : FRC.Shell (1549 : Nat)) + (5 : FRC.Shell (1549 : Nat)) = (0 : FRC.Shell (1549 : Nat))) ∧ ((FRC.YangMills.planeExample (13 : Nat) (7 : FRC.Shell (13 : Nat))).norm = (6 : FRC.Shell (13 : Nat)) ∧ (FRC.YangMills.planeExample (173 : Nat) (87 : FRC.Shell (173 : Nat))).norm = (106 : FRC.Shell (173 : Nat)) ∧ (FRC.YangMills.planeExample (1549 : Nat) (775 : FRC.Shell (1549 : Nat))).norm = (966 : FRC.Shell (1549 : Nat))) ∧ (8 : FRC.Shell (13 : Nat)) * (6 : FRC.Shell (13 : Nat)) + (17 : FRC.Shell (13 : Nat)) = (0 : FRC.Shell (13 : Nat)) ∧ (8 : FRC.Shell (173 : Nat)) * (106 : FRC.Shell (173 : Nat)) + (17 : FRC.Shell (173 : Nat)) = (0 : FRC.Shell (173 : Nat)) ∧ (8 : FRC.Shell (1549 : Nat)) * (966 : FRC.Shell (1549 : Nat)) + (17 : FRC.Shell (1549 : Nat)) = (0 : FRC.Shell (1549 : Nat)) :=77  @FRC.Ledger.p4606278/-- 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$. -/79theorem spectrum_in_two_pi : ((13 : Nat) = (2 : Nat) * (6 : Nat) + (1 : Nat) ∧ (173 : Nat) = (2 : Nat) * (86 : Nat) + (1 : Nat) ∧ (1549 : Nat) = (2 : Nat) * (774 : Nat) + (1 : Nat)) ∧ ((FRC.YangMills.degs (13 : Nat)).fst = (4 : Int) * (6 : Int) * (6 : Int) + (2 : Int) * (6 : Int) + (1 : Int) ∧ (FRC.YangMills.degs (173 : Nat)).fst = (4 : Int) * (86 : Int) * (86 : Int) + (2 : Int) * (86 : Int) + (1 : Int) ∧ (FRC.YangMills.degs (1549 : Nat)).fst = (4 : Int) * (774 : Int) * (774 : Int) + (2 : Int) * (774 : Int) + (1 : Int)) ∧ ((FRC.YangMills.degs (13 : Nat)).snd.fst = ((2 : Int) * (6 : Int) + (2 : Int)) * (FRC.YangMills.degs (13 : Nat)).fst ∧ (FRC.YangMills.degs (173 : Nat)).snd.fst = ((2 : Int) * (86 : Int) + (2 : Int)) * (FRC.YangMills.degs (173 : Nat)).fst ∧ (FRC.YangMills.degs (1549 : Nat)).snd.fst = ((2 : Int) * (774 : Int) + (2 : Int)) * (FRC.YangMills.degs (1549 : Nat)).fst) ∧ ((FRC.YangMills.degs (13 : Nat)).snd.snd = (8 : Int) * (6 : Int) * ((6 : Int) + (1 : Int)) * ((6 : Int) + (1 : Int)) ∧ (FRC.YangMills.degs (173 : Nat)).snd.snd = (8 : Int) * (86 : Int) * ((86 : Int) + (1 : Int)) * ((86 : Int) + (1 : Int)) ∧ (FRC.YangMills.degs (1549 : Nat)).snd.snd = (8 : Int) * (774 : Int) * ((774 : Int) + (1 : Int)) * ((774 : Int) + (1 : Int))) ∧ ((2 : Nat) * (6 : Nat) + (2 : Nat)) % (13 : Nat) = (1 : Nat) ∧ ((2 : Nat) * (86 : Nat) + (2 : Nat)) % (173 : Nat) = (1 : Nat) ∧ ((2 : Nat) * (774 : Nat) + (2 : Nat)) % (1549 : Nat) = (1 : Nat) :=80  @FRC.Ledger.p4606481/-- 46:C22 (p46065) — The product channels: where $3$ is invertible the frame fixes $A_n=\sum_k(-1)^{n-k}\binom nkM(k,k)$ dimensions of $\mathbf8^{\otimes n}$. On every Subject two mesons and three gluons have $d=2$ and $\p^{2}+1$ invariant lines, a meson with a glueball $d=3$, two glueballs $d=8$. On $\SU(3,\F_2)$ three gluons have $d=7$ and two glueballs $d=57$: the instance departs beyond degree $4$. -/82theorem product_channels : ((1 : Int) - (1 : Int) = (0 : Int) ∧ (2 : Int) - (2 : Int) * (1 : Int) + (1 : Int) = (1 : Int) ∧ (6 : Int) - (3 : Int) * (2 : Int) + (3 : Int) * (1 : Int) - (1 : Int) = (2 : Int) ∧ (23 : Int) - (4 : Int) * (6 : Int) + (6 : Int) * (2 : Int) - (4 : Int) * (1 : Int) + (1 : Int) = (8 : Int)) ∧ ((11 : Int) - (3 : Int) * (2 : Int) + (3 : Int) * (1 : Int) - (1 : Int) = (7 : Int) ∧ (92 : Int) - (4 : Int) * (11 : Int) + (6 : Int) * (2 : Int) - (4 : Int) * (1 : Int) + (1 : Int) = (57 : Int)) ∧ ((13 : Nat) * (13 : Nat) + (1 : Nat) = (170 : Nat) ∧ (173 : Nat) * (173 : Nat) + (1 : Nat) = (29930 : Nat) ∧ (1549 : Nat) * (1549 : Nat) + (1 : Nat) = (2399402 : Nat)) ∧ (((13 : Nat) * (13 : Nat) - (1 : Nat)) * (170 : Nat) = (13 : Nat) * (13 : Nat) * (13 : Nat) * (13 : Nat) - (1 : Nat) ∧ (13 : Nat) * (13 : Nat) * (13 : Nat) * (13 : Nat) + (13 : Nat) * (13 : Nat) + (1 : Nat) = (28731 : Nat)) ∧ (((4 : Nat) ^ (2 : Nat) - (1 : Nat)) / (3 : Nat) = (5 : Nat) ∧ ((4 : Nat) ^ (7 : Nat) - (1 : Nat)) / (3 : Nat) = (5461 : Nat) ∧ ((4 : Nat) ^ (8 : Nat) - (1 : Nat)) / (3 : Nat) = (21845 : Nat)) ∧ (8 : Nat) ≤ (2 : Nat) * (13 : Nat) - (1 : Nat) :=83  @FRC.Ledger.p4606584/-- 46:C23 (p46066) — The tally with the same boundary links at every step, of the eigenvalues $g^{\pm j},1$ and $g^{\pm k},1$: the boundary classes of C20 move with the length $n$. On every Subject it reads $1+g^{(j+k)n}+g^{-(j+k)n}+g^{(j-k)n}+g^{-(j-k)n}$ at every regular length, with stated values at the others and the least period $(\p-1)/\gcdop(j,k,\p-1)$. Every exponent is a multiple of $\gcdop(j,k,\p-1)$; the three multipliers add none. -/85theorem uniform_boundary : ((2 : Nat) * (7 : Nat) % (13 : Nat) = (1 : Nat) ∧ (4 : Nat) * (10 : Nat) % (13 : Nat) = (1 : Nat) ∧ (2 : Nat) * (87 : Nat) % (173 : Nat) = (1 : Nat) ∧ (4 : Nat) * (130 : Nat) % (173 : Nat) = (1 : Nat) ∧ (2 : Nat) * (775 : Nat) % (1549 : Nat) = (1 : Nat) ∧ (4 : Nat) * (1162 : Nat) % (1549 : Nat) = (1 : Nat)) ∧ FRC.YangMills.ubValues (13 : Nat) (2 : Nat) (7 : Nat) (4 : Nat) (10 : Nat) (12 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = [(10 : Nat), (0 : Nat), (0 : Nat), (2 : Nat), (5 : Nat), (12 : Nat), (5 : Nat), (2 : Nat), (0 : Nat), (0 : Nat), (10 : Nat), (3 : Nat)] ∧ (FRC.YangMills.ubSweep (13 : Nat) (2 : Nat) (7 : Nat) (4 : Nat) (10 : Nat) (12 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = true ∧ FRC.YangMills.ubSweep (173 : Nat) (2 : Nat) (87 : Nat) (4 : Nat) (130 : Nat) (172 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = true ∧ FRC.YangMills.ubSweep (1549 : Nat) (2 : Nat) (775 : Nat) (4 : Nat) (1162 : Nat) (1548 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = true) ∧ (FRC.YangMills.ubOthers (13 : Nat) (2 : Nat) (4 : Nat) (12 : Nat) (0 : Nat) (1 : Nat) (1 : Nat) = [(3 : Nat), (6 : Nat), (9 : Nat), (12 : Nat)] ∧ FRC.YangMills.ubOthers (173 : Nat) (2 : Nat) (4 : Nat) (172 : Nat) (0 : Nat) (1 : Nat) (1 : Nat) = [(43 : Nat), (86 : Nat), (129 : Nat), (172 : Nat)] ∧ FRC.YangMills.ubOthers (1549 : Nat) (2 : Nat) (4 : Nat) (1548 : Nat) (0 : Nat) (1 : Nat) (1 : Nat) = [(387 : Nat), (774 : Nat), (1161 : Nat), (1548 : Nat)]) ∧ FRC.YangMills.ubTally (13 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = (3 : Nat) ∧ FRC.YangMills.ubTally (173 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = (3 : Nat) ∧ FRC.YangMills.ubTally (1549 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = (3 : Nat) :=86  @FRC.Ledger.p4606687/-- 46:C24 (p46067) — What a reading keeps of the window: the counts of C15 are equal as integers, and on $\F_{13}$ the pair $(1,13)$ has $2574=13\cdot198$ independent invariants and reads $0$, with $52$ of the $117$ nonzero counts. The coefficients of C14 below $\stf^{\p}$ have values in the Subject's arithmetic; from $\stf^{\p}$ on they contain a factorial that reads $0$, and the paper states no reading. -/88theorem readings_of_window : ((6227020800 : Nat) = (2574 : Nat) * ((840 : Nat) * (120 : Nat) * (24 : Nat)) ∧ (2574 : Nat) = (13 : Nat) * (198 : Nat)) ∧ (FRC.YangMills.wrFact (13 : Nat) (12 : Nat) = (12 : Nat) ∧ FRC.YangMills.wrFact (173 : Nat) (172 : Nat) = (172 : Nat) ∧ FRC.YangMills.wrFact (1549 : Nat) (1548 : Nat) = (1548 : Nat)) ∧ ((2 : Nat) * (7 : Nat) % (13 : Nat) = (1 : Nat) ∧ (3 : Nat) * (9 : Nat) % (13 : Nat) = (1 : Nat) ∧ (2 : Nat) * (87 : Nat) % (173 : Nat) = (1 : Nat) ∧ (3 : Nat) * (58 : Nat) % (173 : Nat) = (1 : Nat) ∧ (2 : Nat) * (775 : Nat) % (1549 : Nat) = (1 : Nat) ∧ (3 : Nat) * (1033 : Nat) % (1549 : Nat) = (1 : Nat)) ∧ FRC.YangMills.wrFact (13 : Nat) (13 : Nat) = (0 : Nat) ∧ FRC.YangMills.wrFact (173 : Nat) (173 : Nat) = (0 : Nat) ∧ FRC.YangMills.wrFact (1549 : Nat) (1549 : Nat) = (0 : Nat) :=89  @FRC.Ledger.p4606790/-- 46:C25 (p46068) — Three rings of $n$ plaquettes on $n$ common links. For every prime power $q\ge3$ the tally sums $\chi_i(h_1)\chi_j(h_2)\chi_k(h_3)$ on the boundary classes with the invariant counts of the triples of characters; the mean of $w^{3}$ is $6$. On every Subject, on split classes of the eigenvalues $x^{\pm1},1$, $y^{\pm1},1$, $z^{\pm1},1$, it reads $1+N_{122}(c(x)c(y)+c(x)c(z)+c(y)c(z))$, $c(m)=m+m^{-1}$, $N_{122}=2$ or $4$. -/91theorem three_rings : ((8 : Nat) * (5 : Nat) % (13 : Nat) = (1 : Nat) ∧ (8 : Nat) * (65 : Nat) % (173 : Nat) = (1 : Nat) ∧ (8 : Nat) * (581 : Nat) % (1549 : Nat) = (1 : Nat)) ∧ ((13 : Nat) % (13 : Nat) = (0 : Nat) ∧ (3 : Nat) * (173 : Nat) % (173 : Nat) = (0 : Nat) ∧ (1549 : Nat) % (1549 : Nat) = (0 : Nat)) ∧ FRC.YangMills.trValues (13 : Nat) (2 : Nat) (2 : Nat) (7 : Nat) (4 : Nat) (10 : Nat) (8 : Nat) (5 : Nat) (12 : Nat) (0 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = [((1 : Nat), (6 : Nat)), ((5 : Nat), (9 : Nat)), ((7 : Nat), (9 : Nat)), ((11 : Nat), (6 : Nat))] ∧ (FRC.YangMills.trSweep (13 : Nat) (2 : Nat) (13 : Nat) (2 : Nat) (7 : Nat) (4 : Nat) (10 : Nat) (8 : Nat) (5 : Nat) (12 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = true ∧ FRC.YangMills.trSweep (173 : Nat) (4 : Nat) (519 : Nat) (2 : Nat) (87 : Nat) (4 : Nat) (130 : Nat) (8 : Nat) (65 : Nat) (172 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = true ∧ FRC.YangMills.trSweep (1549 : Nat) (2 : Nat) (1549 : Nat) (2 : Nat) (775 : Nat) (4 : Nat) (1162 : Nat) (8 : Nat) (581 : Nat) (1548 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) = true) ∧ FRC.YangMills.trReading (13 : Nat) (2 : Nat) (2 : Nat) (7 : Nat) (4 : Nat) (10 : Nat) (8 : Nat) (5 : Nat) = (6 : Nat) ∧ FRC.YangMills.trReading (173 : Nat) (4 : Nat) (2 : Nat) (87 : Nat) (4 : Nat) (130 : Nat) (8 : Nat) (65 : Nat) = (25 : Nat) ∧ FRC.YangMills.trReading (1549 : Nat) (2 : Nat) (2 : Nat) (775 : Nat) (4 : Nat) (1162 : Nat) (8 : Nat) (581 : Nat) = (616 : Nat) :=92  @FRC.Ledger.p4606893/-- 46:C26 (p46072) — The series on the shell: $d_R\,c_R=\sum_kh_k\stf^{k}/k!$ with integers $h_k$ ($0,1,1,0,-5,-15,21,413$ for $c_3$) from a recursion without division, on residues at every order. In the divided-power algebra on a Subject $f(0)=0$ gives $f^{\p}=0$, so a reading that respects sums and products sends $\stf$ to $0$; at channel unity on $\F_{13}$ the truncated sum reads $6$, the quotient of truncated sums $4$. -/94theorem series_on_shell : (FRC.YangMills.hurwitzH [(0 : Int), (1 : Int), (1 : Int), (6 : Int), (15 : Int), (65 : Int), (231 : Int), (973 : Int)] [(1 : Int), (0 : Int), (2 : Int), (2 : Int), (12 : Int), (30 : Int), (130 : Int), (462 : Int)] (8 : Nat) = [(0 : Int), (1 : Int), (1 : Int), (0 : Int), (-5 : Int), (-15 : Int), (21 : Int), (413 : Int)] ∧ FRC.YangMills.hurwitzH [(0 : Int), (0 : Int), (2 : Int), (4 : Int), (24 : Int), (80 : Int), (372 : Int), (1512 : Int)] [(1 : Int), (0 : Int), (2 : Int), (2 : Int), (12 : Int), (30 : Int), (130 : Int), (462 : Int)] (8 : Nat) = [(0 : Int), (0 : Int), (2 : Int), (4 : Int), (0 : Int), (-40 : Int), (-148 : Int), (252 : Int)]) ∧ (FRC.YangMills.wrFact (13 : Nat) (13 : Nat) = (0 : Nat) ∧ FRC.YangMills.wrFact (173 : Nat) (173 : Nat) = (0 : Nat) ∧ FRC.YangMills.wrFact (1549 : Nat) (1549 : Nat) = (0 : Nat)) ∧ List.foldl (fun s x => s + x) (0 : FRC.Shell (13 : Nat)) (FRC.YangMills.c3Series [(1 : Nat), (0 : Nat), (2 : Nat), (2 : Nat), (12 : Nat), (30 : Nat), (130 : Nat), (462 : Nat), (1946 : Nat), (7980 : Nat), (34776 : Nat), (153120 : Nat), (694056 : Nat)] [(0 : Nat), (1 : Nat), (1 : Nat), (6 : Nat), (15 : Nat), (65 : Nat), (231 : Nat), (973 : Nat), (3990 : Nat), (17388 : Nat), (76560 : Nat), (347028 : Nat), (1597167 : Nat)] (13 : Nat)) = (6 : FRC.Shell (13 : Nat)) ∧ (FRC.YangMills.truncSums [(1 : Nat), (0 : Nat), (2 : Nat), (2 : Nat), (12 : Nat), (30 : Nat), (130 : Nat), (462 : Nat), (1946 : Nat), (7980 : Nat), (34776 : Nat), (153120 : Nat), (694056 : Nat)] [(0 : Nat), (1 : Nat), (1 : Nat), (6 : Nat), (15 : Nat), (65 : Nat), (231 : Nat), (973 : Nat), (3990 : Nat), (17388 : Nat), (76560 : Nat), (347028 : Nat), (1597167 : Nat)] (13 : Nat)).fst * FRC.YangMills.invS (FRC.YangMills.truncSums [(1 : Nat), (0 : Nat), (2 : Nat), (2 : Nat), (12 : Nat), (30 : Nat), (130 : Nat), (462 : Nat), (1946 : Nat), (7980 : Nat), (34776 : Nat), (153120 : Nat), (694056 : Nat)] [(0 : Nat), (1 : Nat), (1 : Nat), (6 : Nat), (15 : Nat), (65 : Nat), (231 : Nat), (973 : Nat), (3990 : Nat), (17388 : Nat), (76560 : Nat), (347028 : Nat), (1597167 : Nat)] (13 : Nat)).snd = (4 : FRC.Shell (13 : Nat)) :=95  @FRC.Ledger.p4607296/-- 46:X1 (p46018) — Why the gluon is massless yet never seen alone: under B1 a gluon is drive-invariant (massless, A6) and its space has no frame-invariant line (C1, C3), so no registration singles it out. The row explicates the form of the confinement rule; it does not derive confinement. -/97theorem gluon_massless_unregistered : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν a b r : FRC.Shell p}, ¬FRC.Shell.Frame.IsSquare ν → a * a + -(ν * (b * b)) = (1 : FRC.Shell p) → b ≠ (0 : FRC.Shell p) → r * r + -((a + a) * r) + (1 : FRC.Shell p) = (0 : FRC.Shell p) → False) ∧ FRC.YangMills.mult (1 : Nat) (1 : Nat) = (1 : Nat) ∧ FRC.YangMills.mult (1 : Nat) (1 : Nat) - (1 : Nat) = (0 : Nat) ∧ FRC.YangMills.lookup ((1 : Nat), (1 : Nat)) (FRC.YangMills.powers3 (2 : Nat)) = (0 : Nat) ∧ FRC.YangMills.lookup ((1 : Nat), (1 : Nat)) (FRC.YangMills.tensor3 [(((0 : Nat), (1 : Nat)), (1 : Nat))]) = (1 : Nat) :=98  @FRC.Ledger.p4601899/-- 46:X2 (p46019) — Why only colour singlets are registered: under B1 each channel of the unitary frame, a space whose frame-fixed subspace is a line, has exactly one frame-invariant line, and the hadron paper's series of such channels ends at the glueball (C3); products whose fixed subspace is larger are sums of channels, counted in C22. -/100theorem singlets_only : (FRC.YangMills.mult (3 : Nat) (0 : Nat) = (1 : Nat) ∧ FRC.YangMills.mult (1 : Nat) (1 : Nat) = (1 : Nat) ∧ FRC.YangMills.mult (2 : Nat) (2 : Nat) - (2 : Nat) * FRC.YangMills.mult (1 : Nat) (1 : Nat) + (1 : Nat) = (1 : Nat)) ∧ FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) - (6 : Int) = (0 : Int) ∧ FRC.Hadrons.moment6 (3 : Nat) (0 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) = (6 : Int) * (1 : Int) ∧ FRC.Hadrons.moment6 (2 : Nat) (2 : Nat) - (2 : Int) * FRC.Hadrons.moment6 (1 : Nat) (1 : Nat) + (6 : Int) = (6 : Int) * (1 : Int) :=101  @FRC.Ledger.p46019102/-- 46:X4 (p46021) — Why the colour factors take the values LEP measured: they are the second moments of the unitary frame's torus exponents (C4), and the abelian alternative $C_A=0$, $C_F=1$ lies outside the measured brackets (A2). -/103theorem casimirs_are_measured : ((3 : Int) * (3 : Int) - (1 : Int) = (8 : Int) ∧ (6 : Nat) * (4 : Nat) = (3 : Nat) * (8 : Nat) ∧ (2 : Int) * (3 : Int) * (3 : Int) = (18 : Int) ∧ (8 : Nat) * (9 : Nat) = (4 : Nat) * (18 : Nat) ∧ (2 : Nat) * (1 : Nat) = (2 : Nat)) ∧ (268 : Nat) ≤ (300 : Nat) ∧ (300 : Nat) ≤ (310 : Nat) ∧ (3 : Nat) * (121 : Nat) ≤ (400 : Nat) ∧ (400 : Nat) ≤ (3 : Nat) * (139 : Nat) ∧ (4 : Nat) * (211 : Nat) ≤ (900 : Nat) ∧ (900 : Nat) ≤ (4 : Nat) * (233 : Nat) ∧ (0 : Nat) < (268 : Nat) ∧ (100 : Nat) < (121 : Nat) :=104  @FRC.Ledger.p46021105/-- 46:P1 (p46023) — The colour factors of the strong interaction are $C_A=3$, $C_F=\frac43$, $C_A/C_F=\frac94$ (C4). Falsifier: a measured $C_A/C_F$ outside $\frac94$ beyond its error. Confrontation: LEP's $2.89(21)$, $1.30(9)$, $2.22(11)$ (A2), each within one standard deviation. -/106theorem colour_factors_prediction : ((3 : Int) * (3 : Int) - (1 : Int) = (8 : Int) ∧ (6 : Nat) * (4 : Nat) = (3 : Nat) * (8 : Nat) ∧ (2 : Int) * (3 : Int) * (3 : Int) = (18 : Int) ∧ (8 : Nat) * (9 : Nat) = (4 : Nat) * (18 : Nat) ∧ (2 : Nat) * (1 : Nat) = (2 : Nat)) ∧ (268 : Nat) ≤ (300 : Nat) ∧ (300 : Nat) ≤ (310 : Nat) ∧ (3 : Nat) * (121 : Nat) ≤ (400 : Nat) ∧ (400 : Nat) ≤ (3 : Nat) * (139 : Nat) ∧ (4 : Nat) * (211 : Nat) ≤ (900 : Nat) ∧ (900 : Nat) ≤ (4 : Nat) * (233 : Nat) ∧ (0 : Nat) < (268 : Nat) ∧ (100 : Nat) < (121 : Nat) :=107  @FRC.Ledger.p46023108/-- 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$. -/109theorem running_prediction : (FRC.YangMills.alphaTau.within (FRC.YangMills.WF.frac (2785 : Int) (10000 : Nat)) (FRC.YangMills.WF.frac (2795 : Int) (10000 : Nat)) = true ∧ (FRC.YangMills.WF.frac (215 : Int) (100 : Nat)).lt (((FRC.YangMills.WF.frac (312 : Int) (1000 : Nat)).sub FRC.YangMills.alphaTau.snd).div (FRC.YangMills.WF.frac (15 : Int) (1000 : Nat))) = true ∧ (((FRC.YangMills.WF.frac (312 : Int) (1000 : Nat)).sub FRC.YangMills.alphaTau.fst).div (FRC.YangMills.WF.frac (15 : Int) (1000 : Nat))).lt (FRC.YangMills.WF.frac (225 : Int) (100 : Nat)) = true ∧ FRC.YangMills.threeB0 (5 : Nat) = (23 : Int) ∧ FRC.YangMills.threeB0 (4 : Nat) = (25 : Int)) ∧ FRC.YangMills.threeB0 (3 : Nat) = (27 : Int) ∧ FRC.YangMills.threeB0 (4 : Nat) = (25 : Int) ∧ FRC.YangMills.threeB0 (5 : Nat) = (23 : Int) ∧ FRC.YangMills.threeB0 (6 : Nat) = (21 : Int) :=110  @FRC.Ledger.p46024111/-- 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. -/112theorem radial_ratio_prediction : (1432 : Nat) ≤ (1491 : Nat) ∧ (1491 : Nat) ≤ (1656 : Nat) ∧ (2 : Nat) * ((1544 : Nat) - (1491 : Nat)) < (112 : Nat) ∧ (174 : Nat) * (234 : Nat) < (408 : Nat) * (100 : Nat) ∧ (409 : Nat) * (100 : Nat) < (176 : Nat) * (233 : Nat) ∧ (1656 : Nat) < (1740 : Nat) ∧ (14 : Nat) * (16 : Nat) < (1720 : Nat) - (1491 : Nat) ∧ (10 : Nat) * (227 : Nat) < (17195 : Nat) - (14915 : Nat) ∧ (1748 : Nat) - (1720 : Nat) < (2 : Nat) * (16 : Nat) ∧ (1491 : Nat) * (939 : Nat) < (1440 : Nat) * (1000 : Nat) ∧ (1440 : Nat) * (1000 : Nat) * (100 : Nat) < (1491 : Nat) * (939 : Nat) * (103 : Nat) :=113  @FRC.Ledger.p46043114/-- 46:P4 (p46076) — No state of residue $0$ is registered in isolation: on every Subject the triplet and the adjoint of the unitary frame have no invariant line (A9), so there is no free quark and no free gluon. Falsifier: a confirmed free particle that carries colour, such as a fractional electric charge. Confrontation: the searches for free quarks are negative (A19). -/115theorem no_free_quark_or_gluon : FRC.YangMills.mult (1 : Nat) (0 : Nat) = (0 : Nat) ∧ FRC.YangMills.mult (0 : Nat) (1 : Nat) = (0 : Nat) ∧ FRC.YangMills.mult (1 : Nat) (1 : Nat) - (1 : Nat) = (0 : Nat) :=116  @FRC.Ledger.p46076117-- end ledger predicates118119end FRC.YangMills120