Fields.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Fields3import FrcLedger.Keys.Chart45/-!6# 27-fields — the chart readings on Mathlib (16 October 2026)78The paper module of *Gauge Interactions over Finite Holographic Substrate* (tree `27-fields-20260625`) on Mathlib: every9declaration is the chart theme's (`FrcLedger/Theme/Fields.lean`), under the paper's name — the `M`-th roots of unity10(27:C1), the Wilson weight (27:C1), the `2T` area law (27:C1, C7, X7), the Fermi constant (27:C6), and the chart readings of the exclusion rows P3, P4, P5 (17 October 2026). Classical (tier 2). The finite content is the core's (`FrcCore/Fields.lean`).11-/1213namespace FRC.Fields1415/-! ## Old names (16 October 2026): every declaration of this module is an alias of the chart theme's (`FRC.FieldsML`,16`FrcLedger/Theme/Fields.lean`), under the paper's name -/1718/-- 27:C1 — the phase cycle inside `U(1)` (`FieldsML.roots_inclusion`). -/19theorem roots_inclusion (M : ℕ) (hM : M ≠ 0) :20    IsPrimitiveRoot (Complex.exp (2 * Real.pi * Complex.I / M)) M ∧21    (∀ j k : ℕ, Complex.exp (2 * Real.pi * Complex.I / M) ^ (j + k) =22      Complex.exp (2 * Real.pi * Complex.I / M) ^ j * Complex.exp (2 * Real.pi * Complex.I / M) ^ k) ∧23    (∀ j k : ℕ, j < M → k < M →24      Complex.exp (2 * Real.pi * Complex.I / M) ^ j = Complex.exp (2 * Real.pi * Complex.I / M) ^ k → j = k) ∧25    (∀ k : ℕ, (Complex.exp (2 * Real.pi * Complex.I / M) ^ k) ^ M = 1) :=26  FRC.FieldsML.roots_inclusion M hM2728/-- 27:C1 — the Wilson weight (`FieldsML.wilson_weight_nonneg`). -/29theorem wilson_weight_nonneg (ζ : ℂ) (h : ‖ζ‖ = 1) : 0 ≤ 1 - ζ.re ∧ (1 - ζ.re = 0 ↔ ζ = 1) :=30  FRC.FieldsML.wilson_weight_nonneg ζ h3132/-- 27:C1, 27:C7, 27:X7 — the `2T` area law (`FieldsML.area_law_positive`). -/33theorem area_law_positive (x : ℝ) (hx : 1 < x) :34    0 < (x ^ 4 + 4 * x ^ 3 - 4 * x - 1) / (x ^ 4 + 8 * x ^ 3 + 6 * x ^ 2 + 8 * x + 1) ∧35    (x ^ 4 + 4 * x ^ 3 - 4 * x - 1) / (x ^ 4 + 8 * x ^ 3 + 6 * x ^ 2 + 8 * x + 1) < 1 :=36  FRC.FieldsML.area_law_positive x hx3738/-- 27:C6 — the Fermi constant (`FieldsML.fermi_constant`). -/39theorem fermi_constant (g v G MW2 : ℝ) (hg : g ≠ 0) (hv : v ≠ 0) (hM : MW2 = g ^ 2 * v ^ 2 / 4)40    (hG : G / √2 = g ^ 2 / (8 * MW2)) : G = 1 / (√2 * v ^ 2) :=41  FRC.FieldsML.fermi_constant g v G MW2 hg hv hM hG4243/-- 27:P3 [chart] — the one-loop running's near-miss and meeting scale (`FieldsML.running_near_miss`). -/44theorem running_near_miss (ainv s2 as b1 b2 b3 MZ : ℝ) (h1 : ainv = 127.951) (h2 : s2 = 0.23121)45    (h3 : as = 0.1179) (hb1 : b1 = 41 / 10) (hb2 : b2 = -19 / 6) (hb3 : b3 = -7) (hZ : MZ = 91.1876) :46    |1 / as - b3 * ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2)) - (s2 * ainv - b2 * ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2)))| / (s2 * ainv - b2 * ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2))) < 1 / 5 ∧47    (10 : ℝ) ^ 12 < MZ * Real.exp (2 * Real.pi * ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2))) ∧48    MZ * Real.exp (2 * Real.pi * ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2))) < (10 : ℝ) ^ 14 :=49  FRC.FieldsML.running_near_miss ainv s2 as b1 b2 b3 MZ h1 h2 h3 hb1 hb2 hb3 hZ5051/-- 27:P4 [chart] — the proton lifetime at the substrate and the GUT scales (`FieldsML.proton_lifetime`). -/52theorem proton_lifetime (mp a hbar yr : ℚ) (hm : mp = 0.938) (ha : a = 1 / 40) (hh : hbar = 6.582e-25)53    (hy : yr = 3.156e7) :54    (10 : ℚ) ^ 45 ≤ (1.22e19 : ℚ) ^ 4 / (a ^ 2 * mp ^ 5) * hbar / yr ∧55    (10 : ℚ) ^ 34 < (1e16 : ℚ) ^ 4 / (a ^ 2 * mp ^ 5) * hbar / yr ∧56    ∀ M M' : ℚ, 0 < M → 0 < M' →57      (M' ^ 4 / (a ^ 2 * mp ^ 5) * hbar / yr) / (M ^ 4 / (a ^ 2 * mp ^ 5) * hbar / yr) = (M' / M) ^ 4 :=58  FRC.FieldsML.proton_lifetime mp a hbar yr hm ha hh hy5960/-- 27:P5 [chart] — the seesaw band and `m_b/m_τ` (`FieldsML.seesaw_band`). -/61theorem seesaw_band (v mb mt : ℚ) (hv : v = 174) (hb : mb = 4.18) (ht : mt = 1.777) :62    (0.01 : ℚ) < (0.3 : ℚ) ^ 2 * v ^ 2 / 1e14 * 1e9 ∧ (0.3 : ℚ) ^ 2 * v ^ 2 / 1e14 * 1e9 < 0.1 ∧63    (0.01 : ℚ) < (1 : ℚ) ^ 2 * v ^ 2 / 1e15 * 1e9 ∧ (1 : ℚ) ^ 2 * v ^ 2 / 1e15 * 1e9 < 0.1 ∧64    (2 : ℚ) < mb / mt ∧ mb / mt < 3 :=65  FRC.FieldsML.seesaw_band v mb mt hv hb ht6667-- Ledger predicates of 27-fields (generated by make_predicates.py from docs/27-fields/27-fields-ledger.json; edit the ledger, not this section)68/-- 27:C1 (p27013) — The finite gauge correspondence, its exact clauses: the abelian inclusion $\Z/M\hookrightarrow\U(1)$ as the $M$-th roots of unity, the positive cyclotomic action (the Wilson weight $1-\Re\zeta\ge0$), and the exact $q{=}3$ embedding $\SU(2,\F_3)\cong2T$ with the Wilson trace a class function (Theorems~\ref{thm:corrU1},~\ref{thm:corrpos},~\ref{thm:corr2T}); the resolvable-window reconstruction is C12 and the cross-scale running $\Omega$-hard (Z1). -/69theorem p27013 : (∀ (M : ℕ), M ≠ (0 : ℕ) → IsPrimitiveRoot (Complex.exp ((2 : ℂ) * ↑Real.pi * Complex.I / ↑M)) M ∧ (∀ (j k : ℕ), Complex.exp ((2 : ℂ) * ↑Real.pi * Complex.I / ↑M) ^ (j + k) = Complex.exp ((2 : ℂ) * ↑Real.pi * Complex.I / ↑M) ^ j * Complex.exp ((2 : ℂ) * ↑Real.pi * Complex.I / ↑M) ^ k) ∧ (∀ (j k : ℕ), j < M → k < M → Complex.exp ((2 : ℂ) * ↑Real.pi * Complex.I / ↑M) ^ j = Complex.exp ((2 : ℂ) * ↑Real.pi * Complex.I / ↑M) ^ k → j = k) ∧ ∀ (k : ℕ), (Complex.exp ((2 : ℂ) * ↑Real.pi * Complex.I / ↑M) ^ k) ^ M = (1 : ℂ)) ∧ ∀ (ζ : ℂ), ‖ζ‖ = (1 : ℝ) → (0 : ℝ) ≤ (1 : ℝ) - ζ.re ∧ ((1 : ℝ) - ζ.re = (0 : ℝ) ↔ ζ = (1 : ℂ)) :=70  @FRC.LedgerML.p2701371/-- 27:C6 (p27018) — The Weinberg trace formula $\sin^2\sW=\Tr(T_3^2)/\Tr(Q^2)=3/8$ for a complete generation, the unification-point value, and the four-fermion amplitude with $G_F=1/(\sqrt2\,v^2)$; the imported template (A4) evaluated on the realisations B3, B5. -/72theorem p27018 : ∀ (g v G MW2 : ℝ), g ≠ (0 : ℝ) → v ≠ (0 : ℝ) → MW2 = g ^ (2 : ℕ) * v ^ (2 : ℕ) / (4 : ℝ) → G / √(2 : ℝ) = g ^ (2 : ℕ) / ((8 : ℝ) * MW2) → G = (1 : ℝ) / (√(2 : ℝ) * v ^ (2 : ℕ)) :=73  @FRC.LedgerML.p2701874/-- 27:C7 (p27019) — The strong sector: the colour $\SU(3,\Omega)$ frame forced as the minimal triality-carrying rank, the exact $\Z_3$ centre, the gluon connection, and the confinement area law $\sigma>0$ from positivity, with the string tension $\sigma(\beta)=-\ln c_1(\beta)$ computed in finite units (closed form on $2T$; $c_1^{\SU(3)}=\tfrac\beta{18}+\tfrac{\beta^2}{216}+\cdots$). -/75theorem p27019 : ∀ (x : ℝ), (1 : ℝ) < x → (0 : ℝ) < (x ^ (4 : ℕ) + (4 : ℝ) * x ^ (3 : ℕ) - (4 : ℝ) * x - (1 : ℝ)) / (x ^ (4 : ℕ) + (8 : ℝ) * x ^ (3 : ℕ) + (6 : ℝ) * x ^ (2 : ℕ) + (8 : ℝ) * x + (1 : ℝ)) ∧ (x ^ (4 : ℕ) + (4 : ℝ) * x ^ (3 : ℕ) - (4 : ℝ) * x - (1 : ℝ)) / (x ^ (4 : ℕ) + (8 : ℝ) * x ^ (3 : ℕ) + (6 : ℝ) * x ^ (2 : ℕ) + (8 : ℝ) * x + (1 : ℝ)) < (1 : ℝ) :=76  @FRC.LedgerML.p2701977/-- 27:X7 (p27030) — \textbf{The colour sector} is fixed: three colours is the minimal triality-carrying frame, confinement is the compact-group area law from positivity, and asymptotic freedom is the gluon self-coupling, not $N_c=3$ supplemented by an assumed confining phase. -/78theorem p27030 : ∀ (x : ℝ), (1 : ℝ) < x → (0 : ℝ) < (x ^ (4 : ℕ) + (4 : ℝ) * x ^ (3 : ℕ) - (4 : ℝ) * x - (1 : ℝ)) / (x ^ (4 : ℕ) + (8 : ℝ) * x ^ (3 : ℕ) + (6 : ℝ) * x ^ (2 : ℕ) + (8 : ℝ) * x + (1 : ℝ)) ∧ (x ^ (4 : ℕ) + (4 : ℝ) * x ^ (3 : ℕ) - (4 : ℝ) * x - (1 : ℝ)) / (x ^ (4 : ℕ) + (8 : ℝ) * x ^ (3 : ℕ) + (6 : ℝ) * x ^ (2 : ℕ) + (8 : ℝ) * x + (1 : ℝ)) < (1 : ℝ) :=79  @FRC.LedgerML.p2703080/-- 27:P3 (p27037) — \textbf{No TeV supersymmetry} \emph{[forced]}. The Standard-Model content alone runs the measured couplings to a meeting of the first two near $10^{13}\,$GeV, where the Weinberg angle is $3/8$ by the normalisation. The strong coupling misses by $13\%$. The content has no superpartner. Where the completion closes the miss is the $\Omega$-hard running (Z1). \emph{Falsifier:} superpartners. -/81theorem p27037 : ∀ (ainv s2 as b1 b2 b3 MZ : ℝ), ainv = 127.951 → s2 = 0.23121 → as = 0.1179 → b1 = (41 / 10 : ℝ) → b2 = (-19 / 6 : ℝ) → b3 = (-7 : ℝ) → MZ = 91.1876 → |(1 : ℝ) / as - b3 * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2)) - (s2 * ainv - b2 * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2)))| / (s2 * ainv - b2 * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2))) < (1 / 5 : ℝ) ∧ (10 : ℝ) ^ (12 : ℕ) < MZ * Real.exp ((2 : ℝ) * Real.pi * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2))) ∧ MZ * Real.exp ((2 : ℝ) * Real.pi * (((3 / 5 : ℝ) * ((1 : ℝ) - s2) * ainv - s2 * ainv) / (b1 - b2))) < (10 : ℝ) ^ (14 : ℕ) :=82  @FRC.LedgerML.p2703783/-- 27:P4 (p27038) — \textbf{The proton is effectively stable} \emph{[forced]}. The $X,Y$ leptoquarks are the twelve colour--isospin off-block generators. With their mass at the substrate scale (the $\Omega$-hard scale of Z1) the lifetime exceeds $10^{45}$ years, orders beyond the reach of Hyper-Kamiokande. At $10^{16}\,$GeV it already exceeds the Super-Kamiokande bound. \emph{Falsifier:} an observed proton decay near $10^{34}$--$10^{35}$ years. -/84theorem p27038 : ∀ (mp a hbar yr : ℚ), mp = 0.938 → a = (1 / 40 : ℚ) → hbar = 6582e-28 → yr = 3156e4 → (10 : ℚ) ^ (45 : ℕ) ≤ 122e17 ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr ∧ (10 : ℚ) ^ (34 : ℕ) < 1e16 ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr ∧ ∀ (M M' : ℚ), (0 : ℚ) < M → (0 : ℚ) < M' → M' ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr / (M ^ (4 : ℕ) / (a ^ (2 : ℕ) * mp ^ (5 : ℕ)) * hbar / yr) = (M' / M) ^ (4 : ℕ) :=85  @FRC.LedgerML.p2703886/-- 27:P5 (p27039) — \textbf{Majorana neutrinos, heavy singlets, no light sterile neutrino} \emph{[sector]}. Exactly one of the sixteen states is a full singlet, the right-handed neutrino. It admits a Majorana mass at the unification scale (A4), and the seesaw then places the light masses in the observed band for singlet masses of $10^{14}$--$10^{15}\,$GeV. \emph{Falsifier:} a confirmed eV-scale sterile neutrino, or Dirac neutrinos. -/87theorem p27039 : ∀ (v mb mt : ℚ), v = (174 : ℚ) → mb = 4.18 → mt = 1.777 → 1e-2 < 0.3 ^ (2 : ℕ) * v ^ (2 : ℕ) / 1e14 * 1e9 ∧ 0.3 ^ (2 : ℕ) * v ^ (2 : ℕ) / 1e14 * 1e9 < 0.1 ∧ 1e-2 < (1 : ℚ) ^ (2 : ℕ) * v ^ (2 : ℕ) / 1e15 * 1e9 ∧ (1 : ℚ) ^ (2 : ℕ) * v ^ (2 : ℕ) / 1e15 * 1e9 < 0.1 ∧ (2 : ℚ) < mb / mt ∧ mb / mt < (3 : ℚ) :=88  @FRC.LedgerML.p2703989-- end ledger predicates9091end FRC.Fields92