import FrcCore.Theme.YangMills

/-!
# FrcCore.Keys.Yangmills — the keyed theorems of the yangmills theme (ledger migration, task LM19)

One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem
that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration
`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).
-/

namespace FRC.Ledger

-- Keys of the yangmills theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)
/-- p46010 — 46:C1. 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. -/
theorem p46010 : (∀ {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)) :=
  And.intro @FRC.YangMills.no_shell_eigenvalue (And.intro @FRC.YangMills.scalar_of_im_zero (@FRC.YangMills.split_fixed_lines))
/-- p46011 — 46:C2. 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. -/
theorem p46011 : (∀ (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) :=
  And.intro @FRC.YangMills.centre_sweep (And.intro @FRC.YangMills.lab_centres (And.intro @FRC.YangMills.full_centre_sweep (@FRC.YangMills.carrier_triality)))
/-- p46012 — 46:C3. 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$). -/
theorem p46012 : 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) :=
  @FRC.YangMills.glueball_singlet
/-- p46013 — 46:C4. 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. -/
theorem p46013 : ((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)) :=
  And.intro @FRC.YangMills.casimirs (@FRC.YangMills.casimir_exponents)
/-- p46014 — 46:C5. 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$. -/
theorem p46014 : (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) :=
  And.intro @FRC.YangMills.b0_values (And.intro @FRC.YangMills.b0_pos (And.intro @FRC.YangMills.b0_seventeen (@FRC.YangMills.b0_neg)))
/-- p46015 — 46:C6. 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. -/
theorem p46015 : (∀ {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))) :=
  And.intro @FRC.YangMills.drive_exponent (And.intro @FRC.YangMills.drive_exponent_unique (@FRC.YangMills.drive_exponent_add))
/-- p46016 — 46:C7. 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}$. -/
theorem p46016 : (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 :=
  And.intro @FRC.YangMills.moments (And.intro @FRC.YangMills.c3_fractions (And.intro @FRC.YangMills.c3_readback (@FRC.YangMills.c2_lab)))
/-- p46018 — 46:X1. 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. -/
theorem p46018 : (∀ {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) :=
  And.intro @FRC.YangMills.no_shell_eigenvalue (@FRC.YangMills.adjoint_no_invariant)
/-- p46019 — 46:X2. 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. -/
theorem p46019 : (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) :=
  And.intro @FRC.YangMills.residue_series_pieri (@FRC.YangMills.glueball_singlet)
/-- p46021 — 46:X4. 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). -/
theorem p46021 : ((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) :=
  And.intro @FRC.YangMills.casimirs (@FRC.YangMills.colour_factors_within)
/-- p46023 — 46:P1. 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. -/
theorem p46023 : ((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) :=
  And.intro @FRC.YangMills.casimirs (@FRC.YangMills.colour_factors_within)
/-- p46024 — 46:P2. [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$. -/
theorem p46024 : (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) :=
  And.intro @FRC.YangMills.running_one_loop (@FRC.YangMills.b0_values)
/-- p46030 — 46:C9. 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. -/
theorem p46030 : 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) :=
  @FRC.YangMills.adjoint_two_sheets
/-- p46034 — 46:A9. 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$). -/
theorem p46034 : (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) :=
  @FRC.YangMills.frame_root_elements
/-- p46036 — 46:C12. [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. -/
theorem p46036 : ((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) :=
  @FRC.YangMills.wrap_family
/-- p46037 — 46:C10. [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). -/
theorem p46037 : 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 :=
  @FRC.YangMills.herbst_comparison
/-- p46041 — 46:C13. 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). -/
theorem p46041 : ((-((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)) :=
  And.intro @FRC.YangMills.spin_traces (And.intro @FRC.YangMills.faulhaber_third (And.intro @FRC.YangMills.faulhaber_residues (And.intro @FRC.YangMills.complete_cycle_vanishes (@FRC.YangMills.hughes_nielsen_sum))))
/-- p46043 — 46:P3. [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. -/
theorem p46043 : (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) :=
  @FRC.YangMills.radial_ratio
/-- p46051 — 46:C14. 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$. -/
theorem p46051 : ((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 :=
  @FRC.YangMills.series_window
/-- p46053 — 46:C15. 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$. -/
theorem p46053 : 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) :=
  @FRC.YangMills.frame_window
/-- p46056 — 46:C16. 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). -/
theorem p46056 : (((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))) :=
  And.intro @FRC.YangMills.spectral_amplitude (@FRC.YangMills.frame_cycle_trace)
/-- p46057 — 46:C17. 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)$. -/
theorem p46057 : ((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) :=
  @FRC.YangMills.instance_amplitude
/-- p46058 — 46:C18. 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. -/
theorem p46058 : (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) :=
  @FRC.YangMills.instance_transfer
/-- p46061 — 46:C19. 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. -/
theorem p46061 : ((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 :=
  And.intro @FRC.YangMills.subject_spectrum (@FRC.YangMills.degree_identity)
/-- p46062 — 46:C20. 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. -/
theorem p46062 : ((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)) :=
  And.intro @FRC.YangMills.ring_gap (And.intro @FRC.YangMills.ring_tally_plane (@FRC.YangMills.ring_tally_outside_shell))
/-- p46064 — 46:C21. 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$. -/
theorem p46064 : ((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) :=
  @FRC.YangMills.spectrum_in_pi
/-- p46065 — 46:C22. 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$. -/
theorem p46065 : ((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) :=
  @FRC.YangMills.product_channel_counts
/-- p46066 — 46:C23. 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. -/
theorem p46066 : ((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) :=
  @FRC.YangMills.uniform_boundary_tally
/-- p46067 — 46:C24. 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. -/
theorem p46067 : ((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) :=
  @FRC.YangMills.window_readings
/-- p46068 — 46:C25. 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$. -/
theorem p46068 : ((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) :=
  @FRC.YangMills.three_rings_reading
/-- p46071 — 46:C11. [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$. -/
theorem p46071 : 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 :=
  @FRC.YangMills.plaquette_cells
/-- p46072 — 46:C26. 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$. -/
theorem p46072 : (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)) :=
  @FRC.YangMills.shell_series_readings
/-- p46076 — 46:P4. 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). -/
theorem p46076 : 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) :=
  @FRC.YangMills.residue_zero_states
-- end keys

end FRC.Ledger