import Mathlib /-! Generated by `lean/make_web.py` from `FrcLedger/Pnp.lean` with `FrcLedger/Theme/Horizon`, `FrcLedger/Theme/Chart`, `FrcLedger/Theme/Gravity`, `FrcLedger/Theme/Quantum`, `FrcLedger/Theme/Strong`, `FrcLedger/Theme/Fields`, `FrcLedger/Keys/Chart` inlined — one self-contained file for the Lean web editor. Edit the modules, not this file. -/ /-! inlined: FrcLedger/Theme/Horizon.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Horizon — the horizon theme on Mathlib: the shell arithmetic of 20-rh (ledger migration, task LM36) The exact arithmetic of the shell theorem and its neighbours, proved for every shell: an arbitrary finite field `F` with `4κ + 1` elements and a primitive root `g`, or `ZMod p` where the prime is needed, and over any integral domain for the Ramanujan sum. The zero-slot and slot complementarity (20:B4, B5); the Ramanujan sum `c_p(n) = −1` off the origin (20:B7); the constants of the Subject register (20:B10); the quadratic extension `F(η)`, `η² = ν` a nonsquare, as Mathlib's `QuadraticAlgebra F ν 0`: the phase circle of order `p + 1`, Frobenius as conjugation and as inversion on the circle, the quarter-turn off the circle (20:B6); the critical line `Tr z = 1 ⟺ Re z = 2⁻¹` with `p` points and energy `¼ − νb²` (20:B8); the Klein four-group of Frobenius and the half-turn with its fixed loci (20:B9); the scale-shift on the power characters and its trace (20:E1, E12 (iii)), the power characters never orthonormal (20:E13); frame coincidence below the horizon (20:B2) and the laboratory pair `(13, 233)` (20:B1). The theorems moved here from 20-rh's `FrcLedger/Rh.lean` (7 October 2026), under the same names in the namespace `FRC.HorizonML`; that module keeps the old names as aliases. The complex characters of the cycle and the von Mangoldt weight use the reals and live in the chart theme (`Theme/Chart.lean`). Classical (tier 2) on Mathlib's hierarchy, with no reals: the exact Mathlib theme of gate G09. -/ namespace FRC.HorizonML open Finset /-! ## The shell: the zero-slot, slot complementarity and the Ramanujan sum (rows B4, B5, B7) -/ section shell variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] /-- 20:B4 — zero-slot, every shell: `Σ_{x ∈ F^×} x^k = 0` on every nonterminal exponent `1 ≤ k ≤ p − 2`, and `= −1` on the full cycle `k = p − 1`. -/ theorem zero_slot : (∀ k, 1 ≤ k → k ≤ Fintype.card F - 2 → ∑ x : Fˣ, ((x : F) ^ k) = 0) ∧ ∑ x : Fˣ, ((x : F) ^ (Fintype.card F - 1)) = -1 := by refine ⟨fun k hk1 hk2 => ?_, ?_⟩ · rw [FiniteField.sum_pow_units, ite_eq_right] intro hdvd have := Nat.le_of_dvd (by omega) hdvd omega · rw [FiniteField.sum_pow_units, ite_eq_left dvd_rfl] omit [DecidableEq F] in /-- 20:B5 — slot complementarity, every shell: `Φ(k) = −g^k` is injective on the nontrivial spectral slots `1 ≤ k ≤ p − 2` and maps them onto the nonterminal additive slots `F^× ∖ {−1}`. -/ theorem slot_complementarity (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) : Set.InjOn (fun k : ℕ => -(g ^ k)) (Set.Icc 1 (Fintype.card F - 2)) ∧ (fun k : ℕ => -(g ^ k)) '' Set.Icc 1 (Fintype.card F - 2) = {y : F | y ≠ 0 ∧ y ≠ -1} := by have h1 : 1 < Fintype.card F := Fintype.one_lt_card have : NeZero (Fintype.card F - 1) := ⟨by omega⟩ have hg0 : g ≠ 0 := by rintro rfl have := hg.pow_eq_one rw [zero_pow (by omega)] at this exact zero_ne_one this refine ⟨fun a ha b hb hab => ?_, ?_⟩ · simp only [Set.mem_Icc] at ha hb exact hg.pow_inj (by omega) (by omega) (neg_injective hab) · ext y simp only [Set.mem_image, Set.mem_Icc, Set.mem_ofPred_eq] constructor · rintro ⟨k, ⟨hk1, hk2⟩, rfl⟩ refine ⟨neg_ne_zero.2 (pow_ne_zero _ hg0), fun h => ?_⟩ have := neg_injective h exact hg.pow_ne_one_of_pos_of_lt (by omega) (by omega) this · rintro ⟨hy0, hy1⟩ have hpow : (-y) ^ (Fintype.card F - 1) = 1 := FiniteField.pow_card_sub_one_eq_one (-y) (neg_ne_zero.2 hy0) obtain ⟨i, hi, hiy⟩ := hg.eq_pow_of_pow_eq_one hpow have hi0 : i ≠ 0 := by rintro rfl rw [pow_zero] at hiy exact hy1 (by rw [← neg_neg y, ← hiy]) exact ⟨i, ⟨by omega, by omega⟩, by rw [hiy, neg_neg]⟩ end shell section ramanujan variable {R : Type*} [CommRing R] [IsDomain R] /-- 20:B7 — the flat ground state, in any integral domain with a primitive `p`-th root of unity `ω` (the cyclotomic ledger, `𝔽_q` with `q ≡ 1 (mod p)`, or `ℂ`): the full-modulus Ramanujan sum `c_p(n) = Σ_{a=1}^{p−1} ω^{an}` equals `−1` for every `n ≢ 0 (mod p)`, and `p − 1` at the origin; the mode at the spectral origin carries no prime information. -/ theorem ramanujan_sum {p : ℕ} (hp : 0 < p) {ω : R} (hω : IsPrimitiveRoot ω p) (n : ℕ) : (¬ p ∣ n → ∑ a ∈ Ico 1 p, ω ^ (a * n) = -1) ∧ (p ∣ n → ∑ a ∈ Ico 1 p, ω ^ (a * n) = ((p - 1 : ℕ) : R)) := by have hsplit : ∑ a ∈ range p, ω ^ (a * n) = 1 + ∑ a ∈ Ico 1 p, ω ^ (a * n) := by obtain ⟨m, rfl⟩ : ∃ m, p = m + 1 := ⟨p - 1, by omega⟩ rw [sum_range_succ', sum_Ico_eq_sum_range, Nat.add_sub_cancel, zero_mul, pow_zero, add_comm] congr 1 refine sum_congr rfl fun a _ => ?_ rw [add_comm 1 a] constructor · intro hn have hx1 : ω ^ n ≠ 1 := fun h => hn ((hω.pow_eq_one_iff_dvd n).1 h) have hxp : (ω ^ n) ^ p = 1 := by rw [← pow_mul, mul_comm, pow_mul, hω.pow_eq_one, one_pow] have hsum : ∑ a ∈ range p, ω ^ (a * n) = 0 := by have h := geom_sum_mul (ω ^ n) p rw [hxp, sub_self] at h have h' : ∑ a ∈ range p, ω ^ (a * n) = ∑ a ∈ range p, (ω ^ n) ^ a := sum_congr rfl fun a _ => by rw [← pow_mul, mul_comm] rw [h'] exact (mul_eq_zero.1 h).resolve_right (sub_ne_zero.2 hx1) rw [hsum] at hsplit exact (neg_eq_of_add_eq_zero_right hsplit.symm).symm · intro hn have hone : ∀ a, ω ^ (a * n) = 1 := fun a => by obtain ⟨c, rfl⟩ := hn rw [← mul_assoc, mul_comm a, mul_assoc, pow_mul, hω.pow_eq_one, one_pow] simp only [hone, sum_const, Nat.card_Ico, nsmul_eq_mul, mul_one] end ramanujan /-! ## The Subject register on the shell (rows B10, B8's arithmetic) -/ section constants variable {F : Type*} [Field F] [Fintype F] /-- `2 ≠ 0` on a shell of `4κ + 1` elements. -/ lemma two_ne_zero_of_card (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) : (2 : F) ≠ 0 := by intro h2 have hc : ((4 * κ + 1 : ℕ) : F) = 0 := by rw [← hκ]; exact FiniteField.cast_card_eq_zero F have : ((4 * κ + 1 : ℕ) : F) = 2 * (2 * κ) + 1 := by push_cast; ring rw [this, h2, zero_mul, zero_add] at hc exact one_ne_zero hc /-- 20:B8, 20:B10 — the half-turn arithmetic on every shell of `4κ + 1` elements: `2π ≡ −1` with `π = 2κ`, and `2⁻¹ = 2κ + 1 = −π`. -/ theorem half_turn (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) : (2 : F) * ((2 * κ : ℕ) : F) = -1 ∧ (2 : F) * ((2 * κ + 1 : ℕ) : F) = 1 ∧ ((2 * κ + 1 : ℕ) : F) = -((2 * κ : ℕ) : F) ∧ (2 : F)⁻¹ = ((2 * κ + 1 : ℕ) : F) := by have hc : ((4 * κ + 1 : ℕ) : F) = 0 := by rw [← hκ]; exact FiniteField.cast_card_eq_zero F have h2 : (2 : F) ≠ 0 := two_ne_zero_of_card κ hκ have e1 : (2 : F) * ((2 * κ : ℕ) : F) = -1 := by have : ((4 * κ + 1 : ℕ) : F) = 2 * ((2 * κ : ℕ) : F) + 1 := by push_cast; ring rw [this] at hc exact eq_neg_of_add_eq_zero_left hc have e2 : (2 : F) * ((2 * κ + 1 : ℕ) : F) = 1 := by push_cast at e1 ⊢ linear_combination e1 refine ⟨e1, e2, ?_, ?_⟩ · push_cast at e1 e2 ⊢ have : (2 : F) * (2 * (κ : F) + 1 + 2 * (κ : F)) = 0 := by linear_combination e2 + e1 have := (mul_eq_zero.1 this).resolve_left h2 exact eq_neg_of_add_eq_zero_left this · exact (eq_inv_of_mul_eq_one_right e2).symm /-- The half-period `g^{2κ} = −1` for a primitive root of a shell with `4κ + 1` elements. -/ lemma half_period (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) : g ^ (2 * κ) = -1 := by have hκ' : Fintype.card F - 1 = 4 * κ := by omega have hκpos : κ ≠ 0 := by intro h; subst h; have := Fintype.one_lt_card (α := F); omega have h2 : IsPrimitiveRoot (g ^ (2 * κ)) 2 := by rw [hκ'] at hg exact hg.pow (by omega) (show 4 * κ = 2 * κ * 2 by ring) exact h2.eq_neg_one_of_two_right /-- 20:B10 — the Subject constants on every shell: `π = 2κ` with `2π = −1`; the quarter-turn `i = g^{−κ}` (read as `g^{3κ}`, since `g^{4κ} = 1`) equals `−g^κ` and squares to `−1`; `g^π = −1`; and the Euler identity `e^{iπ} = (g^m)^{m·π} = −1` for every odd `m` — the convention "`e = g^m` on the odd representative `m` of `i`" fixes the parity of the exponent, and the identity uses nothing else about `m`. -/ theorem subject_constants (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) : (2 : F) * ((2 * κ : ℕ) : F) = -1 ∧ g ^ (3 * κ) = -(g ^ κ) ∧ (g ^ (3 * κ)) ^ 2 = -1 ∧ g ^ (2 * κ) = -1 ∧ ∀ m : ℕ, m % 2 = 1 → (g ^ m) ^ (m * (2 * κ)) = -1 := by have hhp := half_period κ hκ g hg have hi : g ^ (3 * κ) = -(g ^ κ) := by rw [show 3 * κ = κ + 2 * κ by ring, pow_add, hhp, mul_neg, mul_one] refine ⟨(half_turn κ hκ).1, hi, ?_, hhp, fun m hm => ?_⟩ · rw [hi, neg_sq, ← pow_mul, show κ * 2 = 2 * κ by ring, hhp] · rw [← pow_mul, show m * (m * (2 * κ)) = 2 * κ * (m * m) by ring, pow_mul, hhp] have hodd : Odd (m * m) := by have := Nat.odd_iff.2 hm exact this.mul this exact hodd.neg_one_pow /-- 20:B10 [value] — on `𝔽₁₃(τ; 0, 1, 2)`: `κ = 3`, `π = 6`, `2π = −1`, `i = 2^{−3} = 2^9 = 5`, `i² = −1`, `e = 2^5 = 6` on the odd representative `5`, `2^π = −1`, `e^{iπ} = 6^{30} = −1`. -/ theorem constants13 : (2 : ZMod 13) * 6 = -1 ∧ (2 : ZMod 13) ^ 9 = 5 ∧ (5 : ZMod 13) ^ 2 = -1 ∧ (2 : ZMod 13) ^ 5 = 6 ∧ (2 : ZMod 13) ^ 6 = -1 ∧ (6 : ZMod 13) ^ (5 * 6) = -1 := by decide end constants /-! ## The quadratic extension: the phase circle, the critical line, the two loci of agreement (rows B6, B8, B9) -/ section extension variable {F : Type*} [Field F] (ν : F) local notation "K" => QuadraticAlgebra F ν 0 /-- The trace of `a + bη` is `2a`. -/ lemma trace_eq (z : K) : QuadraticAlgebra.trace z = 2 * z.re := by rw [QuadraticAlgebra.trace_def, zero_mul, add_zero] /-- The norm of `a + bη` is `a² − νb²`. -/ lemma norm_eq (z : K) : QuadraticAlgebra.norm z = z.re * z.re - ν * z.im * z.im := by rw [QuadraticAlgebra.norm_def, zero_mul, zero_mul, add_zero] /-- The conjugate of `a + bη` is `a − bη`. -/ lemma star_eq (z : K) : star z = ⟨z.re, -z.im⟩ := by ext <;> simp [QuadraticAlgebra.re_star, QuadraticAlgebra.im_star] /-- 20:B9 — Frobenius `φ = star` and the functional-equation half-turn `ρ : z ↦ 1 − z` generate a Klein four-group: both are involutions and they commute. -/ theorem klein_four (z : K) : star (star z) = z ∧ (1 - (1 - z)) = z ∧ star (1 - z) = 1 - star z := by refine ⟨star_star z, sub_sub_cancel 1 z, ?_⟩ rw [star_sub, star_one] /-- 20:B9 — the fixed locus of Frobenius is the prime meridian `F` (the elements with `b = 0`). -/ theorem fixed_frobenius (h2 : (2 : F) ≠ 0) (z : K) : star z = z ↔ z.im = 0 := by rw [star_eq] constructor · intro h have := congrArg QuadraticAlgebra.im h simp only at this have h' : (2 : F) * z.im = 0 := by linear_combination -this exact (mul_eq_zero.1 h').resolve_left h2 · intro h ext <;> simp [h] /-- 20:B8, 20:B9 — the finite critical line: `Tr z = 1` exactly when `Re z = 2⁻¹`; this locus is the fixed locus of `σ = ρ ∘ φ : z ↦ 1 − z̄`. -/ theorem trace_eq_one_iff (h2 : (2 : F) ≠ 0) (z : K) : (QuadraticAlgebra.trace z = 1 ↔ z.re = 2⁻¹) ∧ (1 - star z = z ↔ z.re = 2⁻¹) := by have key : (2 : F) * z.re = 1 ↔ z.re = 2⁻¹ := by constructor · intro h; exact eq_inv_of_mul_eq_one_right h · intro h; rw [h, mul_inv_cancel₀ h2] refine ⟨by rw [trace_eq]; exact key, ?_⟩ rw [star_eq] constructor · intro h have := congrArg QuadraticAlgebra.re h simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one] at this exact key.1 (by linear_combination -this) · intro h ext · simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one] have := key.2 h linear_combination -this · simp only [QuadraticAlgebra.im_sub, QuadraticAlgebra.im_one, zero_sub, neg_neg] /-- 20:B9 — the fixed locus of the half-turn `ρ` is the single point `2⁻¹`, the meeting of the prime meridian and the critical line. -/ theorem fixed_half_turn (h2 : (2 : F) ≠ 0) (z : K) : (1 - z = z ↔ z = ⟨2⁻¹, 0⟩) ∧ (z.im = 0 ∧ z.re = 2⁻¹ ↔ z = ⟨2⁻¹, 0⟩) := by have hinv : (2 : F) * 2⁻¹ = 1 := mul_inv_cancel₀ h2 constructor · constructor · intro h have hre := congrArg QuadraticAlgebra.re h have him := congrArg QuadraticAlgebra.im h simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one, QuadraticAlgebra.im_sub, QuadraticAlgebra.im_one, zero_sub] at hre him have h2re : (2 : F) * z.re = 1 := by linear_combination -hre have h2im : (2 : F) * z.im = 0 := by linear_combination -him ext · exact eq_inv_of_mul_eq_one_right h2re · exact (mul_eq_zero.1 h2im).resolve_left h2 · rintro rfl ext · simp only [QuadraticAlgebra.re_sub, QuadraticAlgebra.re_one] linear_combination -hinv · simp only [QuadraticAlgebra.im_sub, QuadraticAlgebra.im_one, sub_zero] · constructor · rintro ⟨him, hre⟩; ext · exact hre · exact him · rintro rfl; exact ⟨rfl, rfl⟩ /-- 20:B8 — on the critical line the energy is `N(z) = ¼ − νb²`. -/ theorem norm_on_line (z : K) (hz : z.re = 2⁻¹) : QuadraticAlgebra.norm z = (4 : F)⁻¹ - ν * z.im ^ 2 := by rw [norm_eq, hz, sq, mul_assoc] congr 1 rw [show (4 : F) = 2 * 2 by norm_num, mul_inv] /-- 20:E12, 20:B8 — the spectral readout: the mode index `θ ∈ F` is read at the point `z(θ) = 2⁻¹ + θη` of the quadratic extension. -/ def readout (θ : F) : K := ⟨2⁻¹, θ⟩ /-- 20:E12, 20:B8 — clause (ii) of the shell theorem: every readout `z(θ) = 2⁻¹ + θη` lies on the trace-one line, its real part is the half-turn `2⁻¹`, and `θ ↦ z(θ)` is injective (with `card_critical_line`, a bijection of `F` onto the line). -/ theorem readout_on_line (h2 : (2 : F) ≠ 0) (θ : F) : QuadraticAlgebra.trace (readout ν θ) = 1 ∧ (readout ν θ).re = 2⁻¹ ∧ Function.Injective (readout ν) := by refine ⟨?_, rfl, fun a b h => by simpa [readout] using congrArg QuadraticAlgebra.im h⟩ rw [trace_eq] exact mul_inv_cancel₀ h2 variable [Fintype F] [DecidableEq F] /-- The extension as a finite type, through its coordinates. -/ noncomputable instance instFintypeK : Fintype K := Fintype.ofEquiv (F × F) (QuadraticAlgebra.equivProd ν 0).symm /-- 20:B8 — the critical line carries exactly `p` points: `z = 2⁻¹ + bη`, one for each `b ∈ F`. -/ theorem card_critical_line (h2 : (2 : F) ≠ 0) : (univ.filter (fun z : K => QuadraticAlgebra.trace z = 1)).card = Fintype.card F := by have hline : univ.filter (fun z : K => QuadraticAlgebra.trace z = 1) = univ.image (fun b : F => (⟨2⁻¹, b⟩ : K)) := by ext z simp only [mem_filter, mem_univ, true_and, mem_image] rw [(trace_eq_one_iff ν h2 z).1] constructor · intro h; exact ⟨z.im, by ext <;> simp [h]⟩ · rintro ⟨b, rfl⟩; rfl rw [hline, card_image_of_injective _ (fun a b h => by simpa using congrArg QuadraticAlgebra.im h), card_univ] omit [DecidableEq F] in /-- 20:E12 — the slot index of a nontrivial slot: for `1 ≤ k ≤ p − 2` the index `θ = Φ(k) = −g^k` at which slot `k` is read is neither `0` (the centre `2⁻¹`) nor `−1` (the full-cycle exponent). -/ theorem readout_slot_index (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (k : ℕ) (hk1 : 1 ≤ k) (hk2 : k ≤ Fintype.card F - 2) : -(g ^ k) ≠ 0 ∧ -(g ^ k) ≠ -1 := by have hcard : 1 < Fintype.card F := Fintype.one_lt_card have hg0 : g ≠ 0 := hg.ne_zero (by omega) refine ⟨fun h => pow_ne_zero k hg0 (neg_eq_zero.1 h), fun h => ?_⟩ have h1 : g ^ k = 1 := neg_inj.1 h have hdvd := (hg.pow_eq_one_iff_dvd k).1 h1 have := Nat.le_of_dvd (by omega) hdvd omega end extension section frobenius variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] {p : ℕ} [hp : Fact p.Prime] [CharP F p] (hcard : Fintype.card F = p) (ν : F) [hν : Fact (¬ IsSquare ν)] local notation "K" => QuadraticAlgebra F ν 0 omit [DecidableEq F] in include hcard hν in /-- On a shell carrying a nonsquare, `2 ≠ 0` (every element of `𝔽₂` is a square). -/ lemma two_ne_zero_of_nonsquare : (2 : F) ≠ 0 := by intro h2 have hp2 : p = 2 := (Nat.prime_dvd_prime_iff_eq hp.out Nat.prime_two).1 ((CharP.cast_eq_zero_iff F p 2).1 (by exact_mod_cast h2)) -- every element of a two-element field is a square: `x^2 = x` apply hν.out refine ⟨ν, ?_⟩ have := FiniteField.pow_card ν rw [hcard, hp2, sq] at this exact this.symm omit [DecidableEq F] in include hcard hν in /-- Euler's criterion for the nonsquare `ν`: `ν^{(p−1)/2} = −1`. -/ lemma nonsquare_pow : ν ^ (p / 2) = -1 := by have h2 : (2 : F) ≠ 0 := two_ne_zero_of_nonsquare hcard ν have hp2 : p ≠ 2 := by intro h; apply h2 have := (CharP.cast_eq_zero_iff F p p).2 dvd_rfl rw [h] at this; exact_mod_cast this have hchar : ringChar F ≠ 2 := by rw [ringChar.eq F p]; exact hp2 have hν0 : ν ≠ 0 := by rintro rfl; exact hν.out ⟨0, by simp⟩ rcases FiniteField.pow_dichotomy hchar hν0 with h | h · exact absurd ((FiniteField.isSquare_iff hchar hν0).2 h) hν.out · rwa [hcard] at h omit [DecidableEq F] in include hcard in /-- 20:B6 — Frobenius on the extension is conjugation: `z^p = z̄` for every `z ∈ F(η)`. -/ theorem frobenius_eq_star (z : K) : z ^ p = star z := by have : CharP K p := charP_of_injective_algebraMap (algebraMap F K).injective p have hodd : p = 2 * (p / 2) + 1 := by have := hp.out.eq_two_or_odd' rcases this with h | h · exfalso have h2 : (2 : F) ≠ 0 := two_ne_zero_of_nonsquare hcard ν apply h2 have := (CharP.cast_eq_zero_iff F p p).2 dvd_rfl rw [h] at this; exact_mod_cast this · exact (Nat.two_mul_div_two_add_one_of_odd h).symm have hω : (QuadraticAlgebra.omega : K) ^ p = -QuadraticAlgebra.omega := by rw [hodd, pow_succ, pow_mul, QuadraticAlgebra.omega_pow_two_eq_add] simp only [zero_smul, add_zero] rw [← Algebra.algebraMap_eq_smul_one, ← map_pow, nonsquare_pow hcard ν, map_neg, map_one, neg_one_mul] have hz : z = algebraMap F K z.re + z.im • QuadraticAlgebra.omega := by rw [Algebra.algebraMap_eq_smul_one]; exact (QuadraticAlgebra.re_smul_add_im_smul z).symm have hre : z.re ^ p = z.re := by rw [← hcard]; exact FiniteField.pow_card z.re have him : z.im ^ p = z.im := by rw [← hcard]; exact FiniteField.pow_card z.im conv_lhs => rw [hz] rw [add_pow_char, ← map_pow, hre, smul_pow, him, hω, star_eq] ext · simp [QuadraticAlgebra.algebraMap_eq, QuadraticAlgebra.re_omega] · simp [QuadraticAlgebra.algebraMap_eq, QuadraticAlgebra.im_omega] omit [DecidableEq F] in include hcard in /-- 20:B6 — the norm is the `(p+1)`-st power: `z^{p+1} = z z̄ = N(z)` in the extension. -/ theorem norm_eq_pow (z : K) : algebraMap F K (QuadraticAlgebra.norm z) = z ^ (p + 1) := by rw [pow_succ, frobenius_eq_star hcard ν z, QuadraticAlgebra.algebraMap_norm_eq_mul_star, mul_comm] include hcard in /-- 20:B6 — the phase circle `U_{p+1} = {z : N(z) = 1}` has exactly `p + 1` elements, and Frobenius is inversion on it: `z̄ = z⁻¹` for `N(z) = 1`. -/ theorem phase_circle : (univ.filter (fun z : K => QuadraticAlgebra.norm z = 1)).card = p + 1 ∧ ∀ z : K, QuadraticAlgebra.norm z = 1 → star z = z⁻¹ := by constructor · -- the circle is the set of `(p+1)`-st roots of unity, counted by a primitive root have hcardK : Fintype.card K = p ^ 2 := by rw [Fintype.card_congr (QuadraticAlgebra.equivProd ν 0), Fintype.card_prod, hcard, sq] have hset : univ.filter (fun z : K => QuadraticAlgebra.norm z = 1) = Polynomial.nthRootsFinset (p + 1) (1 : K) := by ext z rw [mem_filter, Polynomial.mem_nthRootsFinset (by omega), ← norm_eq_pow hcard ν] constructor · rintro ⟨-, h⟩; rw [h, map_one] · intro h; exact ⟨mem_univ _, QuadraticAlgebra.algebraMap_injective (by rw [h, map_one])⟩ rw [hset] -- a primitive `(p+1)`-st root of unity in `K` obtain ⟨ζ, hζ⟩ := IsCyclic.exists_generator (α := Kˣ) have hord : orderOf ζ = p ^ 2 - 1 := by rw [orderOf_eq_card_of_forall_mem_zpowers hζ, Nat.card_eq_fintype_card, Fintype.card_units, hcardK] have hprim : IsPrimitiveRoot ζ (p ^ 2 - 1) := hord ▸ IsPrimitiveRoot.orderOf ζ have hp1 : p ^ 2 - 1 = (p - 1) * (p + 1) := by obtain ⟨q, hq⟩ : ∃ q, p = q + 1 := ⟨p - 1, by have := hp.out.one_lt; omega⟩ rw [hq, Nat.add_sub_cancel] apply Nat.sub_eq_of_eq_add ring have hpos : 0 < p ^ 2 - 1 := by have := hp.out.one_lt; rw [hp1]; exact Nat.mul_pos (by omega) (by omega) have hprim' : IsPrimitiveRoot ((ζ : K) ^ (p - 1)) (p + 1) := by rw [← Units.val_pow_eq_pow_val, IsPrimitiveRoot.coe_units_iff] exact hprim.pow hpos hp1 exact hprim'.card_nthRootsFinset · intro z hz have h := QuadraticAlgebra.algebraMap_norm_eq_mul_star z rw [hz, map_one] at h exact eq_inv_of_mul_eq_one_right h.symm omit [DecidableEq F] in include hcard in /-- 20:B6 — the quarter-turn `i ∈ F` (`i² = −1`) is Frobenius-fixed and off the circle: `N(i) = −1 ≠ 1`. -/ theorem quarter_turn_off_circle (i : F) (hi : i ^ 2 = -1) : star (algebraMap F K i) = algebraMap F K i ∧ QuadraticAlgebra.norm (algebraMap F K i) = -1 ∧ QuadraticAlgebra.norm (algebraMap F K i) ≠ 1 := by have h2 : (2 : F) ≠ 0 := two_ne_zero_of_nonsquare hcard ν have hn : QuadraticAlgebra.norm (algebraMap F K i) = -1 := by rw [QuadraticAlgebra.norm_algebraMap, hi] refine ⟨?_, hn, ?_⟩ · rw [star_eq, QuadraticAlgebra.algebraMap_eq]; simp · rw [hn]; intro h apply h2 linear_combination -h end frobenius /-! ## The scale-shift on the shell: the `𝔽_p` reading (rows E1, E12(iii), E13) -/ section spectrum variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] /-- 20:E1, 20:E12 — the scale-shift `S : x ↦ g^r x` is a permutation of `F^×` (a bijection, so its matrix on `ℓ²(F^×)` is a permutation matrix, hence unitary) with the power characters `x ↦ x^k` as eigenvectors in the `𝔽_p` reading, `S x^k = g^{rk} x^k`, and its fixed-point count — the trace of its permutation matrix — is `(p − 1)·[(p − 1) ∣ r]`, which carries no prime data. -/ theorem scale_shift (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (r : ℕ) : Function.Bijective (fun x : Fˣ => (Units.mk0 g (hg.ne_zero (by have := Fintype.one_lt_card (α := F); omega))) ^ r * x) ∧ (∀ (k : ℕ) (x : F), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧ (univ.filter (fun x : Fˣ => g ^ r * (x : F) = x)).card = if (Fintype.card F - 1) ∣ r then Fintype.card F - 1 else 0 := by refine ⟨(Group.mulLeft_bijective _), fun k x => mul_pow _ _ _, ?_⟩ split_ifs with hdvd · have h1 : g ^ r = 1 := (hg.pow_eq_one_iff_dvd r).2 hdvd have : univ.filter (fun x : Fˣ => g ^ r * (x : F) = x) = univ := by ext x; simp [h1] rw [this, card_univ, Fintype.card_units] · have h1 : g ^ r ≠ 1 := fun h => hdvd ((hg.pow_eq_one_iff_dvd r).1 h) have : univ.filter (fun x : Fˣ => g ^ r * (x : F) = x) = ∅ := by rw [Finset.filter_eq_empty_iff] intro x _ h apply h1 have hx : (x : F) ≠ 0 := x.ne_zero calc g ^ r = g ^ r * (x : F) * (x : F)⁻¹ := by rw [mul_assoc, mul_inv_cancel₀ hx, mul_one] _ = 1 := by rw [h, mul_inv_cancel₀ hx] rw [this, card_empty] /-- 20:E12, 20:E13 — the `𝔽_p`-valued power characters are never orthonormal: the self-pairing `Σ_{x ∈ F^×} x^j · x^j` is `0` or `−1`, never `1`, on every odd shell. -/ theorem power_characters_not_orthonormal (h2 : (2 : F) ≠ 0) (j : ℕ) : ∑ x : Fˣ, ((x : F) ^ j * (x : F) ^ j) ≠ 1 := by have : ∑ x : Fˣ, ((x : F) ^ j * (x : F) ^ j) = ∑ x : Fˣ, ((x : F) ^ (2 * j)) := sum_congr rfl fun x _ => by rw [← pow_add, two_mul] rw [this, FiniteField.sum_pow_units] split_ifs · intro h; apply h2; linear_combination -h · exact zero_ne_one end spectrum /-! ## Frame coincidence below the horizon (row B2) -/ section coincidence /-- 20:B2 — below the horizon the reading is frame-exact: on any shell `ZMod q` with `H² < q`, residues `n ≤ H` are the integers themselves and window products read back exactly, so the Subject `𝔽_p` and the Carrier `𝔽_Ω` agree on the window. -/ theorem window_readback {q : ℕ} [NeZero q] {H : ℕ} (hH : H * H < q) : (∀ m, m ≤ H → ((m : ZMod q)).val = m) ∧ ∀ a b, a ≤ H → b ≤ H → ((a : ZMod q) * b).val = a * b := by have hle : ∀ m, m ≤ H → m < q := fun m hm => by rcases Nat.eq_zero_or_pos H with h | h · subst h; have := Nat.pos_of_ne_zero (NeZero.ne q); omega · exact lt_of_le_of_lt (le_trans hm (Nat.le_mul_self H)) hH refine ⟨fun m hm => ZMod.val_natCast_of_lt (hle m hm), fun a b ha hb => ?_⟩ rw [← Nat.cast_mul, ZMod.val_natCast_of_lt] exact lt_of_le_of_lt (Nat.mul_le_mul ha hb) hH /-- 20:B2 — primality equals irreducibility in the window: for `2 ≤ m ≤ H` and any shell with `H² < q`, `m` is prime iff it admits no factorisation `a · b = m` with `2 ≤ a, b ≤ H` read on the shell. -/ theorem prime_iff_window_irreducible {q : ℕ} [NeZero q] {H : ℕ} (hH : H * H < q) (m : ℕ) (hm2 : 2 ≤ m) (hmH : m ≤ H) : Nat.Prime m ↔ ¬ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (a : ZMod q) * b = m := by have hrb := window_readback (q := q) hH constructor · rintro hp ⟨a, b, ha2, hb2, haH, hbH, hab⟩ have hval := congrArg ZMod.val hab rw [hrb.2 a b haH hbH, hrb.1 m hmH] at hval have hdvd : a ∣ m := ⟨b, hval.symm⟩ rcases (Nat.dvd_prime hp).1 hdvd with h | h · omega · rw [h] at hval have hb1 : b = 1 := Nat.eq_of_mul_eq_mul_left (show 0 < m by omega) (show m * b = m * 1 by rw [Nat.mul_one]; exact hval) omega · intro h rw [Nat.prime_def] refine ⟨hm2, fun a ham => ?_⟩ by_contra hane push Not at hane obtain ⟨b, hb⟩ := ham have hb0 : b ≠ 0 := by rintro rfl; rw [Nat.mul_zero] at hb; omega have hb1 : b ≠ 1 := by rintro rfl; rw [Nat.mul_one] at hb; exact hane.2 hb.symm have ha0 : a ≠ 0 := by rintro rfl; rw [Nat.zero_mul] at hb; omega apply h refine ⟨a, b, by omega, by omega, le_trans (Nat.le_of_dvd (by omega) ⟨b, hb⟩) hmH, le_trans (Nat.le_of_dvd (by omega) ⟨a, by rw [mul_comm]; exact hb⟩) hmH, ?_⟩ rw [← Nat.cast_mul, ← hb] /-- 20:B2 — `⌊√p⌋² < p` for a prime `p`: the horizon window `H = ⌊√p⌋` is wrap-free. -/ lemma sqrt_sq_lt_prime {p : ℕ} (hp : p.Prime) : Nat.sqrt p * Nat.sqrt p < p := by rcases lt_or_eq_of_le (Nat.sqrt_le p) with h | h · exact h · exfalso have hdvd : Nat.sqrt p ∣ p := ⟨Nat.sqrt p, h.symm⟩ rcases (Nat.dvd_prime hp).1 hdvd with h1 | h1 · rw [h1] at h; have := hp.one_lt; omega · rw [h1] at h have := hp.one_lt nlinarith end coincidence /-! ## The laboratory pair (13, 233) (row B1) -/ section lab /-- 20:B1 [value] — the laboratory pair `(13, 233)`: nested, `13² < 233`; the two cycles share the quarter-turn core `Q₄` and nothing else, `gcd(12, 232) = 4`, with `5² = −1` on `𝔽₁₃` and `89² = −1` on `𝔽₂₃₃`; and `12 ∤ 232`. -/ theorem lab_pair : 13 * 13 < 233 ∧ Nat.gcd 12 232 = 4 ∧ (5 : ZMod 13) ^ 2 = -1 ∧ (89 : ZMod 233) ^ 2 = -1 ∧ ¬ 12 ∣ 232 := by decide /-- 20:B1 — no projection of the Carrier's cycle onto the Subject's: there is no surjective homomorphism `C_{232} → C_{12}`, since `12 ∤ 232`. -/ theorem no_cycle_projection : ¬ ∃ f : Multiplicative (ZMod 232) →* Multiplicative (ZMod 12), Function.Surjective f := by rintro ⟨f, hf⟩ have := Subgroup.card_dvd_of_surjective f hf rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card] at this simp only [Fintype.card_multiplicative, ZMod.card] at this exact absurd this (by decide) end lab /-! ## The Gauss sum (26:B5) -/ section gauss /-- 26:B5 — **the Gauss-sum product**: on a finite field `F` (every prime shell), for a nontrivial multiplicative character `χ` into a domain and a primitive additive character `ψ`, `g(χ, ψ) · g(χ⁻¹, ψ⁻¹) = |F|` (Mathlib's `gaussSum_mul_gaussSum_eq_card`); over the complex numbers the second factor is the conjugate of the first, so the modulus squared is `|F|` (the chart theme's `gauss_modulus`). The shell's own telescoping is the core's `ramanujan_sum` and `principal_root`. -/ theorem gauss_product {F : Type*} [Field F] [Fintype F] {R' : Type*} [CommRing R'] [IsDomain R'] {χ : MulChar F R'} (hχ : χ ≠ 1) {ψ : AddChar F R'} (hψ : ψ.IsPrimitive) : gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card F := gaussSum_mul_gaussSum_eq_card hχ hψ end gauss end FRC.HorizonML /-! inlined: FrcLedger/Theme/Chart.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Chart — the chart theme: the readings against the continuum (ledger migration, task LM30) The chart theme holds the readings of the finite results against the continuum, the only theme with the reals (`frc/themes.py`, rank 30). It serves the chart clauses of the master's scale import (00:A7, `scale_import`; the ledger's `ln Ω` for L8, `ln_omega_ledger`), its cosmology and prediction rows: the floor `a₀ = cH₀/2π` (00:L1), the octant record depth and its outputs (00:L3), the primordial tilt (00:L8) and the running floor (00:P1). The chart's numerals — the speed of light, the megaparsec, the Julian year, the fitted values and their errors — are declared data. The octant's theorems moved here from 14-entropy and the floor's from 21-gravity (6 October 2026); those modules keep the old names as aliases. Classical (tier 2) on Mathlib's hierarchy. Every bracket is certified from `π` to six places (`Real.pi_gt_d6`, `Real.pi_lt_d6`), `e` to nine (`Real.exp_one_gt_d9`, `Real.exp_one_lt_d9`) and the Taylor tail of `exp` (`Real.exp_bound`, `Real.exp_bound'`). The realisation content behind each reading — that the octant is the record depth, that the floor is the synchronisation threshold, that `ln Ω` is the tilt's e-fold count — is the rows' realisation clause, not formal content. -/ namespace FRC.Chart open Real /-! ## The scale import's chart numerals (00:A7; 14:A1, C1) -/ section scale /-- 00:A7 [chart] — the scale import's numerals: with the fit's `Λ = 1.088 × 10⁻⁵² m⁻²` (Planck 2018) and the Planck length `ℓ_P = 1.616255 × 10⁻³⁵ m` declared [data], the de Sitter radius `r_H = c/H_Λ`, `r_H² = 3/Λ`, gives `S = π (r_H/ℓ_P)²` between `3.31` and `3.32 × 10¹²²` (the row's `3.3 × 10¹²²`) and `Ω = 4S + 1` between `1.32` and `1.33 × 10¹²³` (the row's `1.3 × 10¹²³`). That the datum fixes the cardinality is the import; nothing here derives the datum. -/ theorem scale_import (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (3.31e122 : ℝ) < S ∧ S < 3.32e122 ∧ (1.32e123 : ℝ) < Ω ∧ Ω < 1.33e123 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp subst hΛ hℓ have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity have hSlo : (3.3160599e122 : ℝ) < S := by rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith have hShi : S < (3.3160611e122 : ℝ) := by rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith subst hΩ refine ⟨by linarith, by linarith, by linarith, by linarith⟩ set_option exponentiation.threshold 512 in /-- 00:L8 [chart] — the ledger's `ln Ω = 283.5`, the numeral the tilt reads, derived from the scale import: with the same `Λ`, `ℓ_P`, `r_H² = 3/Λ`, `S = π (r_H/ℓ_P)²` and `Ω = 4S + 1`, `ln Ω` lies between `283.50` and `283.51`. The logarithm is bracketed by `409 ln 2` (`Real.log_two_gt_d9`, `log_two_lt_d9`) and `1 − 1/m ≤ ln m ≤ m − 1` on the mantissa `m = Ω/2⁴⁰⁹`. -/ theorem ln_omega_ledger (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (283.50 : ℝ) < Real.log Ω ∧ Real.log Ω < 283.51 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp subst hΛ hℓ have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity have hSlo : (3.3160599e122 : ℝ) < S := by rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith have hShi : S < (3.3160611e122 : ℝ) := by rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith subst hΩ have hΩpos : (0 : ℝ) < 4 * S + 1 := by linarith have hmpos : (0 : ℝ) < (4 * S + 1) / 2 ^ 409 := by positivity have hlog : Real.log (4 * S + 1) = 409 * Real.log 2 + Real.log ((4 * S + 1) / 2 ^ 409) := by have e : (4 * S + 1 : ℝ) = 2 ^ 409 * ((4 * S + 1) / 2 ^ 409) := by field_simp conv_lhs => rw [e] rw [Real.log_mul (by positivity) (by positivity), Real.log_pow]; push_cast; ring have hl1 := Real.log_two_gt_d9 have hl2 := Real.log_two_lt_d9 have hm1 : (1.0032614 : ℝ) < (4 * S + 1) / 2 ^ 409 := by rw [lt_div_iff₀ (by positivity)]; norm_num; linarith have hm2 : (4 * S + 1) / 2 ^ 409 < (1.0032619 : ℝ) := by rw [div_lt_iff₀ (by positivity)]; norm_num; linarith have hup := Real.log_le_sub_one_of_pos hmpos have hlo := Real.one_sub_inv_le_log_of_pos hmpos have hinv : 1 / ((4 * S + 1) / 2 ^ 409) < 1 / (1.0032614 : ℝ) := one_div_lt_one_div_of_lt (by norm_num) hm1 rw [inv_eq_one_div] at hlo have hA : (0.00325 : ℝ) < Real.log ((4 * S + 1) / 2 ^ 409) := by have : (1 : ℝ) - 1 / 1.0032614 > 0.00325 := by norm_num linarith have hB : Real.log ((4 * S + 1) / 2 ^ 409) < (0.003262 : ℝ) := by linarith rw [hlog] exact ⟨by linarith, by linarith⟩ set_option exponentiation.threshold 512 in /-- 22:C14, P5 [chart] — **the granularity ceiling at the anchor**: with the scale import's `Ω = 4S + 1` (`S = π (r_H/ℓ_P)²`, the same hypotheses as `scale_import`), `2⁴⁰⁸ < Ω` and `Ω/4 < 2⁴⁰⁸`, so the largest depth `k` with `T(k) = 2^{k + [k odd]} < Ω` is `k* = 408` (the odd `409` would need `4 · 2⁴⁰⁸ < Ω`); and `2²⁰⁴ < √Ω`, `√Ω/4 < 2²⁰⁴`, so at the coherence horizon `k* = 204`. Every quantity compared is below `Ω`. -/ theorem ceiling_bracket (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (2 : ℝ) ^ 408 < Ω ∧ Ω / 4 < (2 : ℝ) ^ 408 ∧ (2 : ℝ) ^ 204 < √Ω ∧ √Ω / 4 < (2 : ℝ) ^ 204 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp subst hΛ hℓ have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity have hSlo : (3.3160599e122 : ℝ) < S := by rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith have hShi : S < (3.3160611e122 : ℝ) := by rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith subst hΩ have h1 : (2 : ℝ) ^ 408 < 4 * S + 1 := by norm_num; linarith have h2 : (4 * S + 1) / 4 < (2 : ℝ) ^ 408 := by norm_num; linarith have hΩpos : (0 : ℝ) < 4 * S + 1 := by linarith refine ⟨h1, h2, ?_, ?_⟩ · rw [Real.lt_sqrt (by positivity)] calc ((2 : ℝ) ^ 204) ^ 2 = 2 ^ 408 := by norm_num _ < 4 * S + 1 := h1 · have hsq : (√(4 * S + 1) / 4) ^ 2 < ((2 : ℝ) ^ 204) ^ 2 := by rw [div_pow, Real.sq_sqrt (le_of_lt hΩpos)] calc (4 * S + 1) / 4 ^ 2 = (4 * S + 1) / 4 / 4 := by ring _ < (2 : ℝ) ^ 408 / 4 := by exact div_lt_div_of_pos_right h2 (by norm_num) _ < (2 : ℝ) ^ 408 := by have : (0 : ℝ) < 2 ^ 408 := by positivity linarith _ = ((2 : ℝ) ^ 204) ^ 2 := by norm_num exact lt_of_pow_lt_pow_left₀ 2 (by positivity) hsq /-- 22:A5, Z2 [chart] — **the Ω ledger's floors**: every null channel's floor lies below the anchor — the Riemann height `(3 × 10¹²)⁴ = 8.1 × 10⁴⁹` (the binding floor, through the decidability horizon `Ω^{1/4}`), the Sorkin and Born tallies `10²²` (one floor, cited twice by the paper's ledger file), the granularity `2⁶⁰` — with the same hypotheses as `scale_import`. -/ theorem omega_floors (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (3e12 : ℝ) ^ 4 = 8.1e49 ∧ (3e12 : ℝ) ^ 4 < Ω ∧ (1e22 : ℝ) < Ω ∧ (2 : ℝ) ^ 60 < Ω := by obtain ⟨-, -, hlo, -⟩ := scale_import Λ ℓP r S Ω hΛ hℓ hr2 hS hΩ refine ⟨by norm_num, ?_, ?_, ?_⟩ <;> norm_num <;> linarith end scale /-! ## 22-quantum: the Tsirelson value, the singlet law and the channel against the continuum (22:C17, X7, P3, C25; C19, P1; 15 October 2026) -/ section quantum /-- The primitive eighth root `ζ₈ = e^{iπ/4}`. -/ noncomputable def zeta8 : ℂ := Complex.exp ((π / 4 : ℝ) * Complex.I) theorem zeta8_pow_four : zeta8 ^ 4 = -1 := by unfold zeta8 rw [← Complex.exp_nat_mul] have : (4 : ℕ) * ((π / 4 : ℝ) * Complex.I) = (π : ℂ) * Complex.I := by push_cast; ring rw [this, Complex.exp_pi_mul_I] theorem zeta8_inv : zeta8⁻¹ = Complex.exp (-((π / 4 : ℝ) * Complex.I)) := by unfold zeta8; rw [← Complex.exp_neg] /-- 22:C17, X7, P3, C25 — **the Tsirelson value is `2√2`**: `ζ₈ + ζ₈⁻¹ = 2 cos(π/4) = √2`, so `S = 2(ζ₈ + ζ₈⁻¹) = 2√2` as a real number and `S² = 8`. -/ theorem tsirelson_real : zeta8 + zeta8⁻¹ = (Real.sqrt 2 : ℂ) ∧ 2 * (zeta8 + zeta8⁻¹) = (2 * Real.sqrt 2 : ℝ) ∧ (2 * (zeta8 + zeta8⁻¹)) ^ 2 = 8 := by have hcos : zeta8 + zeta8⁻¹ = 2 * Complex.cos ((π / 4 : ℝ) : ℂ) := by rw [zeta8_inv, Complex.two_cos, neg_mul]; rfl have hval : zeta8 + zeta8⁻¹ = (Real.sqrt 2 : ℂ) := by rw [hcos, ← Complex.ofReal_cos, Real.cos_pi_div_four] push_cast; ring refine ⟨hval, ?_, ?_⟩ · rw [hval]; push_cast; ring · rw [hval] have : ((Real.sqrt 2 : ℝ) : ℂ) ^ 2 = 2 := by rw [← Complex.ofReal_pow, Real.sq_sqrt (by norm_num)]; push_cast; ring calc (2 * (Real.sqrt 2 : ℂ)) ^ 2 = 4 * ((Real.sqrt 2 : ℝ) : ℂ) ^ 2 := by ring _ = 8 := by rw [this]; norm_num /-- 22:C17 — the singlet law: the correlator at `Δ` setting steps is the real part of `ζ₈₀^Δ = e^{2πiΔ/80}`, `E(Δ) = cos(πΔ/40)`. -/ theorem singlet_law (Δ : ℕ) : (Complex.exp ((2 * π * Δ / 80 : ℝ) * Complex.I)).re = Real.cos (π * Δ / 40) := by rw [Complex.exp_ofReal_mul_I_re] congr 1 ring /-- 22:C19, P1 — the channel's chart: with the branch phase `φ`, the visibility `V = (x + x⁻¹)/2 = cos(φ/2)` and the concurrence `C = (x − x⁻¹)/(2i) = sin(φ/2)` for `x = e^{iφ/2}`, so `V² + C² = 1` and `C² = sin²(φ/2)`; at `φ = 0` the concurrence vanishes. -/ theorem channel_chart (φ : ℝ) : (Complex.exp ((φ / 2 : ℝ) * Complex.I) + Complex.exp (-((φ / 2 : ℝ) * Complex.I))) / 2 = (Real.cos (φ / 2) : ℂ) ∧ (Complex.exp ((φ / 2 : ℝ) * Complex.I) - Complex.exp (-((φ / 2 : ℝ) * Complex.I))) / (2 * Complex.I) = (Real.sin (φ / 2) : ℂ) ∧ Real.cos (φ / 2) ^ 2 + Real.sin (φ / 2) ^ 2 = 1 ∧ Real.sin (0 / 2) = 0 := by refine ⟨?_, ?_, Real.cos_sq_add_sin_sq _, by simp⟩ · rw [Complex.ofReal_cos, Complex.cos, neg_mul] · rw [Complex.ofReal_sin, Complex.sin, neg_mul] have hI : Complex.I ≠ 0 := Complex.I_ne_zero field_simp linear_combination (Complex.exp ((φ / 2 : ℝ) * Complex.I) - Complex.exp (-((φ / 2 : ℝ) * Complex.I))) * Complex.I_sq /-- 22:C19 — the channel entangles: off the trivial phase, `0 < φ < 2π`, the concurrence `C = sin(φ/2)` is not zero. -/ theorem channel_entangles (φ : ℝ) (h0 : 0 < φ) (h1 : φ < 2 * π) : Real.sin (φ / 2) ≠ 0 := ne_of_gt (Real.sin_pos_of_pos_of_lt_pi (by linarith) (by linarith)) end quantum /-! ## 26-pnp: the carrier family, the table beyond the horizon and the dilation generator (26:C2, B4) -/ section pnp set_option exponentiation.threshold 512 in /-- 26:C2 [chart] — **the family's size and the table beyond the horizon**: with the scale import's `Ω = 4S + 1` (the hypotheses of `scale_import`), `2²⁰⁴ < √Ω < 2²⁰⁵`, so the shells of the family `P² < Ω` have at most `205` bits, and `2¹⁰² < Ω^{1/4} < 2¹⁰³`, so a decision table with one entry per input of `204` bits has `2²⁰⁴` entries, below `√Ω` and beyond the absolute horizon `Ω^{1/4}` by more than `2¹⁰¹`. No numeral formed exceeds `Ω` (the largest is `2⁴⁰⁸`). -/ theorem family_bits (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (2 : ℝ) ^ 204 < √Ω ∧ √Ω < (2 : ℝ) ^ 205 ∧ (2 : ℝ) ^ 102 < √(√Ω) ∧ √(√Ω) < (2 : ℝ) ^ 103 := by obtain ⟨h1, h2, h3, -⟩ := ceiling_bracket Λ ℓP r S Ω hΛ hℓ hr2 hS hΩ have hΩpos : (0 : ℝ) < Ω := lt_trans (by positivity) h1 -- `√Ω / 2 = √(Ω / 4) < 2²⁰⁴` from `Ω / 4 < 2⁴⁰⁸ = (2²⁰⁴)²`: the largest numeral formed is `2⁴⁰⁸ < Ω` (the G18 round of -- 16 October 2026: the first proof bounded `Ω` by a power of two above it, a numeral the corpus does not form) have hhalf : √Ω / 2 < (2 : ℝ) ^ 204 := by have e : √Ω / 2 = √(Ω / 4) := by rw [Real.sqrt_div' _ (by norm_num : (0 : ℝ) ≤ 4), show √(4 : ℝ) = 2 by rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.sqrt_sq (by norm_num)]] rw [e, Real.sqrt_lt' (by positivity)] calc Ω / 4 < (2 : ℝ) ^ 408 := h2 _ = ((2 : ℝ) ^ 204) ^ 2 := by norm_num have h5 : √Ω < (2 : ℝ) ^ 205 := by have : (2 : ℝ) ^ 205 = 2 * 2 ^ 204 := by norm_num rw [this]; linarith refine ⟨h3, h5, ?_, ?_⟩ · rw [Real.lt_sqrt (by positivity)] calc ((2 : ℝ) ^ 102) ^ 2 = 2 ^ 204 := by norm_num _ < √Ω := h3 · rw [Real.sqrt_lt' (by positivity)] calc √Ω < (2 : ℝ) ^ 205 := h5 _ < ((2 : ℝ) ^ 103) ^ 2 := by norm_num /-- 26:B5 — **the Gauss-sum modulus**: over `ℂ`, on a finite field `F`, for a nontrivial multiplicative character `χ` and a primitive additive character `ψ`, `g(χ⁻¹, ψ⁻¹)` is the complex conjugate of `g(χ, ψ)` (Mathlib's `star_gaussSum_eq`), so with the horizon theme's `gauss_product`, `g(χ) · conj g(χ) = |g(χ)|² = |F|`: on the prime shell `𝔽_P`, `P`. -/ theorem gauss_modulus {F : Type*} [Field F] [Fintype F] {χ : MulChar F ℂ} (hχ : χ ≠ 1) {ψ : AddChar F ℂ} (hψ : ψ.IsPrimitive) : gaussSum χ ψ * star (gaussSum χ ψ) = Fintype.card F ∧ Complex.normSq (gaussSum χ ψ) = Fintype.card F := by have h := FRC.HorizonML.gauss_product hχ hψ rw [← star_gaussSum_eq] at h refine ⟨h, ?_⟩ have h2 : (Complex.normSq (gaussSum χ ψ) : ℂ) = (Fintype.card F : ℂ) := by rw [← Complex.mul_conj, ← h]; rfl exact_mod_cast h2 /-- 26:B4 [chart] — **the dilation generator**: `Ĥ = −i(x ∂ₓ + ½)` has `x^{−1/2 + iν}` as eigenfunction of eigenvalue `ν` on `x > 0`; the frequency index is the spectrum of `Ĥ` in the continuum reading of the scale shift (20:E1). -/ theorem dilation_eigen (ν x : ℝ) (hx : 0 < x) : -Complex.I * ((x : ℂ) * deriv (fun t : ℝ => (t : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν)) x + (1 / 2 : ℂ) * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν)) = ν * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν) := by set s : ℂ := -(1 / 2 : ℂ) + Complex.I * ν with hs have hx0 : (x : ℂ) ≠ 0 := by exact_mod_cast hx.ne' have hslit : (x : ℂ) ∈ Complex.slitPlane := Complex.ofReal_mem_slitPlane.2 hx have hd : HasDerivAt (fun t : ℝ => (t : ℂ) ^ s) (s * (x : ℂ) ^ (s - 1)) x := (Complex.hasStrictDerivAt_cpow_const hslit).hasDerivAt.comp_ofReal rw [hd.deriv] have hpow : (x : ℂ) * (x : ℂ) ^ (s - 1) = (x : ℂ) ^ s := by rw [Complex.cpow_sub _ _ hx0, Complex.cpow_one, mul_div_cancel₀ _ hx0] have hcoef : -Complex.I * (s + 1 / 2) = ν := by rw [hs]; ring_nf; rw [Complex.I_sq]; ring calc -Complex.I * ((x : ℂ) * (s * (x : ℂ) ^ (s - 1)) + (1 / 2 : ℂ) * (x : ℂ) ^ s) = -Complex.I * (s + 1 / 2) * (x : ℂ) ^ s := by rw [← hpow]; ring _ = ν * (x : ℂ) ^ s := by rw [hcoef] end pnp /-! ## The octant record depth and its outputs (00:L3; 14:C5, C7, P3) -/ section octant /-- 00:L3, 14:C5 [chart] — the chart conversion of the octant: the count `S/2` out of the `4S`-cycle, read on the meridian circle `2π r_H/c`, is the depth `(π/4) r_H/c`. -/ theorem octant_chart (S r c : ℝ) (hS : S ≠ 0) : (S / 2) / (4 * S) * (2 * π * r / c) = (π / 4) * r / c := by rcases eq_or_ne c 0 with rfl | hc · simp · field_simp /-- The octant's rate factor `tanh(3π/8)` is positive. -/ theorem tanh_octant_pos : 0 < tanh (3 * π / 8) := by rw [Real.tanh_eq_sinh_div_cosh] exact div_pos (Real.sinh_pos_iff.2 (by positivity)) (Real.cosh_pos _) /-- 00:L3, 14:P3 [ΛCDM] — the algebraic locus: with `t H_Λ = π/4` (the octant), `H_Λ = H₀ √Ω_Λ` and `Ω_Λ = tanh²(3π/8)`, `t H₀ = (π/4)/tanh(3π/8)`; the numeral `0.950` is bracketed in `locus_bracket`. -/ theorem age_rate_locus (t H0 HΛ Ω : ℝ) (hoct : t * HΛ = π / 4) (hΛ : HΛ = H0 * √Ω) (hΩ : Ω = tanh (3 * π / 8) ^ 2) : t * H0 = (π / 4) / tanh (3 * π / 8) := by have hpos := tanh_octant_pos rw [hΩ, Real.sqrt_sq hpos.le] at hΛ rw [eq_div_iff hpos.ne', ← hoct, hΛ]; ring /-- 00:L3, 14:A8 [ΛCDM] — the rival chart's age identity as the import it is: in flat matter-plus-`Λ` the product of the age and the asymptotic rate is `t₀H_Λ = (2/3) artanh √Ω_Λ`, a function of the one fitted parameter; outside `[0, 1)` the value is junk. Moved here from 14-entropy (task LM30's repair, 7 October 2026), which keeps the name. -/ noncomputable def lcdmAge (Ω : ℝ) : ℝ := 2 / 3 * artanh (√Ω) /-- 00:L3, 14:C7, 14:X3 [ΛCDM] — the octant inversion: the rival chart's identity gives `t₀H_Λ = π/4` at `Ω_Λ = tanh²(3π/8)` and, for `0 ≤ Ω_Λ < 1`, only there. Moved here from 14-entropy, which keeps the name. -/ theorem octant_inversion : lcdmAge (tanh (3 * π / 8) ^ 2) = π / 4 ∧ ∀ Ω : ℝ, 0 ≤ Ω → Ω < 1 → lcdmAge Ω = π / 4 → Ω = tanh (3 * π / 8) ^ 2 := by have hpos := tanh_octant_pos constructor · unfold lcdmAge rw [Real.sqrt_sq hpos.le, Real.artanh_tanh]; ring · intro Ω h0 h1 h unfold lcdmAge at h have hart : artanh (√Ω) = 3 * π / 8 := by linarith have hΩ : √Ω ∈ Set.Ioo (-1 : ℝ) 1 := by refine ⟨by linarith [Real.sqrt_nonneg Ω], ?_⟩ rw [Real.sqrt_lt' one_pos]; simpa using h1 have := Real.tanh_artanh hΩ rw [hart] at this rw [this, Real.sq_sqrt h0] /-- `tanh x = (e^{2x} − 1)/(e^{2x} + 1)`. -/ theorem tanh_eq_exp_two_mul (x : ℝ) : tanh x = (exp (2 * x) - 1) / (exp (2 * x) + 1) := by rw [Real.tanh_eq, Real.exp_neg, two_mul, Real.exp_add] have h := Real.exp_pos x field_simp /-- The Taylor brackets of `e^t` at the two ends of `t = 3π/4 − 2`: seven terms of the series with the tail bound of Mathlib's `Real.exp_bound`. -/ theorem exp_tail_bounds : (1.427884 : ℝ) < exp 0.356194 ∧ exp (0.35619475 : ℝ) < 1.4278857 := by constructor · have h := abs_le.1 (Real.exp_bound (x := 0.356194) (by rw [abs_of_pos (by norm_num)]; norm_num) (n := 7) (by norm_num)) rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.356194)] at h have h1 := h.1 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢ linarith · have h := Real.exp_bound' (x := 0.35619475) (by norm_num) (by norm_num) (n := 7) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢ linarith /-- `e^{3π/4}` bracketed: `10.55071 < e^{3π/4} < 10.55073`, from `π` to six places, `e` to nine, and the Taylor tail. -/ theorem exp_three_pi_four_bounds : (10.55071 : ℝ) < exp (3 * π / 4) ∧ exp (3 * π / 4) < 10.55073 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have he1 := Real.exp_one_gt_d9 have he2 := Real.exp_one_lt_d9 have ht := exp_tail_bounds have hsplit : exp (3 * π / 4) = exp 1 * exp 1 * exp (3 * π / 4 - 2) := by rw [← Real.exp_add, ← Real.exp_add]; congr 1; ring have hlo : exp 0.356194 < exp (3 * π / 4 - 2) := Real.exp_lt_exp.2 (by linarith) have hhi : exp (3 * π / 4 - 2) < exp 0.35619475 := Real.exp_lt_exp.2 (by linarith) have hpos : (0 : ℝ) < exp 1 := Real.exp_pos 1 rw [hsplit] constructor · nlinarith [mul_pos hpos hpos, Real.exp_pos (3 * π / 4 - 2)] · nlinarith [mul_pos hpos hpos, Real.exp_pos (3 * π / 4 - 2)] /-- `tanh(3π/8)` bracketed: `0.82685 < tanh(3π/8) < 0.826851`, from `exp_three_pi_four_bounds`. -/ theorem tanh_octant_bounds : (0.82685 : ℝ) < tanh (3 * π / 8) ∧ tanh (3 * π / 8) < 0.826851 := by obtain ⟨hE1, hE2⟩ := exp_three_pi_four_bounds have htanh : tanh (3 * π / 8) = (exp (3 * π / 4) - 1) / (exp (3 * π / 4) + 1) := by rw [tanh_eq_exp_two_mul]; congr 2 <;> ring_nf have hden : (0 : ℝ) < exp (3 * π / 4) + 1 := by linarith constructor · rw [htanh, lt_div_iff₀ hden]; linarith · rw [htanh, div_lt_iff₀ hden]; linarith /-- 00:L3, 14:P3 — the locus's numeral bracketed: `0.9498 < (π/4)/tanh(3π/8) < 0.9499`, the paper's `0.950`. -/ theorem locus_bracket : (0.9498 : ℝ) < (π / 4) / tanh (3 * π / 8) ∧ (π / 4) / tanh (3 * π / 8) < 0.9499 := by obtain ⟨hl, hu⟩ := tanh_octant_bounds have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hpos : (0 : ℝ) < tanh (3 * π / 8) := by linarith constructor · rw [lt_div_iff₀ hpos]; nlinarith · rw [div_lt_iff₀ hpos]; nlinarith /-- The locus to six places: `0.949866 < (π/4)/tanh(3π/8) < 0.949868`, for the rates read on it. -/ theorem locus_fine : (0.949866 : ℝ) < (π / 4) / tanh (3 * π / 8) ∧ (π / 4) / tanh (3 * π / 8) < 0.949868 := by obtain ⟨hl, hu⟩ := tanh_octant_bounds have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hpos : (0 : ℝ) < tanh (3 * π / 8) := by linarith constructor · rw [lt_div_iff₀ hpos]; nlinarith · rw [div_lt_iff₀ hpos]; nlinarith /-- 00:L3, 14:C7, 14:X3 — the landing bracketed: `0.68368 < tanh²(3π/8) < 0.68369` (the numeral `0.684`) is certified from `π` to six places, `e` to nine and the Taylor tail; and, with the Planck numerals `0.685 ± 0.007` taken as data, the deviation lies between `0.18σ` and `0.19σ`. -/ theorem landing_bracket : (0.68368 : ℝ) < tanh (3 * π / 8) ^ 2 ∧ tanh (3 * π / 8) ^ 2 < 0.68369 ∧ 0.18 * 0.007 < 0.685 - tanh (3 * π / 8) ^ 2 ∧ 0.685 - tanh (3 * π / 8) ^ 2 < 0.19 * 0.007 := by obtain ⟨hl, hu⟩ := tanh_octant_bounds have hsq1 : (0.82685 : ℝ) ^ 2 < tanh (3 * π / 8) ^ 2 := by apply pow_lt_pow_left₀ hl (by norm_num) (by norm_num) have hsq2 : tanh (3 * π / 8) ^ 2 < (0.826851 : ℝ) ^ 2 := by apply pow_lt_pow_left₀ hu (by linarith) (by norm_num) norm_num at hsq1 hsq2 refine ⟨by linarith, by linarith, by linarith, by linarith⟩ /-- 00:L3 — the deviation fixed to the row's rounded `0.19σ`: between `0.186σ` and `0.19σ` below Planck's `0.685 ± 0.007` (data). -/ theorem landing_fine : 0.186 * 0.007 < 0.685 - tanh (3 * π / 8) ^ 2 ∧ 0.685 - tanh (3 * π / 8) ^ 2 < (0.19 * 0.007 : ℝ) := by obtain ⟨h1, h2, _, h4⟩ := landing_bracket exact ⟨by linarith, h4⟩ /-- 00:L3 [chart] — the channel-1 consistency: read on the depth `t = 13.79` Gyr (the row's depth numeral, a Julian year of `365.25` days; data), the locus `t H₀ = (π/4)/tanh(3π/8)` gives `67.35 < H₀ < 67.36` km s⁻¹ Mpc⁻¹ (the megaparsec `3.0856775814913673 × 10¹⁹` km; data): the channel-1 rate `67.4` to `0.1 %` (14:P3, "a consistency, not a prediction"). -/ theorem hubble_landing (t H0 : ℝ) (ht : t = 13.79e9 * (365.25 * 86400)) (hloc : t * H0 = (π / 4) / tanh (3 * π / 8)) : (67.35 : ℝ) < H0 * 3.0856775814913673e19 ∧ H0 * 3.0856775814913673e19 < 67.36 := by obtain ⟨hl, hu⟩ := locus_fine have htpos : (0 : ℝ) < t := by rw [ht]; norm_num have hH : H0 = (π / 4) / tanh (3 * π / 8) / t := by rw [eq_div_iff htpos.ne', mul_comm, hloc] constructor · rw [hH, ht, div_mul_eq_mul_div, lt_div_iff₀ (by norm_num)]; nlinarith · rw [hH, ht, div_mul_eq_mul_div, div_lt_iff₀ (by norm_num)]; nlinarith /-- 00:L3, 14:P3 [chart] — the locus read on the fit-independent stellar age `t★ = 13.61 ± 0.34` Gyr (data; a Julian year of `365.25` days): `68.24 < H₀ < 68.25` km s⁻¹ Mpc⁻¹ (the row's `68.2`); the age's error carried to the rate, `H₀ · 0.34/13.61`, lies between `1.70` and `1.71` (the row's `±1.7`); and the Cepheid ladder's `73.0 ± 1.0` (data), errors combined with `±1.7`, lies between `2.40σ` and `2.42σ` above it (the row's `2.4σ`). -/ theorem hubble_stellar (t H0 : ℝ) (ht : t = 13.61e9 * (365.25 * 86400)) (hloc : t * H0 = (π / 4) / tanh (3 * π / 8)) : (68.24 : ℝ) < H0 * 3.0856775814913673e19 ∧ H0 * 3.0856775814913673e19 < 68.25 ∧ (1.70 : ℝ) < H0 * 3.0856775814913673e19 * (0.34 / 13.61) ∧ H0 * 3.0856775814913673e19 * (0.34 / 13.61) < 1.71 ∧ (2.40 : ℝ) < (73.0 - H0 * 3.0856775814913673e19) / √(1.7 ^ 2 + 1.0 ^ 2) ∧ (73.0 - H0 * 3.0856775814913673e19) / √(1.7 ^ 2 + 1.0 ^ 2) < 2.42 := by obtain ⟨hl, hu⟩ := locus_fine have htpos : (0 : ℝ) < t := by rw [ht]; norm_num have hH : H0 = (π / 4) / tanh (3 * π / 8) / t := by rw [eq_div_iff htpos.ne', mul_comm, hloc] have h1 : (68.24 : ℝ) < H0 * 3.0856775814913673e19 := by rw [hH, ht, div_mul_eq_mul_div, lt_div_iff₀ (by norm_num)]; nlinarith have h2 : H0 * 3.0856775814913673e19 < (68.25 : ℝ) := by rw [hH, ht, div_mul_eq_mul_div, div_lt_iff₀ (by norm_num)]; nlinarith have hs1 : (1.9723 : ℝ) < √(1.7 ^ 2 + 1.0 ^ 2) := by rw [Real.lt_sqrt (by norm_num)]; norm_num have hs2 : √(1.7 ^ 2 + 1.0 ^ 2 : ℝ) < 1.9724 := by rw [Real.sqrt_lt' (by norm_num)]; norm_num have hspos : (0 : ℝ) < √(1.7 ^ 2 + 1.0 ^ 2) := by linarith refine ⟨h1, h2, by nlinarith, by nlinarith, ?_, ?_⟩ · rw [lt_div_iff₀ hspos]; nlinarith · rw [div_lt_iff₀ hspos]; nlinarith end octant /-! ## The floor and its running (00:L1, P1; 21:P3) -/ section floor /-- 00:L1, 21:P3 — the weak-acceleration floor `a₀ = cH₀/2π` at the entailed `H₀ = 67.4 km s⁻¹ Mpc⁻¹` (the speed of light and the megaparsec declared numerals [data]): `a₀` lies between `1.04` and `1.05 × 10⁻¹⁰ m s⁻²`; against the fitted `1.20 × 10⁻¹⁰` it is between `13.0 %` and `13.2 %` low, and the deficit is between `0.65` and `0.67` of the systematic `0.24 × 10⁻¹⁰` (the text's `13 %`, `0.7σ`). -/ theorem floor_value (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) : (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.05e-10 ∧ (0.868 : ℝ) < c * H0 / (2 * π) / 1.2e-10 ∧ c * H0 / (2 * π) / 1.2e-10 < 0.870 ∧ (0.65 : ℝ) < (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 ∧ (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 < 0.67 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 subst hc hH have hA : (1.042e-10 : ℝ) < 299792458 * (67.4e3 / 3.0856775814913673e22) / (2 * π) := by rw [lt_div_iff₀ (by positivity)]; nlinarith have hB : 299792458 * (67.4e3 / 3.0856775814913673e22) / (2 * π) < (1.0423e-10 : ℝ) := by rw [div_lt_iff₀ (by positivity)]; nlinarith refine ⟨by linarith, by linarith, ?_, ?_, ?_, ?_⟩ · rw [lt_div_iff₀ (by norm_num)]; linarith · rw [div_lt_iff₀ (by norm_num)]; linarith · rw [lt_div_iff₀ (by norm_num)]; linarith · rw [div_lt_iff₀ (by norm_num)]; linarith /-- 00:L1 — the floor fixed to the row's rounded `1.04 × 10⁻¹⁰`: at the channel-1 rate `H₀ = 67.4 km s⁻¹ Mpc⁻¹`, `1.04 × 10⁻¹⁰ < a₀ < 1.045 × 10⁻¹⁰ m s⁻²`. -/ theorem floor_fine (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) : (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.045e-10 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 subst hc hH constructor · rw [lt_div_iff₀ (by positivity)]; nlinarith · rw [div_lt_iff₀ (by positivity)]; nlinarith /-- 00:P1 [chart] — the running floor: if the floor is read at every redshift on the registered rate, `a₀(z) = cH(z)/2π`, and the deep-regime Tully–Fisher law `v⁴ = G M a₀` holds at fixed baryonic mass `M`, then `a₀(z)/a₀(0) = H(z)/H(0) = E(z)` and the zero-point evolves as `v(z)/v(0) = E(z)^{1/4}`; the rates and speeds are asked positive at `0` and `z` only. The law `v⁴ = G M a₀` is the deep regime's import. That the floor tracks the registered rate (the gravity realisation, 00:D5) is the row's realisation clause, not formal content. -/ theorem running_floor (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ) (hc : 0 < c) (hG : 0 < G) (hM : 0 < M) (h0 : 0 < H 0) (hz : 0 < H z) (ha : ∀ z, a z = c * H z / (2 * π)) (hv0 : 0 < v 0) (hvz : 0 < v z) (htf : ∀ z, v z ^ 4 = G * M * a z) : a z / a 0 = H z / H 0 ∧ v z / v 0 = (H z / H 0) ^ (1 / 4 : ℝ) := by have hpi := Real.pi_pos have hratio : a z / a 0 = H z / H 0 := by rw [ha z, ha 0]; field_simp refine ⟨hratio, ?_⟩ have ha0 : 0 < a 0 := by rw [ha 0]; positivity have h4 : (v z / v 0) ^ 4 = H z / H 0 := by rw [div_pow, htf z, htf 0, ← hratio]; field_simp rw [← h4, show (1 / 4 : ℝ) = ((4 : ℕ) : ℝ)⁻¹ by norm_num] exact (Real.pow_rpow_inv_natCast (div_pos hvz hv0).le (by norm_num)).symm end floor /-! ## The radial ladder of the minimal pair (38:B2) -/ section ladder /-- 38:B2 [chart] — the radial ladder of the sky: the shell radii `R sin(2aπ/13)`, `a = 1, 2, 3`, are positive, strictly increasing, and inside the rim `R` (the chart flattening of the latitude circles; the capacity `4a < p ⇔ a ≤ κ` is the core's `FRC.Pair.window`). -/ theorem ladder_monotone (R : ℝ) (hR : 0 < R) : 0 < R * Real.sin (2 * π / 13) ∧ R * Real.sin (2 * π / 13) < R * Real.sin (4 * π / 13) ∧ R * Real.sin (4 * π / 13) < R * Real.sin (6 * π / 13) ∧ R * Real.sin (6 * π / 13) < R := by have hpi := Real.pi_pos have mono : ∀ x y : ℝ, 0 ≤ x → x < y → y ≤ π / 2 → Real.sin x < Real.sin y := fun x y hx hxy hy => Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith) hy hxy refine ⟨mul_pos hR (Real.sin_pos_of_pos_of_lt_pi (by positivity) (by linarith)), ?_, ?_, ?_⟩ · exact mul_lt_mul_of_pos_left (mono _ _ (by positivity) (by linarith) (by linarith)) hR · exact mul_lt_mul_of_pos_left (mono _ _ (by positivity) (by linarith) (by linarith)) hR · have h := mono (6 * π / 13) (π / 2) (by positivity) (by linarith) le_rfl rw [Real.sin_pi_div_two] at h calc R * Real.sin (6 * π / 13) < R * 1 := mul_lt_mul_of_pos_left h hR _ = R := mul_one R end ladder /-! ## The primordial tilt (00:L8) -/ section tilt /-- 00:L8 [chart] — the tilt at the ledger's `ln Ω = 283.5` (`ln_omega_ledger`, from the scale import 00:A7; data): `n_s − 1 = −π²/ln Ω` has magnitude between `0.03481` and `0.03482` (the row's `−0.0348`); against Planck 2018's `−0.0351 ± 0.0042` (data) the deviation is between `+0.068σ` and `+0.069σ` (the row's `+0.07σ`); the count `½ ln Ω` gives `−π²/(ln Ω/2)`, off by between `8.2σ` and `8.25σ` (the row's exclusion at `8.2σ`). That `ln Ω` is the e-fold count of the frame's scale range is the row's realisation clause, not formal content. -/ theorem tilt_ledger : (0.03481 : ℝ) < π ^ 2 / 283.5 ∧ π ^ 2 / 283.5 < 0.03482 ∧ (0.068 * 0.0042 : ℝ) < 0.0351 - π ^ 2 / 283.5 ∧ 0.0351 - π ^ 2 / 283.5 < 0.069 * 0.0042 ∧ (8.2 * 0.0042 : ℝ) < π ^ 2 / (283.5 / 2) - 0.0351 ∧ π ^ 2 / (283.5 / 2) - 0.0351 < 8.25 * 0.0042 := by have hpi1 := Real.pi_gt_d6 have hpi2 := Real.pi_lt_d6 have hsq1 : (3.141592 : ℝ) ^ 2 < π ^ 2 := pow_lt_pow_left₀ hpi1 (by norm_num) (by norm_num) have hsq2 : π ^ 2 < (3.141593 : ℝ) ^ 2 := pow_lt_pow_left₀ hpi2 (by linarith) (by norm_num) norm_num at hsq1 hsq2 refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ · rw [lt_div_iff₀ (by norm_num)]; linarith · rw [div_lt_iff₀ (by norm_num)]; linarith · have : π ^ 2 / 283.5 < (0.0351 - 0.068 * 0.0042 : ℝ) := by rw [div_lt_iff₀ (by norm_num)]; norm_num; linarith linarith · have : (0.0351 - 0.069 * 0.0042 : ℝ) < π ^ 2 / 283.5 := by rw [lt_div_iff₀ (by norm_num)]; norm_num; linarith linarith · have : (8.2 * 0.0042 + 0.0351 : ℝ) < π ^ 2 / (283.5 / 2) := by rw [lt_div_iff₀ (by norm_num)]; norm_num; linarith linarith · have : π ^ 2 / (283.5 / 2) < (8.25 * 0.0042 + 0.0351 : ℝ) := by rw [div_lt_iff₀ (by norm_num)]; norm_num; linarith linarith /-- 00:L8 — the e-fold count of the frame's scale range: from `1/√Ω` to `√Ω` the logarithm spans `ln Ω`. -/ theorem efold_count (Ω : ℝ) (hΩ : 0 < Ω) : Real.log (√Ω / (1 / √Ω)) = Real.log Ω := by have hs : 0 < √Ω := Real.sqrt_pos.2 hΩ have e : √Ω / (1 / √Ω) = Ω := by rw [div_div_eq_mul_div, div_one, Real.mul_self_sqrt hΩ.le] rw [e] end tilt /-! ## 20-rh: the complex characters of the cycle, the characters as eigenvectors of the scale-shift, and the von Mangoldt weight (20:E1, E12, E13, C5, C2; task LM36) Moved here from 20-rh's `FrcLedger/Rh.lean` under the same names; that module keeps the old names as aliases. The exact shell arithmetic of the same rows is the horizon theme's (`Theme/Horizon.lean`, `FRC.HorizonML`). -/ section characters open Complex Finset variable {n : ℕ} [NeZero n] /-- The `j`-th chart mode of the cycle `C_n`: `χ_j(m) = e^{2πi·jm/n}`. On the shell, `m` is the discrete logarithm of the residue `g^m` and `n = p − 1`. -/ noncomputable def chi (j m : ZMod n) : ℂ := ZMod.stdAddChar (j * m) /-- The coefficient of `v` on the mode `χ_j`: `⟨v, χ_j⟩ = Σ_m v(m) χ_j(m)̄`. -/ noncomputable def coef (v : ZMod n → ℂ) (j : ZMod n) : ℂ := ∑ m, v m * (starRingEnd ℂ) (chi j m) lemma chi_conj (j m : ZMod n) : (starRingEnd ℂ) (chi j m) = ZMod.stdAddChar (-(j * m)) := by rw [chi, AddChar.map_neg_eq_conj] /-- 20:E13 — orthogonality of the chart modes: `Σ_m χ_j(m) χ_k(m)̄ = n·[j = k]`, each of squared norm `n = p − 1` (with `chi_inversion`, the `p − 1` characters are an orthogonal basis of `ℂ^{F^×}`; the orthonormal system is `χ_j/√n`). -/ theorem chi_orthogonal (j k : ZMod n) : ∑ m, chi j m * (starRingEnd ℂ) (chi k m) = if j = k then (n : ℂ) else 0 := by have : ∀ m, chi j m * (starRingEnd ℂ) (chi k m) = ZMod.stdAddChar (m * (j - k)) := fun m => by rw [chi_conj, chi, ← AddChar.map_add_eq_mul] congr 1; ring simp_rw [this] rw [AddChar.sum_mulShift _ (ZMod.isPrimitive_stdAddChar n), ZMod.card] simp only [sub_eq_zero] split_ifs <;> simp /-- 20:E12, 20:E1 — clause (iii): the scale-shift `m ↦ m + 1` (the residue `g^m ↦ g^{m+1}`) has every chart mode as an eigenvector, with eigenphase `e^{2πi·j/n}` independent of the vector: `χ_j(m + 1) = e^{2πi j/n} χ_j(m)`. -/ theorem chi_shift (j m : ZMod n) : chi j (m + 1) = ZMod.stdAddChar j * chi j m ∧ ZMod.stdAddChar (j : ZMod n) = Complex.exp (2 * Real.pi * I * j.val / n) := by constructor · rw [chi, chi, mul_add, mul_one, AddChar.map_add_eq_mul, mul_comm] · rw [ZMod.stdAddChar_apply, ZMod.toCircle_apply] /-- 20:E12, 20:E13 — clause (i): Fourier inversion on the cycle, `v = (1/n) Σ_j ⟨v, χ_j⟩ χ_j`, with the constant mode carrying the mean, `⟨v, χ_0⟩ = Σ_m v(m)`, so the nontrivial modes carry `v − v̄·1`. -/ theorem chi_inversion (v : ZMod n → ℂ) : (∀ m, v m = (n : ℂ)⁻¹ * ∑ j, coef v j * chi j m) ∧ coef v 0 = ∑ m, v m ∧ ∀ m, v m - (n : ℂ)⁻¹ * ∑ m', v m' = (n : ℂ)⁻¹ * ∑ j ∈ univ.erase 0, coef v j * chi j m := by have hn : (n : ℂ) ≠ 0 := by exact_mod_cast NeZero.ne n have hkey : ∀ m, ∑ j, coef v j * chi j m = (n : ℂ) * v m := by intro m simp only [coef, sum_mul] rw [sum_comm] have : ∀ m', ∑ j, v m' * (starRingEnd ℂ) (chi j m') * chi j m = v m' * ∑ j, chi j m * (starRingEnd ℂ) (chi j m') := fun m' => by rw [mul_sum]; exact sum_congr rfl fun j _ => by ring simp_rw [this] have horth : ∀ m', ∑ j, chi j m * (starRingEnd ℂ) (chi j m') = if m' = m then (n : ℂ) else 0 := by intro m' have : ∀ j, chi j m * (starRingEnd ℂ) (chi j m') = ZMod.stdAddChar (j * (m - m')) := fun j => by rw [chi_conj, chi, ← AddChar.map_add_eq_mul] congr 1; ring simp_rw [this] rw [AddChar.sum_mulShift _ (ZMod.isPrimitive_stdAddChar n), ZMod.card] by_cases h : m' = m · subst h; simp · rw [ite_eq_right (fun e => h (sub_eq_zero.1 e).symm), ite_eq_right h]; simp simp_rw [horth] simp [mul_comm] have hmean : coef v 0 = ∑ m, v m := by simp only [coef, chi, zero_mul, AddChar.map_zero_eq_one, map_one, mul_one] refine ⟨fun m => ?_, hmean, fun m => ?_⟩ · rw [hkey, ← mul_assoc, inv_mul_cancel₀ hn, one_mul] · have hsplit := sum_erase_add univ (fun j => coef v j * chi j m) (mem_univ 0) rw [hkey] at hsplit have h0 : coef v 0 * chi 0 m = ∑ m', v m' := by rw [hmean, chi, zero_mul, AddChar.map_zero_eq_one, mul_one] rw [h0] at hsplit have : ∑ j ∈ univ.erase 0, coef v j * chi j m = (n : ℂ) * v m - ∑ m', v m' := by linear_combination hsplit rw [this, mul_sub, ← mul_assoc, inv_mul_cancel₀ hn, one_mul] /-- 20:E13, 20:C5 — Parseval on the cycle: `Σ_j |⟨v, χ_j⟩|² = n Σ_m |v(m)|²`; the chart modes are complete. -/ theorem chi_parseval (v : ZMod n → ℂ) : ∑ j, normSq (coef v j) = n * ∑ m, normSq (v m) := by have h := (chi_inversion v).1 apply Complex.ofReal_injective push_cast simp_rw [← Complex.mul_conj] have hc : ∀ j, (starRingEnd ℂ) (coef v j) = ∑ m, (starRingEnd ℂ) (v m) * chi j m := fun j => by simp only [coef, map_sum, map_mul, Complex.conj_conj] calc ∑ j, coef v j * (starRingEnd ℂ) (coef v j) = ∑ j, ∑ m, (starRingEnd ℂ) (v m) * (coef v j * chi j m) := by refine sum_congr rfl fun j _ => ?_ rw [hc, mul_sum]; exact sum_congr rfl fun m _ => by ring _ = ∑ m, (starRingEnd ℂ) (v m) * ∑ j, coef v j * chi j m := by rw [sum_comm]; exact sum_congr rfl fun m _ => by rw [mul_sum] _ = ∑ m, (starRingEnd ℂ) (v m) * ((n : ℂ) * v m) := by refine sum_congr rfl fun m _ => ?_ congr 1 have hn : (n : ℂ) ≠ 0 := by exact_mod_cast NeZero.ne n have := h m rw [this, ← mul_assoc, mul_inv_cancel₀ hn, one_mul] _ = (n : ℂ) * ∑ m, v m * (starRingEnd ℂ) (v m) := by rw [mul_sum]; exact sum_congr rfl fun m _ => by ring /-- 20:C5 — mean-square flatness: for a mean-removed vector `u ≠ 0` on the cycle (`Σ_m u(m) = 0`), the normalised correlations `r_j = |⟨u, χ_j⟩|/(‖u‖ ‖χ_j‖)` with the nonconstant modes satisfy `Σ_{j≠0} r_j² = 1` exactly, so their mean square over the `n − 1 = p − 2` nonconstant modes is `1/(p − 2)`: the root-mean-square correlation is `1/√(p − 2)`. -/ theorem flatness (u : ZMod n → ℂ) (hmean : ∑ m, u m = 0) (hu : u ≠ 0) : ∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m)) = 1 ∧ (∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m))) / ((n : ℝ) - 1) = 1 / ((n : ℝ) - 1) := by have hpos : 0 < ∑ m, normSq (u m) := by obtain ⟨m, hm⟩ : ∃ m, u m ≠ 0 := by by_contra h; push Not at h; exact hu (funext h) exact sum_pos' (fun m _ => normSq_nonneg _) ⟨m, mem_univ _, normSq_pos.2 hm⟩ have hn : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n) have hden : (n : ℝ) * ∑ m, normSq (u m) ≠ 0 := (mul_pos hn hpos).ne' have h0 : coef u 0 = 0 := by rw [(chi_inversion u).2.1, hmean] have hsplit := sum_erase_add univ (fun j => normSq (coef u j)) (mem_univ 0) rw [chi_parseval, h0, normSq_zero, add_zero] at hsplit have h1 : ∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m)) = 1 := by rw [← sum_div, hsplit, div_self hden] exact ⟨h1, by rw [h1]⟩ end characters section eigen /-- 20:E12, 20:E1 — the multiplicative characters of the shell are eigenvectors of the scale-shift in the abstract reading: `χ(g^r x) = χ(g)^r χ(x)` for every `χ : F^× →* ℂ^×`. -/ theorem character_eigen {F : Type*} [Field F] (χ : Fˣ →* ℂˣ) (g x : Fˣ) (r : ℕ) : χ (g ^ r * x) = χ g ^ r * χ x := by rw [map_mul, map_pow] end eigen /-! ## The resonance: the von Mangoldt weight (row C2) -/ section resonance open ArithmeticFunction Finset /-- 20:C2 — `Λ = μ ∗ log` exactly on the divisor lattice: `Λ(n) = Σ_{d ∣ n} μ(d) log(n/d)`; and the support of `Λ` is the prime powers. (Hardy's limit `R_L → (φ(n)/n) Λ(n)` is the import A3.) -/ theorem vonMangoldt_moebius (m : ℕ) : vonMangoldt m = ∑ d ∈ m.divisors, (moebius d : ℝ) * Real.log ((m : ℝ) / d) ∧ (vonMangoldt m ≠ 0 ↔ IsPrimePow m) := by refine ⟨?_, vonMangoldt_ne_zero_iff⟩ rw [← moebius_mul_log_eq_vonMangoldt, mul_apply, Nat.sum_divisorsAntidiagonal (fun a b => (moebius : ArithmeticFunction ℝ) a * ArithmeticFunction.log b)] refine sum_congr rfl fun d hd => ?_ simp only [intCoe_apply, log_apply] rw [Nat.cast_div (Nat.dvd_of_mem_divisors hd) (by exact_mod_cast (Nat.pos_of_mem_divisors hd).ne')] end resonance /-! ## The strip (20:D8): the Euler product excludes zeros with real part at least one, and the functional equation confines the nontrivial zeros to the open strip, in orbits of the Klein four-group `s ↦ 1 − s`, `s ↦ s̄` (13 October 2026). -/ section strip open ComplexConjugate /-- A zero of `ζ` with real part at most zero is a trivial zero `−2(n+1)`: at `s' = 1 − s` the functional equation reads `ζ s = 2 (2π)^{−s'} Γ(s') cos(π s'/2) ζ(s')` with `Re s' ≥ 1`, where `ζ(s') ≠ 0` (the Euler product), so `cos(π s'/2) = 0`, `s'` an odd integer and `s` an even integer `≤ 0`; `s = 0` is excluded by `ζ 0 = −1/2`. -/ theorem zero_re_nonpos_trivial {s : ℂ} (h0 : riemannZeta s = 0) (hre : s.re ≤ 0) : ∃ n : ℕ, s = -2 * (n + 1) := by have hs0 : s ≠ 0 := fun h => by rw [h, riemannZeta_zero] at h0; norm_num at h0 set s' := 1 - s with hs' have hre' : 1 ≤ s'.re := by simp only [hs', Complex.sub_re, Complex.one_re]; linarith have hne : ∀ n : ℕ, s' ≠ -n := fun n h => by have := congrArg Complex.re h simp only [Complex.neg_re, Complex.natCast_re] at this have : (0 : ℝ) ≤ n := Nat.cast_nonneg n linarith have hne1 : s' ≠ 1 := fun h => hs0 (by rw [hs'] at h; linear_combination -h) have hfe := riemannZeta_one_sub hne hne1 have h1s : 1 - s' = s := by rw [hs']; ring rw [h1s, h0] at hfe have hz : riemannZeta s' ≠ 0 := riemannZeta_ne_zero_of_one_le_re hre' have hΓ : Complex.Gamma s' ≠ 0 := Complex.Gamma_ne_zero_of_re_pos (by linarith) have hpow : (2 * (Real.pi : ℂ)) ^ (-s') ≠ 0 := by rw [Complex.cpow_ne_zero_iff]; left exact mul_ne_zero two_ne_zero (Complex.ofReal_ne_zero.2 Real.pi_ne_zero) have hcos : Complex.cos ((Real.pi : ℂ) * s' / 2) = 0 := by have h := hfe.symm simp only [mul_eq_zero, two_ne_zero, false_or, hpow, hΓ, hz, or_false] at h exact h obtain ⟨k, hk⟩ := Complex.cos_eq_zero_iff.1 hcos have hπ : (Real.pi : ℂ) ≠ 0 := Complex.ofReal_ne_zero.2 Real.pi_ne_zero have hs'k : s' = 2 * k + 1 := by have : (Real.pi : ℂ) * s' = (Real.pi : ℂ) * (2 * k + 1) := by linear_combination 2 * hk exact mul_left_cancel₀ hπ this have hsk : s = -2 * k := by rw [← h1s, hs'k]; ring have hk0 : 0 ≤ k := by have := congrArg Complex.re hsk simp only [neg_mul, Complex.neg_re, Complex.mul_re, Complex.re_ofNat, Complex.im_ofNat, Complex.intCast_re, Complex.intCast_im, mul_zero, sub_zero] at this have : (0 : ℝ) ≤ k := by linarith exact_mod_cast this have hk1 : k ≠ 0 := fun h => hs0 (by rw [hsk, h]; simp) refine ⟨(k - 1).toNat, ?_⟩ have hk1' : 1 ≤ k := by omega have : ((k - 1).toNat : ℤ) = k - 1 := Int.toNat_of_nonneg (by omega) rw [hsk] have hcast : ((((k - 1).toNat : ℕ) : ℂ)) = (k : ℂ) - 1 := by rw [← Int.cast_natCast, this]; push_cast; ring rw [hcast]; ring /-- 20:D8, the strip: a nontrivial zero of `ζ` lies in the open strip `0 < Re s < 1`, and its Klein-four orbit under `s ↦ 1 − s` and `s ↦ s̄` consists of zeros: `Re s < 1` by the Euler product (`riemannZeta_ne_zero_of_one_le_re`), `0 < Re s` by the functional equation with the Euler product on the reflected side, `ζ(1 − s) = 0` by the functional equation (`riemannZeta_one_sub`) and `ζ(s̄) = 0` by `riemannZeta_conj`. -/ theorem zeros_in_strip {s : ℂ} (h0 : riemannZeta s = 0) (htriv : ¬∃ n : ℕ, s = -2 * (n + 1)) (h1 : s ≠ 1) : 0 < s.re ∧ s.re < 1 ∧ riemannZeta (1 - s) = 0 ∧ riemannZeta (conj s) = 0 := by have hlt : s.re < 1 := by by_contra h exact riemannZeta_ne_zero_of_one_le_re (not_lt.1 h) h0 have hpos : 0 < s.re := by by_contra h exact htriv (zero_re_nonpos_trivial h0 (not_lt.1 h)) refine ⟨hpos, hlt, ?_, ?_⟩ · have hne : ∀ n : ℕ, s ≠ -n := fun n h => by have := congrArg Complex.re h simp only [Complex.neg_re, Complex.natCast_re] at this have : (0 : ℝ) ≤ n := Nat.cast_nonneg n linarith rw [riemannZeta_one_sub hne h1, h0, mul_zero] · rw [riemannZeta_conj, h0, map_zero] end strip /-! ## Turing's count (20:F1; 15 October 2026): the completed zeta is real on the line, and a sign change of it between two heights is a zero of `ζ` on the line between them — the analytic half of the certificate, whose finite half is `FRC.Horizon.turing_chain`, `turing_equal`, `turing_phantom`. -/ section turing open ComplexConjugate theorem line_ne_zero (t : ℝ) : (1 / 2 + t * Complex.I : ℂ) ≠ 0 := by intro h have := congrArg Complex.re h simp at this theorem line_ne_one (t : ℝ) : (1 / 2 + t * Complex.I : ℂ) ≠ 1 := by intro h have := congrArg Complex.re h norm_num at this /-- The factor `π^{−w/2} Γ(w/2)` does not vanish for `Re w > 0`. -/ theorem scale_ne_zero {w : ℂ} (hw : 0 < w.re) : ((Real.pi : ℂ) ^ (-w / 2) * Complex.Gamma (w / 2)) ≠ 0 := by refine mul_ne_zero ?_ ?_ · exact Complex.cpow_ne_zero_iff.mpr (Or.inl (by exact_mod_cast Real.pi_ne_zero)) · exact Complex.Gamma_ne_zero_of_re_pos (by simp; linarith) /-- 20:F1 — `Λ(w) = ζ(w) π^{−w/2} Γ(w/2)` for `Re w > 0` (Mathlib's `riemannZeta_eq_completedRiemannZeta₀` with `completedRiemannZeta_eq`). -/ theorem completed_eq_mul {w : ℂ} (hw : 0 < w.re) : completedRiemannZeta w = riemannZeta w * ((Real.pi : ℂ) ^ (-w / 2) * Complex.Gamma (w / 2)) := by have hw0 : w ≠ 0 := fun h => by simp [h] at hw rw [riemannZeta_eq_completedRiemannZeta₀ hw0, ← completedRiemannZeta_eq, div_mul_cancel₀ _ (scale_ne_zero hw)] /-- 20:F1 — `Λ(s̄) = conj Λ(s)` for `Re s > 0`: `ζ`, `Γ` and the real power commute with conjugation. -/ theorem completed_conj {s : ℂ} (hs : 0 < s.re) : completedRiemannZeta (conj s) = conj (completedRiemannZeta s) := by have hs' : 0 < (conj s).re := by simpa using hs rw [completed_eq_mul hs', completed_eq_mul hs, map_mul, map_mul, riemannZeta_conj, ← Complex.Gamma_conj] congr 2 · have h1 : (-(conj s) / 2 : ℂ) = conj (-s / 2) := by rw [map_div₀, map_neg, map_ofNat] have hπ : (Real.pi : ℂ).arg ≠ Real.pi := by rw [Complex.arg_ofReal_of_nonneg Real.pi_pos.le]; exact Real.pi_ne_zero.symm rw [h1, Complex.cpow_conj _ _ hπ, Complex.conj_ofReal] · congr 1; rw [map_div₀, map_ofNat] /-- 20:F1 — the completed zeta is real on the line: `1 − s = s̄` there, so `Λ(s) = Λ(1 − s) = Λ(s̄) = conj Λ(s)`. -/ theorem completed_im_line (t : ℝ) : (completedRiemannZeta (1 / 2 + t * Complex.I)).im = 0 := by set s : ℂ := 1 / 2 + t * Complex.I with hs have hre : 0 < s.re := by simp [hs] have h1 : conj s = 1 - s := by apply Complex.ext <;> simp [hs]; norm_num have h2 : conj (completedRiemannZeta s) = completedRiemannZeta s := by rw [← completed_conj hre, h1, completedRiemannZeta_one_sub] exact Complex.conj_eq_iff_im.mp h2 /-- The real part of the completed zeta along the line is continuous in the height. -/ theorem continuous_line_re : Continuous (fun t : ℝ => (completedRiemannZeta (1 / 2 + t * Complex.I)).re) := by have hline : Continuous (fun t : ℝ => (1 / 2 + t * Complex.I : ℂ)) := by fun_prop refine Complex.continuous_re.comp (continuous_iff_continuousAt.mpr fun t => ?_) exact ContinuousAt.comp (f := fun t : ℝ => (1 / 2 + t * Complex.I : ℂ)) (g := completedRiemannZeta) (differentiableAt_completedZeta (line_ne_zero t) (line_ne_one t)).continuousAt hline.continuousAt /-- 20:F1 — Turing's count, the analytic clause: a sign change of `Re Λ(1/2 + it)` between the heights `a < b` is a zero of `ζ` on the line strictly between them (the intermediate value theorem on the real function `completed_im_line`, divided by the non-vanishing factor `scale_ne_zero`). Each certified sign change of the package's main sum is such a zero; the finite count is `FRC.Horizon.turing_chain`. -/ theorem zero_of_sign_change {a b : ℝ} (hab : a < b) (h : (completedRiemannZeta (1 / 2 + a * Complex.I)).re * (completedRiemannZeta (1 / 2 + b * Complex.I)).re < 0) : ∃ t : ℝ, a < t ∧ t < b ∧ riemannZeta (1 / 2 + t * Complex.I) = 0 := by set f : ℝ → ℝ := fun t => (completedRiemannZeta (1 / 2 + t * Complex.I)).re with hf have hc : ContinuousOn f (Set.Icc a b) := continuous_line_re.continuousOn have key : ∀ t : ℝ, f t = 0 → riemannZeta (1 / 2 + t * Complex.I) = 0 := by intro t ht have hre : 0 < (1 / 2 + t * Complex.I : ℂ).re := by simp have hΛ : completedRiemannZeta (1 / 2 + t * Complex.I) = 0 := Complex.ext (by simpa [hf] using ht) (by simpa using completed_im_line t) have := completed_eq_mul hre rw [hΛ] at this exact (mul_eq_zero.mp this.symm).resolve_right (scale_ne_zero hre) rcases mul_neg_iff.mp h with ⟨ha, hb⟩ | ⟨ha, hb⟩ · obtain ⟨t, ⟨hta, htb⟩, hft⟩ := intermediate_value_Ioo' hab.le hc ⟨hb, ha⟩ exact ⟨t, hta, htb, key t hft⟩ · obtain ⟨t, ⟨hta, htb⟩, hft⟩ := intermediate_value_Ioo hab.le hc ⟨ha, hb⟩ exact ⟨t, hta, htb, key t hft⟩ end turing end FRC.Chart /-! inlined: FrcLedger/Theme/Gravity.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Gravity — the gravity theme on Mathlib: the exact faces of 21-gravity (10 October 2026) The exact Mathlib variants of 21-gravity's rows, moved from the paper module `FrcLedger/Gravity.lean` (which keeps every old name as an alias): the Carrier register on a field with `4S + 1 = 0` — the calibration congruence, the register value `G = 2S`, the action quantum as the quarter-turn pair (21:A1, C2, C5, C16); the count face of the area law and the merger law on `ℤ` (21:C13); the cover forcing and the PPN triangle over `ℚ` (21:A9, C7, C8, C25); the mass–energy channel as a gcd (21:A9); the central difference's anti-self-adjointness and the finite Fourier shift theorem on `ZMod N` (21:C9, C20). No reals here (gate G09): the chart readings are `Theme/Strong.lean`'s. The core proves the same faces with no axioms (`FrcCore/Theme/Gravity.lean`, `Theme/Drift.lean`, `Theme/Lattice.lean`, `Theme/Shift.lean`); these are their Mathlib counterparts on the classical hierarchy. -/ namespace FRC.GravML /-! ## The Carrier register (21:A1, C2, C5, C16) -/ section register variable {K : Type*} [Field K] /-- 21:C16, 21:A1 — the calibration congruence: on the Carrier chart `4S + 1 = 0` the full cycle `2π ↦ 4S` is `−1` and `(4S)² = 1`, one residue relation. -/ theorem calibration_congruence (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) : ((4 * S : ℕ) : K) = -1 ∧ ((4 * S : ℕ) : K) ^ 2 = 1 := by push_cast at hΩ ⊢ exact ⟨by linear_combination hΩ, by linear_combination (4 * (S : K) - 1) * hΩ⟩ /-- 21:C2, 21:C5, 21:C16 — the register value of the Newton constant, `G = 2S`, on the Carrier chart `4S + 1 = 0`: `2G = −1` (the half-cycle); `(−2) G = 1`, the face convention `4π ↦ −2` with `G = (−2)⁻¹`; the Gauss count `(2 · 4S) G = 1`; `c² = 2⁻¹ = 2S + 1` and `G = −c²` (the chart ratio `4π/2π = 2` is read as `(−2)/(−1)`). The uniqueness of the linear solution is `Dimensions.G_unique`. -/ theorem newton_register (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) : 2 * ((2 * S : ℕ) : K) = -1 ∧ (-2) * ((2 * S : ℕ) : K) = 1 ∧ (2 * ((4 * S : ℕ) : K)) * ((2 * S : ℕ) : K) = 1 ∧ 2 * ((2 * S + 1 : ℕ) : K) = 1 ∧ ((2 * S + 1 : ℕ) : K) = 2⁻¹ ∧ ((2 * S : ℕ) : K) = -((2 * S + 1 : ℕ) : K) := by push_cast at hΩ ⊢ refine ⟨by linear_combination hΩ, by linear_combination -hΩ, by linear_combination (4 * (S : K) - 1) * hΩ, by linear_combination hΩ, ?_, by linear_combination hΩ⟩ exact eq_inv_of_mul_eq_one_left (by linear_combination hΩ) /-- On the Carrier `𝔽_Ω`, `Ω = 4S + 1` prime, `2 ≠ 0` (`Ω` is odd). -/ theorem carrier_two_ne_zero (S : ℕ) [hp : Fact (Nat.Prime (4 * S + 1))] : (2 : ZMod (4 * S + 1)) ≠ 0 := by rw [show (2 : ZMod (4 * S + 1)) = ((2 : ℕ) : ZMod (4 * S + 1)) by norm_cast, Ne, ZMod.natCast_eq_zero_iff] intro hd have h1 : 4 * S + 1 ≤ 2 := Nat.le_of_dvd (by norm_num) hd have h2 : 2 ≤ 4 * S + 1 := hp.out.two_le omega /-- In any field with `4S + 1 = 0` and `2 ≠ 0`, a quarter-turn `i² = −1` gives a square root of `S`, `r = i/2`, with `(2r)² = −1`. -/ theorem hbar_of_quarter_turn {K : Type*} [Field K] (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) (h2 : (2 : K) ≠ 0) (i : K) (hi : i ^ 2 = -1) : ∃ r : K, r ^ 2 = (S : K) ∧ (2 * r) ^ 2 = -1 := by push_cast at hΩ have h4 : (2⁻¹ : K) ^ 2 * 4 = 1 := by field_simp; norm_num refine ⟨i * 2⁻¹, ?_, ?_⟩ · calc (i * 2⁻¹) ^ 2 = i ^ 2 * (2⁻¹) ^ 2 := by ring _ = -1 * (2⁻¹) ^ 2 := by rw [hi] _ = (S : K) := by linear_combination (-(2⁻¹ : K) ^ 2) * hΩ + (S : K) * h4 · have : 2 * (i * 2⁻¹) = i := by field_simp rw [this, hi] /-- 21:C5, 21:C16, 21:A1 — the action quantum as the quarter-turn pair: on every Carrier `Ω = 4S + 1` prime, `S` is a square (`S = (i/2)²` with `i² = −1`, since `4S = −1`), so `ħ = 2√S` has `ħ² = 4S = −1` — `ħ` is one of the quarter-turn pair `±i`. -/ theorem hbar_register (S : ℕ) [Fact (Nat.Prime (4 * S + 1))] : ∃ r : ZMod (4 * S + 1), r ^ 2 = (S : ZMod (4 * S + 1)) ∧ (2 * r) ^ 2 = -1 := by obtain ⟨i, hi⟩ : IsSquare (-1 : ZMod (4 * S + 1)) := ZMod.exists_sq_eq_neg_one_iff.mpr (by omega) exact hbar_of_quarter_turn S (ZMod.natCast_self _) (carrier_two_ne_zero S) i (by rw [sq]; exact hi.symm) end register /-! ## The count face and the cover forcing (21:A9, C7, C8, C13, C25) -/ section count /-- 21:C13 — the count face of the area law on a symmetry-complete shell `p = 4κ + 1`: with `S = (p² − 1)/4`, i.e. `4S + 1 = p²` for `S = κ(4κ + 2)`, and the coordinate area `A = p(p + 1)`, the ratio `S/A = κ/p` holds exactly (`Sp = κA`) and `S = (A/4)(1 − 1/p)` (`4Sp = A(p − 1)`) — the Bekenstein quarter as the `Q₄` quotient. -/ theorem count_face (κ : ℕ) : 4 * (κ * (4 * κ + 2)) + 1 = (4 * κ + 1) ^ 2 ∧ (κ * (4 * κ + 2)) * (4 * κ + 1) = κ * ((4 * κ + 1) * (4 * κ + 2)) ∧ 4 * (κ * (4 * κ + 2)) * (4 * κ + 1) = ((4 * κ + 1) * (4 * κ + 2)) * (4 * κ) := ⟨by ring, by ring, by ring⟩ /-- 21:C13 — the merger area law on the count face, `A = M(M + 1)`: `ΔA = 2M₁M₂` exactly under additive mass, the paper's instance `27 811 + 1 596 → 29 407` giving `ΔA = 88 772 712`; with a radiated `δ` the count gives `ΔA = 2M₁M₂ − (2(M₁ + M₂) + 1)δ + δ²`, at most the additive value for `0 ≤ δ ≤ 2(M₁ + M₂) + 1` — the area statement an inequality (the coefficient `−2(M₁ + M₂)δ` is the `A = M²` form; on the count face the linear term carries the extra `−δ`). -/ theorem merger_area_law (M₁ M₂ δ : ℤ) : (M₁ + M₂) * (M₁ + M₂ + 1) - M₁ * (M₁ + 1) - M₂ * (M₂ + 1) = 2 * M₁ * M₂ ∧ (M₁ + M₂ - δ) * (M₁ + M₂ - δ + 1) - M₁ * (M₁ + 1) - M₂ * (M₂ + 1) = 2 * M₁ * M₂ - (2 * (M₁ + M₂) + 1) * δ + δ ^ 2 ∧ (0 ≤ δ → δ ≤ 2 * (M₁ + M₂) + 1 → (M₁ + M₂ - δ) * (M₁ + M₂ - δ + 1) - M₁ * (M₁ + 1) - M₂ * (M₂ + 1) ≤ 2 * M₁ * M₂) ∧ (27811 + 1596) * (27811 + 1596 + 1) - 27811 * (27811 + 1) - 1596 * (1596 + 1) = (88772712 : ℤ) := by refine ⟨by ring, by ring, ?_, by norm_num⟩ intro h0 h1 nlinarith [mul_nonneg h0 (sub_nonneg.mpr h1)] /-- 21:A9, 21:C25, 21:C7, 21:C8 — the cover forcing: the apsidal coefficient `2 − β + 2γ` against the PPN-free deficit `3/2` equals the two-face ratio `2` exactly when `2γ − β = 1`, with deviation `(2/3)(2γ − β − 1)`; channel unity `γ = 1` makes the deflection factor `(1 + γ)/2` equal to `1` (the full `4Gm/c²b`) and, together with the forcing, gives `β = 1`, the perihelion factor `(2 + 2γ − β)/3` then `1`. -/ theorem cover_forcing (β γ : ℚ) : ((2 - β + 2 * γ) / (3 / 2) = 2 ↔ 2 * γ - β = 1) ∧ (2 - β + 2 * γ) / (3 / 2) - 2 = 2 / 3 * (2 * γ - β - 1) ∧ (γ = 1 → (1 + γ) / 2 = 1 ∧ (2 * γ - β = 1 → β = 1 ∧ (2 + 2 * γ - β) / 3 = 1)) := by refine ⟨?_, by ring, ?_⟩ · constructor <;> intro h <;> linarith · rintro rfl exact ⟨by norm_num, fun h => ⟨by linarith, by linarith⟩⟩ /-- 38:C8 — the face-ratio identity of the parametrised post-Newtonian family (Statement *The physical floors*, 38-s13): with the apsidal coefficient `2 − β + 2γ` and the `β, γ`-free clock-deficit coefficient `3/2`, the face ratio is `(2/3)(2 + 2γ − β)`, equal to `2` exactly when `2γ − β = 1`, with deviation `(2/3)(2γ − β − 1)`; the exponential metric `β = γ = 1` satisfies it; in Brans–Dicke theory (`β = 1`, `γ = (1 + ω)/(2 + ω)`) the combination is `2γ − β − 1 = −2/(2 + ω)`, nonzero at every finite coupling, deviation `−4/(3(2 + ω))`, and below every `ε` past `ω = 2/ε` (the general-relativistic limit, stated over `ℚ`). The coefficients themselves are the continuum chart's (the series of the isotropic metric, `o1_gr_chart.py`); the algebra is exact over `ℚ`. -/ theorem ppn_faces (β γ : ℚ) : (2 - β + 2 * γ) / (3 / 2) = 2 / 3 * (2 + 2 * γ - β) ∧ (2 / 3 * (2 + 2 * γ - β) = 2 ↔ 2 * γ - β = 1) ∧ 2 / 3 * (2 + 2 * γ - β) - 2 = 2 / 3 * (2 * γ - β - 1) ∧ (2 * (1 : ℚ) - 1 = 1) ∧ (∀ ω : ℚ, 2 + ω ≠ 0 → 2 * ((1 + ω) / (2 + ω)) - 1 - 1 = -2 / (2 + ω) ∧ 2 / 3 * (2 * ((1 + ω) / (2 + ω)) - 1 - 1) = -4 / (3 * (2 + ω)) ∧ -2 / (2 + ω) ≠ 0) ∧ (∀ ε : ℚ, 0 < ε → ∃ W : ℚ, ∀ ω : ℚ, W < ω → |(-2 : ℚ) / (2 + ω)| < ε) := by refine ⟨by ring, ⟨fun h => by linarith, fun h => by linarith⟩, by ring, by norm_num, fun ω hω => ⟨?_, ?_, ?_⟩, ?_⟩ · field_simp; ring · field_simp; ring · exact div_ne_zero (by norm_num) hω · intro ε hε refine ⟨2 / ε, fun ω hω => ?_⟩ have h2 : 0 < 2 / ε := by positivity have hpos : 0 < 2 + ω := by linarith rw [abs_div, abs_neg, abs_of_pos hpos, abs_of_pos (by norm_num : (0 : ℚ) < 2), div_lt_iff₀ hpos] have : 2 / ε < ω := hω rw [div_lt_iff₀ hε] at this linarith /-- 38:C12, 38:C7 — the registration dictionary on a hosted pair: matching the temporal face `κ/(2S)` to the circular-orbit clock deficit `(3/2) r_g/p_sl` forces `p_sl = 3 (S/κ) r_g`, under which the angular face reads `3 r_g/p_sl = κ/S` automatically: one relation, homogeneous of degree `0`, fixing the ratio `p_sl/r_g = 3S/κ` — `58` at `(13, 233)` (`κ = 3`, `S = 58`: `p_sl = S r_g`), `174` at `(5, 233)`; the two faces `κ/S : κ/(2S) = 2`. -/ theorem registration_dictionary (κ S rg psl : ℚ) (hκ : κ ≠ 0) (hS : S ≠ 0) (hrg : rg ≠ 0) (hpsl : psl ≠ 0) : ((3 / 2) * (rg / psl) = κ / (2 * S) ↔ psl = 3 * (S / κ) * rg) ∧ (psl = 3 * (S / κ) * rg → 3 * rg / psl = κ / S ∧ psl / rg = 3 * S / κ) ∧ (κ / S) / (κ / (2 * S)) = 2 ∧ 3 * (58 : ℚ) / 3 = 58 ∧ 3 * (58 : ℚ) / 1 = 174 := by refine ⟨⟨fun h => ?_, fun h => ?_⟩, fun h => ⟨?_, ?_⟩, ?_, by norm_num, by norm_num⟩ · field_simp at h ⊢; linarith · subst h; field_simp · subst h; field_simp · subst h; field_simp · field_simp /-- 21:A9 — the mass–energy channel `C_{p−1} ∩ C_{2(p+1)} = Q₄`: on every shell `p ≡ 1 (mod 4)`, `gcd(p − 1, 2(p + 1)) = 4`; the subgroup reading — in the cyclic unit group of `𝔽_{p²}` (order `(p − 1)(p + 1)`) the subgroups of orders `p − 1` and `2(p + 1)` meet in the subgroup of order `gcd` — is not formalised here. -/ theorem channel_q4 (p : ℕ) (hp : p % 4 = 1) : Nat.gcd (p - 1) (2 * (p + 1)) = 4 := by obtain ⟨κ, rfl⟩ : ∃ κ, p = 4 * κ + 1 := ⟨p / 4, by omega⟩ have h1 : 4 * κ + 1 - 1 = 4 * κ := by omega have h2 : 2 * (4 * κ + 1 + 1) = 4 * (1 + 2 * κ) := by ring rw [h1, h2, Nat.gcd_mul_left, Nat.gcd_add_mul_right_right, Nat.gcd_one_right] end count /-! ## The lattice on `ZMod N` (21:C9, C20) -/ section lattice variable {N : ℕ} [NeZero N] {R : Type*} [CommRing R] /-- 21:C9 — anti-self-adjointness of the central difference on the cycle `ℤ/N`: with `(Δf)(x) = f(x + 1) − f(x − 1)`, `Σ_x f(x)(Δg)(x) = −Σ_x (Δf)(x) g(x)` — `Δᵀ = −Δ`, the identity that carries the discrete Fierz–Pauli gauge invariance (the package proves the four-term functional's invariance as an exact integer identity; the paper's `½` in `D_μ = (T_μ − T_μ⁻¹)/2` scales both sides alike). The one-sided difference `(δf)(x) = f(x + 1) − f(x)` has adjoint the negative *backward* difference, `Σ_x f(x)(δg)(x) = −Σ_x (f(x) − f(x − 1)) g(x)` — the package's failing control is that this is not `−δ`. -/ theorem central_difference_adjoint (f g : ZMod N → R) : ∑ x, f x * (g (x + 1) - g (x - 1)) = -∑ x, (f (x + 1) - f (x - 1)) * g x ∧ ∑ x, f x * (g (x + 1) - g x) = -∑ x, (f x - f (x - 1)) * g x := by have h1 : ∑ x, f x * g (x + 1) = ∑ x, f (x - 1) * g x := by rw [← Equiv.sum_comp (Equiv.addRight (1 : ZMod N)) (fun x => f (x - 1) * g x)] simp have h2 : ∑ x, f x * g (x - 1) = ∑ x, f (x + 1) * g x := by rw [← Equiv.sum_comp (Equiv.subRight (1 : ZMod N)) (fun x => f (x + 1) * g x)] simp constructor · simp only [mul_sub, sub_mul, Finset.sum_sub_distrib, h1, h2]; ring · simp only [mul_sub, sub_mul, Finset.sum_sub_distrib, h1]; ring /-- The finite Fourier transform on the cycle, against a character `ζ` with `ζ^N = 1`: `(F f)(k) = Σ_x f(x) ζ^{xk}`. -/ def dft (ζ : R) (f : ZMod N → R) (k : ZMod N) : R := ∑ x, f x * ζ ^ (x.val * k.val) omit [NeZero N] in /-- A root of unity is insensitive to the reduction of its exponent modulo `N`. -/ theorem pow_val_mod (ζ : R) (hζ : ζ ^ N = 1) (m k : ℕ) : ζ ^ ((m % N) * k) = ζ ^ (m * k) := by conv_rhs => rw [← Nat.mod_add_div m N] rw [add_mul, pow_add, mul_assoc, pow_mul, pow_mul, hζ, one_pow, mul_one] omit [NeZero N] in /-- A root of unity is insensitive to the reduction of a factor of its exponent modulo `N`. -/ theorem pow_mul_val_mod (ζ : R) (hζ : ζ ^ N = 1) (k m : ℕ) : ζ ^ (k * (m % N)) = ζ ^ (k * m) := by rw [mul_comm, pow_val_mod ζ hζ, mul_comm] /-- 21:C20 — the finite Fourier shift theorem in both forms, the kick of the two-shift law: the kick, a character `ζ^{ax}` multiplying `f` in position, shifts the transform, `F(ζ^{a·} f)(k) = (F f)(k + a)`; dually, shifting `f` by `a` multiplies its transform by the character, `F(f(· − a))(k) = ζ^{ak} (F f)(k)`. -/ theorem shift_theorem (ζ : R) (hζ : ζ ^ N = 1) (f : ZMod N → R) (a k : ZMod N) : dft ζ (fun x => ζ ^ (a.val * x.val) * f x) k = dft ζ f (k + a) ∧ dft ζ (fun x => f (x - a)) k = ζ ^ (a.val * k.val) * dft ζ f k := by constructor · unfold dft apply Finset.sum_congr rfl intro x _ dsimp only rw [ZMod.val_add, pow_mul_val_mod ζ hζ, mul_add, pow_add, mul_comm a.val x.val] ring · unfold dft rw [Finset.mul_sum, ← Equiv.sum_comp (Equiv.addRight a)] apply Finset.sum_congr rfl intro x _ simp only [Equiv.coe_addRight, add_sub_cancel_right] rw [ZMod.val_add, pow_val_mod ζ hζ, add_mul, pow_add] ring end lattice end FRC.GravML /-! inlined: FrcLedger/Theme/Quantum.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Quantum — the quantum theme on Mathlib: the ledger's identities (22-quantum, 15 October 2026) What the core states on every shell (`FrcCore/Theme/Observation.lean`, `Interference.lean`, `Composite.lean`) is read here on the ledger itself: * the Sorkin hierarchy on every commutative ring with an additive conjugation — the ledgers `ℤ[i]` and `ℤ[ζ_d]` among them (`sorkin_hierarchy`, `sorkin_second`, 22:C8, X8, P2); * the ledger weight `z z̄ = N(z)` of a Gaussian-integer amplitude is a nonnegative rational integer, a realised tally (`pair_count_tally`, 22:C7, X1); * the Hadamard layers on the Gaussian integers: `(1 + i)^{2m} = 2^m i^m`, the norm `2^k`, and the minimal denominator — `2` does not divide `i^m (1 + i)` (`gaussian_layers`, `gaussian_norm`, `gaussian_minimal`, `tally_norm_eq`, 22:C14, P5). Exact throughout (`ℤ[i]`, commutative rings): the readings against the continuum — the Tsirelson value `2√2`, the singlet law `cos(πΔ/40)` and the channel's chart `cos(φ/2)`, `sin(φ/2)` — are the chart theme's, in `FrcLedger/Theme/Chart.lean` (section `quantum`), the one theme with the reals. -/ namespace FRC.QuantumML /-! ## The Sorkin hierarchy on the ledger -/ /-- The `k`-fold mixed difference of `f : R → R` along the directions `a 0, …, a (k−1)`. -/ def mixedDiff {R : Type*} [CommRing R] (a : ℕ → R) (f : R → R) : ℕ → R → R | 0, x => f x | k + 1, x => mixedDiff a f k (x + a k) - mixedDiff a f k x /-- The second difference of the weight `w(x) = x c(x)` with `c` additive is the cross term `b c(a) + a c(b)`. -/ theorem sorkin_second {R : Type*} [CommRing R] {c : R → R} (hc : ∀ x y, c (x + y) = c x + c y) (a : ℕ → R) (x : R) : mixedDiff a (fun x => x * c x) 2 x = a 1 * c (a 0) + a 0 * c (a 1) := by simp only [mixedDiff, hc] ring /-- 22:C8, X8, P2 — **the Sorkin hierarchy on the ledger**: on every commutative ring `R` (the ledgers `ℤ[i]` and `ℤ[ζ_d]` among them) with an additive conjugation `c`, the `k`-fold mixed difference of the weight `w(x) = x c(x)` vanishes for every `k ≥ 3` and every base point; so the interference terms `I_k` (the mixed difference at the origin) are zero exactly from the third order on. -/ theorem sorkin_hierarchy {R : Type*} [CommRing R] {c : R → R} (hc : ∀ x y, c (x + y) = c x + c y) (a : ℕ → R) : ∀ k x, mixedDiff a (fun x => x * c x) (k + 3) x = 0 | 0, x => by show mixedDiff a (fun x => x * c x) 2 (x + a 2) - mixedDiff a (fun x => x * c x) 2 x = 0 rw [sorkin_second hc, sorkin_second hc, sub_self] | k + 1, x => by show mixedDiff a (fun x => x * c x) (k + 3) (x + a (k + 3)) - mixedDiff a (fun x => x * c x) (k + 3) x = 0 rw [sorkin_hierarchy hc a k, sorkin_hierarchy hc a k, sub_self] /-- 22:C8 — `I₂` is generically nonzero: on `ℤ[i]` with the conjugation and the paths `a = b = 1`, `I₂ = 2`. -/ theorem sorkin_second_witness : mixedDiff (fun _ => (1 : GaussianInt)) (fun x => x * star x) 2 0 = 2 := by rw [sorkin_second (fun x y => star_add x y)] decide /-! ## The Hadamard layers on the Gaussian integers -/ /-- The Gaussian unit `i` and the ramified `1 + i`. -/ def gi : GaussianInt := ⟨0, 1⟩ def onePlusI : GaussianInt := ⟨1, 1⟩ theorem onePlusI_sq : onePlusI ^ 2 = 2 * gi := by decide theorem gi_norm : Zsqrtd.norm gi = 1 := by decide theorem onePlusI_norm : Zsqrtd.norm onePlusI = 2 := by decide /-- 22:C14 — `2m` balanced layers: `(1 + i)^{2m} = 2^m i^m`, and `2m + 1` layers give `2^m i^m (1 + i)`. -/ theorem gaussian_layers (m : ℕ) : onePlusI ^ (2 * m) = 2 ^ m * gi ^ m ∧ onePlusI ^ (2 * m + 1) = 2 ^ m * gi ^ m * onePlusI := by constructor · rw [pow_mul, onePlusI_sq, mul_pow] · rw [pow_succ, pow_mul, onePlusI_sq, mul_pow] theorem norm_pow (x : GaussianInt) : ∀ k : ℕ, Zsqrtd.norm (x ^ k) = (Zsqrtd.norm x) ^ k | 0 => by simp | k + 1 => by rw [pow_succ, Zsqrtd.norm_mul, norm_pow x k, pow_succ] /-- 22:C14 — the norm of `k` layers is `2^k`. -/ theorem gaussian_norm (k : ℕ) : Zsqrtd.norm (onePlusI ^ k) = 2 ^ k := by rw [norm_pow, onePlusI_norm] /-- 22:C14 — the minimal denominator: `2` does not divide `i^m (1 + i)` in `ℤ[i]` (its norm is `2`, not a multiple of `4`), so the amplitude `i^m (1 + i)/2^{m+1}` of `2m + 1` layers has the denominator `2^{m+1}` exactly, and `i^m/2^m` of `2m` layers the denominator `2^m` (`i^m` a unit). -/ theorem gaussian_minimal (m : ℕ) : ¬ (2 : GaussianInt) ∣ gi ^ m * onePlusI := by intro ⟨z, hz⟩ have h := congrArg Zsqrtd.norm hz rw [Zsqrtd.norm_mul, Zsqrtd.norm_mul, norm_pow, gi_norm, onePlusI_norm, one_pow, one_mul] at h have h2 : Zsqrtd.norm (2 : GaussianInt) = 4 := by decide rw [h2] at h omega /-- 22:C7, 22:X1 — the ledger weight is a realised tally: for a Gaussian-integer amplitude `z` the weight `z z̄` is the norm `N(z) = a² + b²`, a nonnegative rational integer (the coincidence count). -/ theorem pair_count_tally (z : GaussianInt) : z * star z = (Zsqrtd.norm z : GaussianInt) ∧ 0 ≤ Zsqrtd.norm z := ⟨(Zsqrtd.norm_eq_mul_conj z).symm, Zsqrtd.norm_nonneg (by norm_num) z⟩ /-- 22:C14, P5 — the minimal tally norm `T(k) = 2^{k + [k odd]}` is the square of the minimal denominator `2^{⌈k/2⌉}`. -/ theorem tally_norm_eq (k : ℕ) : 2 ^ (k + k % 2) = (2 ^ ((k + 1) / 2)) ^ 2 := by rw [← pow_mul] congr 1 omega end FRC.QuantumML /-! inlined: FrcLedger/Theme/Strong.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Strong — the chart theme's strong field, crossover and series (10 October 2026) The readings of 21-gravity on the reals, moved from the paper module `FrcLedger/Gravity.lean` (which keeps every old name as an alias), every numeral re-anchored to the ledger's scale import (00:A7: `ln Ω = 283.5`, `Ω = 1.3 × 10¹²³`; `Theme/Chart.lean`'s `ln_omega_ledger`). The strong field: the operational cut `e^{2M/r_f} = Ω` with the ordering `r_* < r_f < M` exactly when `M > (ln Ω/2)²` (21:C12, P7); the photon sphere at `r = 2Gm` with `b_c = 2e·Gm` as the minimum of `r e^{2Gm/r}` (21:C12, P1); the shadow `+4.6 %` and ringdown `−4.4 %` bracketed from `e` and `√3` (21:P1); the eikonal pair `Ω_c = λ = 1/(2eM)` from the derivatives of `r² e^{4M/r}` at `2M` (00:E14, 16 October 2026); the innermost stable orbit at `r = 3 + √5` and the efficiency `5.48 %` against Schwarzschild's `5.72 %` (21:P1); the capacity ratio `1/ln²Ω = 1.24 × 10⁻⁵` at `283.5` (21:C13); the redshift's linear form (21:C4). The crossover: the registration root `η` of `wη² − 2η + w = 0` in `(0, 1)`, the crossover squeezed between its deep and Newtonian limits, the Tully–Fisher algebra (21:C19, P4, X2); the discriminant `0.051` at `g_N = 5a₀` against the simple interpolant (21:P4). The primordial fixed point `n_s = 1` (21:C18; the tilt at `283.5` is `Chart.tilt_ledger`). The dispersion symbol and the locked sum on `ℂ` (21:C15, C1). The series: the exponential reading composes and the isotropic Schwarzschild factor is `e^{−2 artanh(U/2)}` (21:C11); the post-Newtonian Taylor brackets (21:C8, P6); the preferred-frame scale `1/√Ω` at `1.3 × 10¹²³` (21:P2, C10); cardinality dilution (21:X8, C5). Classical (tier 2) on Mathlib's hierarchy; every bracket from `π` to six places, `e` to nine and the Taylor tail of `exp`. The finite content is proved with no axioms in the core (`FrcCore/Theme/Drift.lean`, `Theme/Lattice.lean`); the exact Mathlib variants are `Theme/Gravity.lean`'s. -/ namespace FRC.Strong open Real /-! ## Cardinality dilution (21:X8, C5) -/ section register /-- 21:X8, 21:C5 — the weakness of gravity as cardinality dilution: with the Planck mass the locality horizon, `m_P = √Ω`, the dimensionless coupling of two masses `m` is `(m/m_P)² = m²/Ω`, small because `Ω` is large. C5's frame covariance is not formal content. -/ theorem dilution (m Ω : ℝ) (hΩ : 0 < Ω) : (m / √Ω) ^ 2 = m ^ 2 / Ω := by rw [div_pow, sq_sqrt hΩ.le] end register /-! ## The strong field (21:C4, C12, C13, P1, P7) -/ section strongfield /-- 21:C12, 21:P7 — the operational cut and the slip core in the substrate coordinate (`G = 1`, `M` in Planck masses, `L = ln Ω`): `r_f = 2M/L` carries `e^{2M/r_f} = Ω` (the round-trip delay's factor); `r_* = √M < r_f` exactly when `M > (L/2)²`, and `r_f < M` exactly when `L > 2` (master E10). -/ theorem operational_cut (M L Ω : ℝ) (hM : 0 < M) (hL : 0 < L) (hΩ : L = log Ω) (hΩ0 : 0 < Ω) : exp (2 * M / (2 * M / L)) = Ω ∧ (√M < 2 * M / L ↔ (L / 2) ^ 2 < M) ∧ (2 * M / L < M ↔ 2 < L) := by refine ⟨?_, ?_, ?_⟩ · have : 2 * M / (2 * M / L) = L := by field_simp rw [this, hΩ, exp_log hΩ0] · rw [Real.sqrt_lt' (by positivity), div_pow, lt_div_iff₀ (by positivity)] constructor <;> intro h <;> nlinarith · rw [div_lt_iff₀ hL] constructor <;> intro h <;> nlinarith /-- 21:P1 — the photon sphere (`prop:shadow`, `rem:exponential`): the impact parameter `b(r) = r e^{2Gm/r}` of the exponential metric satisfies `b(r) ≥ 2e·Gm` for every `r > 0`, with equality exactly at `r = 2Gm` (from `x + 1 ≤ eˣ`, strict off `x = 0`): the photon sphere is at `r_ph = 2Gm`, the critical impact parameter `b_c = 2e·Gm`. -/ theorem photon_sphere (Gm r : ℝ) (hG : 0 < Gm) (hr : 0 < r) : 2 * exp 1 * Gm ≤ r * exp (2 * Gm / r) ∧ (r * exp (2 * Gm / r) = 2 * exp 1 * Gm ↔ r = 2 * Gm) := by have hsplit : exp (2 * Gm / r) = exp 1 * exp (2 * Gm / r - 1) := by rw [← exp_add]; ring_nf have hx := Real.add_one_le_exp (2 * Gm / r - 1) have hkey : 2 * exp 1 * Gm = r * exp 1 * (2 * Gm / r - 1 + 1) := by field_simp; ring have hpos : 0 < r * exp 1 := by positivity constructor · rw [hsplit, hkey] calc r * exp 1 * (2 * Gm / r - 1 + 1) ≤ r * exp 1 * exp (2 * Gm / r - 1) := mul_le_mul_of_nonneg_left hx hpos.le _ = r * (exp 1 * exp (2 * Gm / r - 1)) := by ring · constructor · intro h by_contra hne have hx' : 2 * Gm / r - 1 ≠ 0 := by intro h0 apply hne have : 2 * Gm / r = 1 := by linarith rw [div_eq_one_iff_eq hr.ne'] at this linarith have hlt := Real.add_one_lt_exp hx' have : r * exp 1 * (2 * Gm / r - 1 + 1) < r * exp 1 * exp (2 * Gm / r - 1) := mul_lt_mul_of_pos_left hlt hpos rw [hsplit, ← mul_assoc] at h linarith · rintro rfl have : 2 * Gm / (2 * Gm) = 1 := by field_simp rw [this]; ring /-- `√3` to seven places. -/ theorem sqrt_three_bounds : (1.7320508 : ℝ) < √3 ∧ √3 < 1.7320509 := ⟨(Real.lt_sqrt (by norm_num)).mpr (by norm_num), (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)⟩ /-- 21:P1 — the shadow and the ringdown against general relativity, bracketed from `e` (nine places) and `√3`: the critical impact parameters `b_c = 2e·Gm` (this work) and `3√3·Gm` (Schwarzschild) have ratio `2e/(3√3)` between `1.0462` and `1.0463` (the shadow `+4.6 %`), and the eikonal ringdown frequency, `∝ 1/b_c`, ratio `3√3/(2e)` between `0.9557` and `0.9558` (`−4.4 %`); the Sgr A* excess `(4e − 6√3) θ_g` at the GRAVITY `θ_g = 5.12 µas` [data, A8] lies between `2.46` and `2.47 µas` (the `2.5 µas` of the text). -/ theorem shadow_bracket : (1.0462 : ℝ) < 2 * exp 1 / (3 * √3) ∧ 2 * exp 1 / (3 * √3) < 1.0463 ∧ (0.9557 : ℝ) < 3 * √3 / (2 * exp 1) ∧ 3 * √3 / (2 * exp 1) < 0.9558 ∧ (2.46 : ℝ) < (4 * exp 1 - 6 * √3) * 5.12 ∧ (4 * exp 1 - 6 * √3) * 5.12 < 2.47 := by have e1 := Real.exp_one_gt_d9 have e2 := Real.exp_one_lt_d9 obtain ⟨s1, s2⟩ := sqrt_three_bounds have hs : (0 : ℝ) < √3 := by positivity have he : (0 : ℝ) < exp 1 := exp_pos 1 refine ⟨?_, ?_, ?_, ?_, by nlinarith, by nlinarith⟩ · rw [lt_div_iff₀ (by positivity)]; nlinarith · rw [div_lt_iff₀ (by positivity)]; nlinarith · rw [lt_div_iff₀ (by positivity)]; nlinarith · rw [div_lt_iff₀ (by positivity)]; nlinarith /-- 00:E14 — the eikonal pair of the exponential reading (`G = 1`, `M` the mass): with `h(r) = r² e^{4M/r} = b(r)²` the square of the impact function, `h′(r) = e^{4M/r}(2r − 4M)` for `r ≠ 0`, zero exactly at `r_c = 2M` (the photon sphere of `photon_sphere`), and `h″(2M) = 2e²`; the orbital rate squared `Ω_c² = 1/h(2M) = 1/(2eM)²` and the Lyapunov rate squared `λ² = e^{−4u} h″/(2h)` at `2M` coincide, and the pair is `3√3/(2e)` of Schwarzschild's `1/(3√3 M)` (`shadow_bracket` brackets that ratio). -/ theorem eikonal_pair (M : ℝ) (hM : 0 < M) : (∀ r : ℝ, r ≠ 0 → HasDerivAt (fun r : ℝ => r ^ 2 * exp (4 * M / r)) (exp (4 * M / r) * (2 * r - 4 * M)) r) ∧ (∀ r : ℝ, exp (4 * M / r) * (2 * r - 4 * M) = 0 ↔ r = 2 * M) ∧ (∀ r : ℝ, r ≠ 0 → HasDerivAt (fun r : ℝ => exp (4 * M / r) * (2 * r - 4 * M)) (exp (4 * M / r) * (2 - 4 * M * (2 * r - 4 * M) / r ^ 2)) r) ∧ exp (4 * M / (2 * M)) * (2 - 4 * M * (2 * (2 * M) - 4 * M) / (2 * M) ^ 2) = 2 * exp 2 ∧ (2 * M) ^ 2 * exp (4 * M / (2 * M)) = (2 * exp 1 * M) ^ 2 ∧ exp (-(4 * M / (2 * M))) * (2 * exp 2) / (2 * ((2 * M) ^ 2 * exp (4 * M / (2 * M)))) = (1 / (2 * exp 1 * M)) ^ 2 ∧ (1 / (2 * exp 1 * M)) / (1 / (3 * √3 * M)) = 3 * √3 / (2 * exp 1) := by have hM0 : M ≠ 0 := hM.ne' have h42 : 4 * M / (2 * M) = 2 := by field_simp; ring have he2 : exp 2 = exp 1 ^ 2 := by calc exp 2 = exp (1 + 1) := by norm_num _ = exp 1 * exp 1 := Real.exp_add 1 1 _ = exp 1 ^ 2 := by ring have hs3 : (0 : ℝ) < √3 := Real.sqrt_pos.mpr (by norm_num) -- the derivative of the exponent 4M/r have hinner : ∀ r : ℝ, r ≠ 0 → HasDerivAt (fun r : ℝ => 4 * M / r) (-(4 * M) / r ^ 2) r := by intro r hr have := (hasDerivAt_inv hr).const_mul (4 * M) refine this.congr_deriv ?_ |>.congr_of_eventuallyEq (Filter.Eventually.of_forall fun y => ?_) · field_simp · simp [div_eq_mul_inv] refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ · intro r hr have hexp := (hinner r hr).exp have := (hasDerivAt_pow 2 r).mul hexp refine this.congr_deriv ?_ field_simp ring · intro r constructor · intro h rcases mul_eq_zero.mp h with h | h · exact absurd h (Real.exp_pos _).ne' · linarith · intro h; subst h; ring · intro r hr have hexp := (hinner r hr).exp have hlin : HasDerivAt (fun r : ℝ => 2 * r - 4 * M) 2 r := by simpa using ((hasDerivAt_id r).const_mul (2 : ℝ)).sub_const (4 * M) have := hexp.mul hlin refine this.congr_deriv ?_ field_simp ring · rw [h42]; field_simp; ring · rw [h42, he2]; ring · have h1 : exp 1 ≠ 0 := (Real.exp_pos 1).ne' rw [h42, Real.exp_neg, he2] field_simp · have h1 : exp 1 ≠ 0 := (Real.exp_pos 1).ne' field_simp /-- 21:P1 — the innermost stable circular orbit of the exponential metric (`G = m = 1`, isotropic radius), with the circular-orbit relations of the paper's `prop:isco` taken as given and not formalised (`L² = e^{2/r} r²/(r − 2)` and `E² = e^{−2/r}(r − 1)/(r − 2)` for a circular orbit at `r > 2`): what is proved is that `log L²` has derivative `(r² − 6r + 4)/(r²(r − 2))`, that `r_ISCO = 3 + √5` is the root of `r² − 6r + 4` above `2`, and that `(r − 1)/(r − 2) = r/4` there, so `E² = e^{−2/r} r/4` at the orbit. -/ theorem isco (r : ℝ) (hr : 2 < r) : HasDerivAt (fun r : ℝ => 2 / r + 2 * log r - log (r - 2)) ((r ^ 2 - 6 * r + 4) / (r ^ 2 * (r - 2))) r ∧ (3 + √5) ^ 2 - 6 * (3 + √5) + 4 = 0 ∧ 2 < 3 + √5 ∧ (3 + √5 - 1) / (3 + √5 - 2) = (3 + √5) / 4 := by have h5 := Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num) have hs5 : (0 : ℝ) < √5 := by positivity refine ⟨?_, by linear_combination h5, by linarith, ?_⟩ · have hr0 : r ≠ 0 := by linarith have hr2 : r - 2 ≠ 0 := by linarith have d1 : HasDerivAt (fun r : ℝ => 2 / r) (-(2 / r ^ 2)) r := by have := (hasDerivAt_inv hr0).const_mul 2 convert this using 1 <;> [funext x; skip] <;> ring have d2 : HasDerivAt (fun r : ℝ => 2 * log r) (2 * r⁻¹) r := (Real.hasDerivAt_log hr0).const_mul 2 have d3 : HasDerivAt (fun r : ℝ => log (r - 2)) (1 / (r - 2)) r := ((hasDerivAt_id' r).sub_const 2).log hr2 convert (d1.add d2).sub d3 using 1 field_simp ring · rw [div_eq_div_iff (by linarith) (by norm_num)] linear_combination -h5 /-- A bracket of `e^{−x}` from `x₁ < x < x₂`, a lower bound of `e^{x₁}` and an upper bound of `e^{x₂}`. -/ theorem exp_neg_bracket {x x₁ x₂ lo hi : ℝ} (hx₁ : x₁ < x) (hx₂ : x < x₂) (hlo : 0 < lo) (h1 : lo < exp x₁) (h2 : exp x₂ < hi) : hi⁻¹ < exp (-x) ∧ exp (-x) < lo⁻¹ := by constructor · calc hi⁻¹ < (exp x₂)⁻¹ := inv_strictAnti₀ (exp_pos _) h2 _ = exp (-x₂) := (exp_neg _).symm _ < exp (-x) := exp_lt_exp.mpr (by linarith) · calc exp (-x) < exp (-x₁) := exp_lt_exp.mpr (by linarith) _ = (exp x₁)⁻¹ := exp_neg _ _ < lo⁻¹ := inv_strictAnti₀ hlo h1 /-- The Taylor brackets of `e^t` at the two ends of `t = 2/r_ISCO = (3 − √5)/2`. -/ theorem exp_isco_tail_bounds : (1.465161 : ℝ) < exp 0.381966 ∧ exp (0.3819661 : ℝ) < 1.465163 := by constructor · have h := abs_le.1 (Real.exp_bound (x := 0.381966) (by rw [abs_of_pos (by norm_num)]; norm_num) (n := 7) (by norm_num)) rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.381966)] at h have h1 := h.1 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢ linarith · have h := Real.exp_bound' (x := 0.3819661) (by norm_num) (by norm_num) (n := 7) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢ linarith /-- `√5` to seven places. -/ theorem sqrt_five_bounds : (2.2360679 : ℝ) < √5 ∧ √5 < 2.2360680 := ⟨(Real.lt_sqrt (by norm_num)).mpr (by norm_num), (Real.sqrt_lt' (by norm_num)).mpr (by norm_num)⟩ /-- 21:P1 — the accretion efficiency bracketed: at `r_ISCO = 3 + √5` the orbital energy `E = √(e^{−2/r} r/4)` lies between `0.9452` and `0.9453`, so `1 − E` is between `5.47 %` and `5.48 %` (the text's `5.48 %`), against Schwarzschild's `1 − √(8/9)` between `5.71 %` and `5.72 %`. -/ theorem isco_efficiency : (0.0547 : ℝ) < 1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) ∧ 1 - √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) < 0.0548 ∧ (0.0571 : ℝ) < 1 - √(8 / 9) ∧ 1 - √(8 / 9) < (0.0572 : ℝ) := by obtain ⟨s1, s2⟩ := sqrt_five_bounds obtain ⟨t1, t2⟩ := exp_isco_tail_bounds have hx : 2 / (3 + √5) = (3 - √5) / 2 := by have h5 := Real.sq_sqrt (show (0 : ℝ) ≤ 5 by norm_num) rw [div_eq_div_iff (by positivity) (by norm_num)] linear_combination h5 obtain ⟨hlo, hhi⟩ := exp_neg_bracket (x := 2 / (3 + √5)) (x₁ := 0.381966) (x₂ := 0.3819661) (by rw [hx]; linarith) (by rw [hx]; linarith) (by norm_num) t1 t2 norm_num at hlo hhi have hE := exp_pos (-(2 / (3 + √5))) have hv1 : (0.89341 : ℝ) < exp (-(2 / (3 + √5))) * (3 + √5) / 4 := by nlinarith have hv2 : exp (-(2 / (3 + √5))) * (3 + √5) / 4 < (0.89345 : ℝ) := by nlinarith have hq1 : (0.9452 : ℝ) < √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) := (Real.lt_sqrt (by norm_num)).mpr (by nlinarith) have hq2 : √(exp (-(2 / (3 + √5))) * (3 + √5) / 4) < (0.9453 : ℝ) := (Real.sqrt_lt' (by norm_num)).mpr (by nlinarith) have hs1 : (0.9428 : ℝ) < √(8 / 9) := (Real.lt_sqrt (by norm_num)).mpr (by norm_num) have hs2 : √(8 / 9 : ℝ) < 0.9429 := (Real.sqrt_lt' (by norm_num)).mpr (by norm_num) refine ⟨by linarith, by linarith, by linarith, by linarith⟩ /-- The arithmetic behind 21:C13's capacity ratio: for `r_f = r_s/L` the square of `r_f/r_s` is `1/L²`, and at `L = ln Ω = 283.5` (the scale import) the ratio lies between `1.24 × 10⁻⁵` and `1.25 × 10⁻⁵` (the text's `1.24 × 10⁻⁵`); that the externally resolvable capacity scales as `(r_f/r_s)²` is the paper's count, not formal content. -/ theorem capacity_ratio (rs L : ℝ) (hrs : rs ≠ 0) (hL : L ≠ 0) : (rs / L / rs) ^ 2 = 1 / L ^ 2 := by field_simp theorem capacity_ratio_numeral : (1.24e-5 : ℝ) < 1 / 283.5 ^ 2 ∧ (1 / 283.5 ^ 2 : ℝ) < 1.25e-5 := by norm_num /-- 21:C4 — the redshift as clock rate: the bias field `e^{−u}` with `u = Gm/rc²` gives `Δf/f = 1 − e^{−u} = u + O(u²)`, `|1 − e^{−u} − u| ≤ u²` on `0 ≤ u ≤ 1`. -/ theorem redshift_linear (u : ℝ) (h0 : 0 ≤ u) (h1 : u ≤ 1) : |1 - exp (-u) - u| ≤ u ^ 2 := by have h := Real.exp_bound (x := -u) (by rw [abs_neg, abs_of_nonneg h0]; exact h1) (n := 2) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial, abs_neg, abs_of_nonneg h0] at h rw [abs_le] at h ⊢ constructor <;> nlinarith [sq_nonneg u] end strongfield /-! ## The floor and the crossover (21:C19, P4, X2) -/ section floor /-- 21:C19, 21:P4 — the registration root: for `0 < w < 1` the quadratic `wη² − 2η + w = 0` (rational in the paper's `w`, here over `ℝ`) has exactly the roots `(1 ∓ √(1 − w²))/w`; the smaller, `η = (1 − √(1 − w²))/w`, lies in `(0, 1)` and the larger exceeds `1`, so the in-`(0, 1)` root that fixes the resolved fraction `f = 1 − η^a` is unique. -/ theorem registration_root (w : ℝ) (hw0 : 0 < w) (hw1 : w < 1) : w * ((1 - √(1 - w ^ 2)) / w) ^ 2 - 2 * ((1 - √(1 - w ^ 2)) / w) + w = 0 ∧ 0 < (1 - √(1 - w ^ 2)) / w ∧ (1 - √(1 - w ^ 2)) / w < 1 ∧ 1 < (1 + √(1 - w ^ 2)) / w ∧ (∀ x : ℝ, w * x ^ 2 - 2 * x + w = 0 → x = (1 - √(1 - w ^ 2)) / w ∨ x = (1 + √(1 - w ^ 2)) / w) := by have hw2 : 0 ≤ 1 - w ^ 2 := by nlinarith set s := √(1 - w ^ 2) with hs have hs2 : s ^ 2 = 1 - w ^ 2 := Real.sq_sqrt hw2 have hs0 : 0 ≤ s := Real.sqrt_nonneg _ have hs1 : s < 1 := by rw [hs, Real.sqrt_lt' (by norm_num)]; nlinarith have hsw : 1 - w < s := by nlinarith [mul_pos hw0 (sub_pos.mpr hw1)] have hab : (1 - s) / w + (1 + s) / w = 2 / w := by rw [← add_div]; ring_nf have hsum : w * (2 / w) = 2 := by field_simp have hprod : w * ((1 - s) / w * ((1 + s) / w)) = w := by rw [div_mul_div_comm, ← mul_div_assoc, div_eq_iff (by positivity)] linear_combination (-w) * hs2 have hquad : ∀ x : ℝ, w * x ^ 2 - 2 * x + w = w * (x - (1 - s) / w) * (x - (1 + s) / w) := by intro x have e : w * (x - (1 - s) / w) * (x - (1 + s) / w) = w * x ^ 2 - w * ((1 - s) / w + (1 + s) / w) * x + w * ((1 - s) / w * ((1 + s) / w)) := by ring rw [e, hab, hsum, hprod] refine ⟨?_, div_pos (by linarith) hw0, ?_, ?_, ?_⟩ · rw [hquad]; ring · rw [div_lt_one hw0]; linarith · rw [lt_div_iff₀ hw0]; linarith · intro x hx rw [hquad] at hx rcases mul_eq_zero.mp hx with h | h · rcases mul_eq_zero.mp h with h | h · exact absurd h hw0.ne' · left; linarith · right; linarith /-- 21:C19, 21:P4 — the crossover `g_obs = g_N/(1 − e^{−√x})`, `x = g_N/a₀`, squeezed: with `t = √x > 0`, `1 ≤ t/(1 − e^{−t})`, and `t/(1 − e^{−t}) ≤ 1/(1 − 3t/4)` for `t ≤ 1`; and the Tully–Fisher algebra is exact: `v² = g_obs r` with `g_obs = √(g_N a₀)`, `g_N = GM/r²`, gives `v⁴ = GMa₀`. -/ theorem crossover_limits (t : ℝ) (ht : 0 < t) : 0 < 1 - exp (-t) ∧ 1 ≤ t / (1 - exp (-t)) ∧ (t ≤ 1 → t / (1 - exp (-t)) ≤ 1 / (1 - 3 * t / 4)) ∧ (∀ G M r a₀ v : ℝ, 0 < r → 0 ≤ G * M → 0 ≤ a₀ → v ^ 2 = √(G * M / r ^ 2 * a₀) * r → v ^ 4 = G * M * a₀) := by have hpos : 0 < 1 - exp (-t) := by have : exp (-t) < exp 0 := exp_lt_exp.mpr (by linarith) rw [exp_zero] at this linarith refine ⟨hpos, ?_, ?_, ?_⟩ · rw [le_div_iff₀ hpos] have := Real.add_one_le_exp (-t) linarith · intro ht1 have h := Real.exp_bound (x := -t) (by rw [abs_neg, abs_of_pos ht]; exact ht1) (n := 2) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial, abs_neg, abs_of_pos ht] at h rw [abs_le] at h have h34 : 0 < 1 - 3 * t / 4 := by linarith rw [div_le_div_iff₀ hpos h34] nlinarith · intro G M r a₀ v hr hGM ha v2 have hnn : 0 ≤ G * M / r ^ 2 * a₀ := by positivity calc v ^ 4 = (v ^ 2) ^ 2 := by ring _ = (√(G * M / r ^ 2 * a₀)) ^ 2 * r ^ 2 := by rw [v2]; ring _ = G * M / r ^ 2 * a₀ * r ^ 2 := by rw [Real.sq_sqrt hnn] _ = G * M * a₀ := by field_simp /-- 21:C19, 21:P4, 21:X2 — the deep limit: `t/(1 − e^{−t}) → 1` as `t → 0⁺`, so `g_obs/√(g_N a₀) → 1` — the deep regime `g_obs = √(g_N a₀)`, the floor read as noise with no dark sector. -/ theorem crossover_deep_limit : Filter.Tendsto (fun t : ℝ => t / (1 - exp (-t))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := by have hc : ContinuousAt (fun t : ℝ => 1 / (1 - 3 * t / 4)) 0 := by apply ContinuousAt.div continuousAt_const · fun_prop · norm_num have hup : Filter.Tendsto (fun t : ℝ => 1 / (1 - 3 * t / 4)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := by have := hc.tendsto.mono_left (nhdsWithin_le_nhds : nhdsWithin (0 : ℝ) (Set.Ioi 0) ≤ nhds 0) simpa using this refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hup ?_ ?_ · filter_upwards [self_mem_nhdsWithin] with t ht exact (crossover_limits t ht).2.1 · filter_upwards [Ioo_mem_nhdsGT (show (0 : ℝ) < 1 by norm_num)] with t ht exact (crossover_limits t ht.1).2.2.1 ht.2.le /-- 21:C19, 21:P4 — the Newtonian limit: `1 − e^{−t} → 1` as `t → ∞`, so `g_obs/g_N → 1` for `x → ∞`. -/ theorem crossover_newton_limit : Filter.Tendsto (fun t : ℝ => 1 - exp (-t)) Filter.atTop (nhds 1) := by have := Real.tendsto_exp_neg_atTop_nhds_zero simpa using tendsto_const_nhds.sub this /-- The Taylor brackets of `e^t` at the two ends of `t = √5 − 2`. -/ theorem exp_root_five_tail_bounds : (1.2662602 : ℝ) < exp 0.2360679 ∧ exp (0.2360680 : ℝ) < 1.2662605 := by constructor · have h := abs_le.1 (Real.exp_bound (x := 0.2360679) (by rw [abs_of_pos (by norm_num)]; norm_num) (n := 7) (by norm_num)) rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.2360679)] at h have h1 := h.1 norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢ linarith · have h := Real.exp_bound' (x := 0.2360680) (by norm_num) (by norm_num) (n := 7) (by norm_num) norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢ linarith /-- 21:P4 — the discriminant against the simple interpolant at `g_N = 5a₀`: the crossover `ν(5) = 1/(1 − e^{−√5})` lies between `1.11966` and `1.11967`, the simple interpolant `ν_s(5) = 1/2 + √(1/4 + 1/5)` between `1.17082` and `1.17083`, so they part by between `0.0511` and `0.0512` in `g_obs/g_N` (the text's `0.05`). -/ theorem interpolant_discriminant : (1.11966 : ℝ) < 1 / (1 - exp (-√5)) ∧ 1 / (1 - exp (-√5)) < 1.11967 ∧ (1.17082 : ℝ) < 1 / 2 + √(1 / 4 + 1 / 5) ∧ 1 / 2 + √(1 / 4 + 1 / 5) < 1.17083 ∧ (0.0511 : ℝ) < (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) ∧ (1 / 2 + √(1 / 4 + 1 / 5)) - 1 / (1 - exp (-√5)) < 0.0512 := by obtain ⟨s1, s2⟩ := sqrt_five_bounds obtain ⟨t1, t2⟩ := exp_root_five_tail_bounds have hm1 := Real.exp_neg_one_gt_d9 have hm2 := Real.exp_neg_one_lt_d9 have hsplit : exp (-√5) = exp (-1) * exp (-1) * exp (2 - √5) := by rw [← exp_add, ← exp_add]; ring_nf obtain ⟨hlo, hhi⟩ := exp_neg_bracket (x := √5 - 2) (x₁ := 0.2360679) (x₂ := 0.2360680) (by linarith) (by linarith) (by norm_num) t1 t2 norm_num at hlo hhi have hm : (0 : ℝ) < exp (-1) := exp_pos _ have hq1 : (0.106877 : ℝ) < exp (-√5) := by rw [hsplit]; nlinarith [mul_pos hm hm] have hq2 : exp (-√5) < (0.106878 : ℝ) := by rw [hsplit]; nlinarith [mul_pos hm hm] have hden : (0 : ℝ) < 1 - exp (-√5) := by linarith have hr1 : (1.11966 : ℝ) < 1 / (1 - exp (-√5)) := by rw [lt_div_iff₀ hden]; linarith have hr2 : 1 / (1 - exp (-√5)) < (1.11967 : ℝ) := by rw [div_lt_iff₀ hden]; linarith have hs1 : (0.67082 : ℝ) < √(1 / 4 + 1 / 5) := (Real.lt_sqrt (by norm_num)).mpr (by norm_num) have hs2 : √(1 / 4 + 1 / 5 : ℝ) < 0.67083 := (Real.sqrt_lt' (by norm_num)).mpr (by norm_num) refine ⟨hr1, hr2, by linarith, by linarith, by linarith, by linarith⟩ end floor /-! ## The primordial fixed point (21:C18) -/ section primordial /-- 21:C18 — the fixed point: for a power law `P(k) = k^n` the dimensionless `k³P(k)` is the same at every scale `k > 0` exactly when `n = −3`, i.e. `n_s − 1 = n + 3 = 0`, the Harrison–Zel'dovich `n_s = 1`, uniquely; that the drive's jitter spectrum is this fixed point is the paper's argument. -/ theorem scale_invariance_iff (n : ℝ) : (∀ k : ℝ, 0 < k → k ^ 3 * k ^ n = 1) ↔ n = -3 := by constructor · intro h have h2 := h 2 (by norm_num) have h3 : (2 : ℝ) ^ (n + 3) = 1 := by rw [rpow_add (by norm_num : (0 : ℝ) < 2), show (2 : ℝ) ^ (3 : ℝ) = 2 ^ (3 : ℕ) by exact_mod_cast rpow_natCast 2 3] linarith have hl := congrArg Real.log h3 rw [Real.log_rpow (by norm_num), Real.log_one] at hl rcases mul_eq_zero.mp hl with h | h · linarith · exact absurd h (Real.log_pos (by norm_num)).ne' · rintro rfl k hk rw [Real.rpow_neg hk.le, show (3 : ℝ) = (3 : ℕ) by norm_num, rpow_natCast] exact mul_inv_cancel₀ (pow_ne_zero 3 hk.ne') end primordial /-! ## The dispersion symbol and the locked sum (21:C1, C15) -/ section lattice /-- 21:C15 — the dispersion symbol: the central second difference acts on the plane wave `e^{ikx}` by `−(2 − 2 cos k) = −4 sin²(k/2)`; the wave equation, its two polarisations and the speed `c` are the package's. -/ theorem dispersion_symbol (k : ℝ) : 2 - 2 * cos k = 4 * sin (k / 2) ^ 2 := by have h := Real.cos_two_mul (k / 2) rw [show 2 * (k / 2) = k by ring] at h rw [h, Real.cos_sq']; ring /-- 21:C1 — the coherent coefficient: a locked cluster of `m` cells with one phase sums with coefficient exactly `m`, `‖Σ_{j linarith rw [show -(2 * (1 / 2 * log ((1 + U / 2) / (1 - U / 2)))) = -log ((1 + U / 2) / (1 - U / 2)) by ring, exp_neg, exp_log hpos, inv_div] /-- 21:C8, 21:P6, 21:C7 — the post-Newtonian inputs as Taylor brackets on `|U| ≤ 1/2`: the exponential metric's `A = e^{−2U}`, `B = e^{2U}` against the isotropic Schwarzschild `A_S = ((1 − U/2)/(1 + U/2))²`, `B_S = (1 + U/2)⁴` satisfy `|A − A_S − U³/6| ≤ 3U⁴` and `|B − B_S − U²/2| ≤ 3|U|³`: the single-potential inputs consumed by C23 coincide through first post-Newtonian order (`A` to `O(U²)`, `B` to `O(U)`) and part at 2PN with `δA = U³/6`, `δB = U²/2`; the two-body superposition of C23 is the package's. -/ theorem pn_series (U : ℝ) (hU : |U| ≤ 1 / 2) : |exp (-(2 * U)) - ((1 - U / 2) / (1 + U / 2)) ^ 2 - U ^ 3 / 6| ≤ 3 * U ^ 4 ∧ |exp (2 * U) - (1 + U / 2) ^ 4 - U ^ 2 / 2| ≤ 3 * |U| ^ 3 := by have hU' := abs_le.1 hU have hden : 1 + U / 2 ≠ 0 := by intro h; linarith [hU'.1] have hden2 : (9 / 16 : ℝ) ≤ (1 + U / 2) ^ 2 := by nlinarith [hU'.1] have hU4 : 0 ≤ U ^ 4 := by positivity have habs4 : |U| ^ 4 = U ^ 4 := by rw [← abs_pow, abs_of_nonneg hU4] have habs3 : |U| ^ 3 * |U| = U ^ 4 := by rw [← pow_succ, ← abs_pow, abs_of_nonneg (by positivity)] have hU3 : 0 ≤ |U| ^ 3 := by positivity constructor · have h := Real.exp_bound (x := -(2 * U)) (by rw [abs_neg, abs_mul, abs_two]; linarith) (n := 4) (by norm_num) rw [abs_neg, abs_mul, abs_two] at h norm_num [Finset.sum_range_succ, Nat.factorial] at h rw [abs_le] at h have hpow : (2 * |U|) ^ 4 = 16 * U ^ 4 := by rw [mul_pow, habs4]; norm_num rw [hpow] at h have hA : ((1 - U / 2) / (1 + U / 2)) ^ 2 - (1 - 2 * U + 2 * U ^ 2 - 3 / 2 * U ^ 3) = U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2 := by rw [div_pow, eq_div_iff (pow_ne_zero 2 hden), sub_mul, div_mul_cancel₀ _ (pow_ne_zero 2 hden)] ring have hrem : |U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2| ≤ 2.12 * U ^ 4 := by rw [abs_div, abs_mul, abs_of_nonneg hU4, abs_of_pos (by positivity : (0 : ℝ) < (1 + U / 2) ^ 2), div_le_iff₀ (by positivity)] have : |1 + 3 * U / 8| ≤ 1.1875 := by rw [abs_le]; constructor <;> linarith [hU'.1, hU'.2] nlinarith [abs_nonneg (1 + 3 * U / 8)] rw [abs_le] at hrem have hA' : ((1 - U / 2) / (1 + U / 2)) ^ 2 = 1 - 2 * U + 2 * U ^ 2 - 3 / 2 * U ^ 3 + U ^ 4 * (1 + 3 * U / 8) / (1 + U / 2) ^ 2 := by linarith [hA] rw [hA', abs_le] constructor <;> nlinarith [hrem.1, hrem.2, h.1, h.2] · have h := Real.exp_bound (x := 2 * U) (by rw [abs_mul, abs_two]; linarith) (n := 3) (by norm_num) rw [abs_mul, abs_two] at h norm_num [Finset.sum_range_succ, Nat.factorial] at h rw [abs_le] at h ⊢ have hpow : (2 * |U|) ^ 3 = 8 * |U| ^ 3 := by rw [mul_pow]; norm_num rw [hpow] at h have hU4' : U ^ 4 ≤ |U| ^ 3 / 2 := by rw [← habs3]; nlinarith have hcube : U ^ 3 ≤ |U| ^ 3 ∧ -(|U| ^ 3) ≤ U ^ 3 := by constructor · calc U ^ 3 ≤ |U ^ 3| := le_abs_self _ _ = |U| ^ 3 := abs_pow U 3 · calc -(|U| ^ 3) = -|U ^ 3| := by rw [abs_pow] _ ≤ U ^ 3 := neg_abs_le _ constructor <;> nlinarith [h.1, h.2, hcube.1, hcube.2] /-- 21:P2, 21:C10 — the numeral behind the preferred-frame scale: the drive's signature is `O(1/√Ω)` (the paper's `α₁, α₂`), and at the scale import's `Ω = 1.3 × 10¹²³` (00:A7) this lies between `2.7` and `2.8 × 10⁻⁶²` (the row's `3 × 10⁻⁶²`). -/ theorem preferred_frame_scale : (2.7e-62 : ℝ) < 1 / √(1.3e123) ∧ 1 / √(1.3e123) < 2.8e-62 := by have hs : 0 < √(1.3e123 : ℝ) := Real.sqrt_pos.2 (by norm_num) constructor · rw [lt_one_div (by norm_num) hs, Real.sqrt_lt' (by norm_num)]; norm_num · rw [one_div_lt hs (by norm_num), Real.lt_sqrt (by norm_num)]; norm_num end series end FRC.Strong /-! inlined: FrcLedger/Theme/Fields.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Theme.Fields — the chart theme's readings of the interactions (27-fields, 16 October 2026) The clauses of 27-fields that read the continuum: the phase cycle `ℤ/M` inside `U(1)` as the `M`-th roots of unity (`roots_inclusion`, 27:C1), the Wilson weight `1 − Re ζ ≥ 0` on the unit circle, zero at the identity alone (`wilson_weight_nonneg`, 27:C1), the `2T` area-law coefficient `c₁ = (x⁴ + 4x³ − 4x − 1)/(x⁴ + 8x³ + 6x² + 8x + 1)` in `(0, 1)` for `x = e^{β/2} > 1` (`area_law_positive`, 27:C1, C7, X7), the Fermi constant `G_F = 1/(√2 v²)` from `G_F/√2 = g²/(8 M_W²)` and `M_W² = g² v²/4` (`fermi_constant`, 27:C6); and, since 17 October 2026, the chart readings of the three exclusion rows: the one-loop running of the measured couplings to the meeting `α₁ = α₂` with the strong coupling's near-miss (`running_near_miss`, 27:P3), the proton lifetime `M_X⁴/(α² m_p⁵)` at the substrate and the GUT scales (`proton_lifetime`, 27:P4), the seesaw band and `m_b/m_τ` (`seesaw_band`, 27:P5). Classical (tier 2) on Mathlib's hierarchy. The finite content of the same rows is proved with no axioms in the core (`FrcCore/Theme/Interactions.lean`, `Theme/Unitary.lean`, `FrcCore/Fields.lean`). -/ namespace FRC.FieldsML open Real /-- 27:C1 — the phase cycle inside `U(1)`: `ζ_M = exp(2πi/M)` is a primitive `M`-th root of unity, `k ↦ ζ_M^k` is a homomorphism of the cycle (`ζ^{j+k} = ζ^j ζ^k`), injective on `0 ≤ k < M`, and every image is an `M`-th root. -/ theorem roots_inclusion (M : ℕ) (hM : M ≠ 0) : IsPrimitiveRoot (Complex.exp (2 * π * Complex.I / M)) M ∧ (∀ j k : ℕ, Complex.exp (2 * π * Complex.I / M) ^ (j + k) = Complex.exp (2 * π * Complex.I / M) ^ j * Complex.exp (2 * π * Complex.I / M) ^ k) ∧ (∀ j k : ℕ, j < M → k < M → Complex.exp (2 * π * Complex.I / M) ^ j = Complex.exp (2 * π * Complex.I / M) ^ k → j = k) ∧ (∀ k : ℕ, (Complex.exp (2 * π * Complex.I / M) ^ k) ^ M = 1) := by have h := Complex.isPrimitiveRoot_exp M hM refine ⟨h, fun j k => pow_add _ _ _, fun j k hj hk e => h.pow_inj hj hk e, fun k => ?_⟩ rw [← pow_mul, Nat.mul_comm k M, pow_mul, h.pow_eq_one, one_pow] /-- 27:C1 — the Wilson weight on the unit circle: for `‖ζ‖ = 1`, `0 ≤ 1 − Re ζ`, with equality exactly at `ζ = 1`. -/ theorem wilson_weight_nonneg (ζ : ℂ) (h : ‖ζ‖ = 1) : 0 ≤ 1 - ζ.re ∧ (1 - ζ.re = 0 ↔ ζ = 1) := by have hre : ζ.re ≤ 1 := h ▸ Complex.re_le_norm ζ refine ⟨by linarith, ⟨fun h0 => ?_, fun h1 => by rw [h1]; simp⟩⟩ have hre1 : ζ.re = 1 := by linarith have h2 : ζ.re * ζ.re + ζ.im * ζ.im = 1 := by rw [← Complex.normSq_apply, Complex.normSq_eq_norm_sq, h, one_pow] have him : ζ.im = 0 := by nlinarith exact Complex.ext (by simpa using hre1) (by simpa using him) /-- 27:C1, 27:C7, 27:X7 — the area law from positivity on `2T`: for `x = e^{β/2} > 1` the coefficient `c₁ = (x⁴ + 4x³ − 4x − 1)/(x⁴ + 8x³ + 6x² + 8x + 1)` lies in `(0, 1)`, so the string tension `σ = −ln c₁` is positive. -/ theorem area_law_positive (x : ℝ) (hx : 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 := by have hx0 : 0 < x := by linarith have hD : 0 < x ^ 4 + 8 * x ^ 3 + 6 * x ^ 2 + 8 * x + 1 := by positivity have hN : 0 < x ^ 4 + 4 * x ^ 3 - 4 * x - 1 := by have e : x ^ 4 + 4 * x ^ 3 - 4 * x - 1 = (x - 1) * (x ^ 3 + 5 * x ^ 2 + 5 * x + 1) := by ring rw [e]; exact mul_pos (by linarith) (by positivity) refine ⟨div_pos hN hD, (div_lt_one hD).2 ?_⟩ nlinarith /-- 27:C6 — the Fermi constant: with `M_W² = g² v²/4` and `G_F/√2 = g²/(8 M_W²)`, `G_F = 1/(√2 v²)`. -/ theorem fermi_constant (g v G MW2 : ℝ) (hg : g ≠ 0) (hv : v ≠ 0) (hM : MW2 = g ^ 2 * v ^ 2 / 4) (hG : G / √2 = g ^ 2 / (8 * MW2)) : G = 1 / (√2 * v ^ 2) := by have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 hv have hg2 : g ^ 2 ≠ 0 := pow_ne_zero 2 hg have hs : (√2 : ℝ) ≠ 0 := by positivity have h2 : (√2 : ℝ) * √2 = 2 := Real.mul_self_sqrt (by norm_num) have e : G / √2 = 1 / (2 * v ^ 2) := by rw [hG, hM]; field_simp; ring calc G = √2 * (G / √2) := by field_simp _ = √2 * (1 / (2 * v ^ 2)) := by rw [e] _ = 1 / (√2 * v ^ 2) := by rw [mul_one_div, div_eq_div_iff (mul_ne_zero two_ne_zero hv2) (mul_ne_zero hs hv2), ← mul_assoc, h2, one_mul] /-- 27:P3 [chart] — the one-loop running of the measured couplings with the Standard-Model coefficients `b = (41/10, −19/6, −7)`: at the meeting `α₁ = α₂` the strong coupling misses by less than a fifth, and the meeting scale `M_Z e^{2πu}` lies in `[10¹², 10¹⁴]` GeV. The inputs are the measured `α⁻¹(M_Z) = 127.951`, `sin²θ_W = 0.23121`, `α_s = 0.1179` and `M_Z = 91.1876` GeV (the paper's A6). -/ theorem running_near_miss (ainv s2 as b1 b2 b3 MZ : ℝ) (h1 : ainv = 127.951) (h2 : s2 = 0.23121) (h3 : as = 0.1179) (hb1 : b1 = 41 / 10) (hb2 : b2 = -19 / 6) (hb3 : b3 = -7) (hZ : 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 * exp (2 * π * ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2))) ∧ MZ * exp (2 * π * ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2))) < (10 : ℝ) ^ 14 := by set u : ℝ := ((3 / 5 * (1 - s2) * ainv - s2 * ainv) / (b1 - b2)) with hudef have hu : u = (3 / 5 * (1 - 0.23121) * 127.951 - 0.23121 * 127.951) / (41 / 10 - -19 / 6) := by rw [hudef, h1, h2, hb1, hb2] have hu25 : 25 < 2 * π * u := by rw [hu]; nlinarith [pi_gt_d2] have hu26 : 2 * π * u < 26 := by rw [hu]; nlinarith [pi_lt_d2] have e25 : (2.7182818283 : ℝ) ^ 25 < exp (2 * π * u) := by calc (2.7182818283 : ℝ) ^ 25 < exp 1 ^ 25 := by exact pow_lt_pow_left₀ exp_one_gt_d9 (by norm_num) (by norm_num) _ = exp 25 := by rw [← exp_nat_mul]; norm_num _ < exp (2 * π * u) := exp_lt_exp.2 hu25 have e26 : exp (2 * π * u) < (2.7182818286 : ℝ) ^ 26 := by calc exp (2 * π * u) < exp 26 := exp_lt_exp.2 hu26 _ = exp 1 ^ 26 := by rw [← exp_nat_mul]; norm_num _ < (2.7182818286 : ℝ) ^ 26 := pow_lt_pow_left₀ exp_one_lt_d9 (exp_pos 1).le (by norm_num) refine ⟨?_, ?_, ?_⟩ · rw [hu, h1, h2, h3, hb2, hb3]; norm_num [abs_lt] · rw [hZ]; nlinarith [e25] · rw [hZ]; nlinarith [e26] /-- 27:P4 [chart] — the proton lifetime `τ_p = M_X⁴/(α² m_p⁵)` in years, with `m_p = 0.938` GeV, `α_GUT = 1/40`, `ħ = 6.582 × 10⁻²⁵` GeV s and the year `3.156 × 10⁷` s: at the Planck scale `M_X = 1.22 × 10¹⁹` GeV it exceeds `10⁴⁵` yr, at `M_X = 10¹⁶` GeV it exceeds the Super-Kamiokande bound `10³⁴` yr, and two lifetimes stand in the ratio `(M′/M)⁴`. -/ theorem proton_lifetime (mp a hbar yr : ℚ) (hm : mp = 0.938) (ha : a = 1 / 40) (hh : hbar = 6.582e-25) (hy : yr = 3.156e7) : (10 : ℚ) ^ 45 ≤ (1.22e19 : ℚ) ^ 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 := by subst hm ha hh hy refine ⟨by norm_num, by norm_num, fun M M' hM hM' => ?_⟩ have hM0 : M ≠ 0 := hM.ne' field_simp /-- 27:P5 [chart] — the seesaw `m_ν = y² v²/M_R` with `v = 174` GeV: for `y = 0.3` at `M_R = 10¹⁴` GeV and for `y = 1` at `M_R = 10¹⁵` GeV the light mass lies in `(0.01, 0.1)` eV; and `m_b/m_τ = 4.18/1.777` lies in `(2, 3)`. -/ theorem seesaw_band (v mb mt : ℚ) (hv : v = 174) (hb : mb = 4.18) (ht : mt = 1.777) : (0.01 : ℚ) < (0.3 : ℚ) ^ 2 * v ^ 2 / 1e14 * 1e9 ∧ (0.3 : ℚ) ^ 2 * v ^ 2 / 1e14 * 1e9 < 0.1 ∧ (0.01 : ℚ) < (1 : ℚ) ^ 2 * v ^ 2 / 1e15 * 1e9 ∧ (1 : ℚ) ^ 2 * v ^ 2 / 1e15 * 1e9 < 0.1 ∧ (2 : ℚ) < mb / mt ∧ mb / mt < 3 := by subst hv hb ht norm_num end FRC.FieldsML /-! inlined: FrcLedger/Keys/Chart.lean (verbatim, minus its import lines) -/ /-! # FrcLedger.Keys.Chart — the keyed theorems of the chart theme (ledger migration, task LM19) One declaration per key, `FRC.LedgerML.p`, 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..p` as an alias. Every declaration has the axioms of Mathlib's hierarchy at most (`check_axioms.py`). -/ namespace FRC.LedgerML -- Keys of the chart theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file) /-- p00009 — 00:A7. Scale, the sole quantitative import: the de Sitter entropy of the observable universe fixes the cardinality exactly, $\Om=4\dS+1$. Its chart numeral is $\dS=\pi(r_H/\ell_P)^2=3.3\times10^{122}$ [chart] at $r_H=c/H_\Lambda$ (14-entr), so $\Om=1.3\times10^{123}$ [chart]. The Carrier congruences are certified by the realisations (B5, C8), not imported. Metrology: L2. -/ theorem p00009 : ∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → 331e120 < S ∧ S < 332e120 ∧ 132e121 < Ω ∧ Ω < 133e121 := @FRC.Chart.scale_import /-- p00133 — 00:P1. The acceleration floor tracks the drive rate, $a_0(z)\propto H(z)$: a relation, $\Om$-blind, derived from L1 under the gravity realisation (D5); the knee shifts and the Tully--Fisher zero-point evolves as $E(z)^{1/4}$. Falsifier: a floor constant in redshift, or tracking other than $H(z)$. Confrontation (43-muse): MUSE-DARK III excludes a constant floor to $z=1.3$; RC100 implies the local floor by $z\simeq2$, pending refit. -/ theorem p00133 : ∀ (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < M → (0 : ℝ) < H (0 : ℝ) → (0 : ℝ) < H z → (∀ (z : ℝ), a z = c * H z / ((2 : ℝ) * Real.pi)) → (0 : ℝ) < v (0 : ℝ) → (0 : ℝ) < v z → (∀ (z : ℝ), v z ^ (4 : ℕ) = G * M * a z) → a z / a (0 : ℝ) = H z / H (0 : ℝ) ∧ v z / v (0 : ℝ) = (H z / H (0 : ℝ)) ^ (1 / 4 : ℝ) := @FRC.Chart.running_floor /-- p00148 — 00:L8. $n_s=1$ is the scale-dilation fixed point (Harrison--Zel'dovich [import]). The tilt's committed form is $n_s-1=-\pi^2/\ln\Om$ [chart], $\ln\Om$ the e-fold count of the frame's scale range from $1/\sqrt\Om$ to $\sqrt\Om$, a realisation fixed by the measured tilt: $-0.0348$ [approx] at $\ln\Om=283.5$ (A7), $+0.07\sigma$ from Planck 2018's $-0.0351\pm0.0042$ [import]. The count $\tfrac12\ln\Om$ is excluded at $8.2\sigma$. Falsifier: a Planck-resolution deviation from $-\pi^2/\ln\Om$. -/ theorem p00148 : (3481e-5 < Real.pi ^ (2 : ℕ) / 283.5 ∧ Real.pi ^ (2 : ℕ) / 283.5 < 3482e-5 ∧ 68e-3 * 42e-4 < 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 ∧ 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 < 69e-3 * 42e-4 ∧ 8.2 * 42e-4 < Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 ∧ Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 < 8.25 * 42e-4) ∧ ∀ (Ω : ℝ), (0 : ℝ) < Ω → Real.log (√Ω / ((1 : ℝ) / √Ω)) = Real.log Ω := And.intro @FRC.Chart.tilt_ledger (@FRC.Chart.efold_count) /-- p00192 — 00:L1. The synchronisation floor $a_0=cH_0/2\pi$ fixes the acceleration scale parameter-free: the $2\pi$ by the angle--count dictionary (14:B2), the threshold one cycle per drive period (32:B3), $1.04\times10^{-10}$ [chart] at the channel-1 $H_0=67.4$ (L3), tied to $H(z)$, not $\Lambda$ (P1; 21:X1). Below the floor the amplitude reading, given the barrier identification (32:B8, 21:B9), gives the radial acceleration relation unfitted. Falsifiers: 32:B3, 21:P4. -/ theorem p00192 : (∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67) ∧ ∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 1045e-13 := And.intro @FRC.Chart.floor_value (@FRC.Chart.floor_fine) /-- p00193 — 00:L3. \textbf{The octant record depth and its outputs}: the record depth is bounded by the octant, $\dS/2$ chronons $=13.79$ Gyr ($(\pi/4)r_H/c$, chart), on the octant sector of B14. Zero-freedom: $\Omega_\Lambda=\tanh^2(3\pi/8)=0.684$ (chart; $0.19\sigma$); on the stellar age $13.61\pm0.34$ Gyr, $H_0=68.2\pm1.7$ ($2.4\sigma$ from the ladder); $w=-1$ rigid --- a confirmed drift falsifies $\Lambda\sim1/\Om$. Falsifiers: octant-capped ages, the running floor $a_0(z)\propto H(z)$ (Z7), the ladder bias. -/ theorem p00193 : (∀ (S r c : ℝ), S ≠ (0 : ℝ) → S / (2 : ℝ) / ((4 : ℝ) * S) * ((2 : ℝ) * Real.pi * r / c) = Real.pi / (4 : ℝ) * r / c) ∧ (0.68368 < Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) ∧ Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) < 0.68369 ∧ 0.18 * 7e-3 < 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) ∧ 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) < 0.19 * 7e-3) ∧ (0.186 * 7e-3 < 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) ∧ 0.685 - Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) < 0.19 * 7e-3) ∧ (∀ (t H0 HΛ Ω : ℝ), t * HΛ = Real.pi / (4 : ℝ) → HΛ = H0 * √Ω → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) → t * H0 = Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ))) ∧ (0.9498 < Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ∧ Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) < 0.9499) ∧ (FRC.Chart.lcdmAge (Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) = Real.pi / (4 : ℝ) ∧ ∀ (Ω : ℝ), (0 : ℝ) ≤ Ω → Ω < (1 : ℝ) → FRC.Chart.lcdmAge Ω = Real.pi / (4 : ℝ) → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ)) ∧ (∀ (t H0 : ℝ), t = 1379e7 * (365.25 * (86400 : ℝ)) → t * H0 = Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) → 67.35 < H0 * 30856775814913673e3 ∧ H0 * 30856775814913673e3 < 67.36) ∧ ∀ (t H0 : ℝ), t = 1361e7 * (365.25 * (86400 : ℝ)) → t * H0 = Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) → 68.24 < H0 * 30856775814913673e3 ∧ H0 * 30856775814913673e3 < 68.25 ∧ 1.70 < H0 * 30856775814913673e3 * (0.34 / 13.61) ∧ H0 * 30856775814913673e3 * (0.34 / 13.61) < 1.71 ∧ 2.40 < (73.0 - H0 * 30856775814913673e3) / √(1.7 ^ (2 : ℕ) + 1.0 ^ (2 : ℕ)) ∧ (73.0 - H0 * 30856775814913673e3) / √(1.7 ^ (2 : ℕ) + 1.0 ^ (2 : ℕ)) < 2.42 := And.intro @FRC.Chart.octant_chart (And.intro @FRC.Chart.landing_bracket (And.intro @FRC.Chart.landing_fine (And.intro @FRC.Chart.age_rate_locus (And.intro @FRC.Chart.locus_bracket (And.intro @FRC.Chart.octant_inversion (And.intro @FRC.Chart.hubble_landing (@FRC.Chart.hubble_stellar))))))) /-- p00201 — 00:E14. \textbf{The eikonal pair}: on the exponential reading (E4) the photon sphere sits at $r_c=2M$, $b_c=2eM$, and the orbital rate equals the Lyapunov rate, $\Omega_c=\lambda=1/(2eM)$, both $3\sqrt3/(2e)$ of Schwarzschild's. The wave operator's $\ell=2$ mode (E13) is $(0.4641-0.0923\,i)/M$ [approx], $0.8\%$ above the eikonal $(\ell+\tfrac12)/(2eM)$. Falsifier: that mode read as the remnant's $(2,2,0)$ oscillation, $+24\%$ against Kerr, excluded by GW250114 [import]. -/ theorem p00201 : (∀ (M : ℝ), (0 : ℝ) < M → (∀ (r : ℝ), r ≠ (0 : ℝ) → HasDerivAt (fun r => r ^ (2 : ℕ) * Real.exp ((4 : ℝ) * M / r)) (Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) * r - (4 : ℝ) * M)) r) ∧ (∀ (r : ℝ), Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) * r - (4 : ℝ) * M) = (0 : ℝ) ↔ r = (2 : ℝ) * M) ∧ (∀ (r : ℝ), r ≠ (0 : ℝ) → HasDerivAt (fun r => Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) * r - (4 : ℝ) * M)) (Real.exp ((4 : ℝ) * M / r) * ((2 : ℝ) - (4 : ℝ) * M * ((2 : ℝ) * r - (4 : ℝ) * M) / r ^ (2 : ℕ))) r) ∧ Real.exp ((4 : ℝ) * M / ((2 : ℝ) * M)) * ((2 : ℝ) - (4 : ℝ) * M * ((2 : ℝ) * ((2 : ℝ) * M) - (4 : ℝ) * M) / ((2 : ℝ) * M) ^ (2 : ℕ)) = (2 : ℝ) * Real.exp (2 : ℝ) ∧ ((2 : ℝ) * M) ^ (2 : ℕ) * Real.exp ((4 : ℝ) * M / ((2 : ℝ) * M)) = ((2 : ℝ) * Real.exp (1 : ℝ) * M) ^ (2 : ℕ) ∧ Real.exp (-((4 : ℝ) * M / ((2 : ℝ) * M))) * ((2 : ℝ) * Real.exp (2 : ℝ)) / ((2 : ℝ) * (((2 : ℝ) * M) ^ (2 : ℕ) * Real.exp ((4 : ℝ) * M / ((2 : ℝ) * M)))) = ((1 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ) * M)) ^ (2 : ℕ) ∧ (1 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ) * M) / ((1 : ℝ) / ((3 : ℝ) * √(3 : ℝ) * M)) = (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ))) ∧ 1.0462 < (2 : ℝ) * Real.exp (1 : ℝ) / ((3 : ℝ) * √(3 : ℝ)) ∧ (2 : ℝ) * Real.exp (1 : ℝ) / ((3 : ℝ) * √(3 : ℝ)) < 1.0463 ∧ 0.9557 < (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ)) ∧ (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ)) < 0.9558 ∧ 2.46 < ((4 : ℝ) * Real.exp (1 : ℝ) - (6 : ℝ) * √(3 : ℝ)) * 5.12 ∧ ((4 : ℝ) * Real.exp (1 : ℝ) - (6 : ℝ) * √(3 : ℝ)) * 5.12 < 2.47 := And.intro @FRC.Strong.eikonal_pair (@FRC.Strong.shadow_bracket) /-- p14038 — 14:P3. The age--rate locus $t_{\mathrm{age}}H_0=(\pi/4)/\tanh(3\pi/8)=0.950$, exact for the realisation set. Read on the fit-independent stellar age ($13.61\pm0.34$ Gyr): $H_0=68.2\pm1.7$ km/s/Mpc \apx, $0.5\sigma$ from Planck, $0.65\sigma$ from TRGB, $2.4\sigma$ from the Cepheid ladder --- the framework favours the CMB/TRGB value at that significance, and forbids the $\Omega_\Lambda\approx0.76$ by which the rival chart would accommodate the ladder value at the same age. Read on the channel-1 $\Lambda$ it returns the channel-1 $H_0$ (to $0.1\%$): a consistency, not a prediction (C8). Falsifier: a confirmed ladder $H_0$ with the stellar age standing ($t_\star H_0\ge1.0$ against $0.950$). -/ theorem p14038 : (∀ (t H0 HΛ Ω : ℝ), t * HΛ = Real.pi / (4 : ℝ) → HΛ = H0 * √Ω → Ω = Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ^ (2 : ℕ) → t * H0 = Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ))) ∧ 0.9498 < Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) ∧ Real.pi / (4 : ℝ) / Real.tanh ((3 : ℝ) * Real.pi / (8 : ℝ)) < 0.9499 := And.intro @FRC.Chart.age_rate_locus (@FRC.Chart.locus_bracket) set_option linter.defProp false in /-- p20032 — 20:E1. The scale-evolution generator: on the shell the scale-shift $x\mapsto\gen^{\,r}x$ is a unitary permutation of $\Fx{\p}$ with the complex characters as eigenvectors; in the analytic chart [chart] the dilation group $U_r=e^{ir\Hh}$ has the self-adjoint generator $\Hh=-i(x\partial_x+\half)$ with generalised eigenfunctions $x^{-\bar\rho}$, $\rho=\half+i\gamma$, the symmetrizing $\half$ the half-turn of B8; the chart assignment is used nowhere as a shell identity. -/ def p20032 := And.intro @FRC.HorizonML.scale_shift (And.intro @FRC.Chart.character_eigen (@FRC.Chart.chi_shift)) set_option linter.defProp false in /-- p20043 — 20:E12, 00:Z10. \textbf{The shell theorem.} On every shell, with no hypothesis: (i) $v$ expands in the constant mode and the nonterminal modes of the quarter-turn meridian; (ii) every readout lies on $\Tr=1$, real part $2^{-1}=2\kp+1=-\pi$; (iii) the scale-shift has the modes as eigenvectors, eigenphases $2\pi j/(\p-1)$ independent of $v$. No off-line mode; true of every vector, the Davenport--Heilbronn vector included. -/ def p20043 := And.intro @FRC.Chart.chi_inversion (And.intro @FRC.Chart.chi_shift (And.intro @FRC.HorizonML.scale_shift (And.intro @FRC.HorizonML.readout_on_line (@FRC.HorizonML.readout_slot_index)))) set_option linter.defProp false in /-- p20044 — 20:E13. Shell-basis completeness is not a clause of E12: the $\p-1$ complex characters are an orthogonal basis of $\mathbb C^{\Fx{\p}}$ ($\lVert\chi_j\rVert^{2}=\p-1$; finite Parseval), true of every vector, the trivial character carrying the mean $\psi(\p-1)/(\p-1)$; the $\Fp$-valued power characters are never orthonormal and do not expand $v$; completeness for the zero set of $\zeta$ is D5, a different clause. -/ def p20044 := And.intro @FRC.Chart.chi_orthogonal (And.intro @FRC.Chart.chi_parseval (And.intro @FRC.Chart.chi_inversion (@FRC.HorizonML.power_characters_not_orthonormal))) /-- p20047 — 20:F1. \textbf{Turing's count on the shell.} On every cell $C_y\le N^{\mathrm{crit}}_y\le\mathcal N_y$ (A7); the cell is clean when $\mathcal N_y=N^{\mathrm{crit}}_y$, and $C_y=\mathcal N_y$ certifies it, every zero simple. The shell estimates $\mathcal N$ by the comb count (Appendix~\ref{app:comb}; uncertified) and reads $C$ from the main sum's sign changes (A10), zeros on the line. An off-line zero is a phantom, $\mathcal N_y-N^{\mathrm{crit}}_y>0$. -/ theorem p20047 : ∀ {a b : ℝ}, a < b → (completedRiemannZeta ((1 / 2 : ℂ) + ↑a * Complex.I)).re * (completedRiemannZeta ((1 / 2 : ℂ) + ↑b * Complex.I)).re < (0 : ℝ) → ∃ t, a < t ∧ t < b ∧ riemannZeta ((1 / 2 : ℂ) + ↑t * Complex.I) = (0 : ℂ) := @FRC.Chart.zero_of_sign_change set_option linter.defProp false in /-- p20080 — 20:D8. The strip: the Euler product excludes zeros with real part at least one, and the functional equation confines the nontrivial zeros to the open strip in Klein-four orbits of size two on the line and four off it; the Davenport--Heilbronn vector, without the product, is not multiplicative and has an off-line zero. No core witness: the statement is analytic. -/ def p20080 := @FRC.Chart.zeros_in_strip set_option linter.defProp false in /-- p21016 — 21:C1. The linearised dynamics is the gradient flow of a coherence free energy --- its current derived from the pair tally conditional on channel unity (Lemma~\ref{lem:pairtally}) --- and a locked cluster of cardinality $m$ couples with coefficient exactly $m$. -/ def p21016 := @FRC.Strong.locked_sum /-- p21019 — 21:C4. The equivalence principle as an identity; the bias field is clock rate, giving the redshift $\Delta f/f=Gm/rc^2$; the turnaround radius against the Hubble drive. -/ theorem p21019 : ∀ (u : ℝ), (0 : ℝ) ≤ u → u ≤ (1 : ℝ) → |(1 : ℝ) - Real.exp (-u) - u| ≤ u ^ (2 : ℕ) := @FRC.Strong.redshift_linear /-- p21020 — 21:C5. The magnitude $G=\hbar c/m_P^2$, frame-covariant (a relativity principle for scale); gravity's weakness is cardinality dilution. -/ theorem p21020 : (∀ (S : ℕ) [Fact (Nat.Prime ((4 : ℕ) * S + (1 : ℕ)))], ∃ r, r ^ (2 : ℕ) = ↑S ∧ ((2 : ZMod ((4 : ℕ) * S + (1 : ℕ))) * r) ^ (2 : ℕ) = (-1 : ZMod ((4 : ℕ) * S + (1 : ℕ)))) ∧ ∀ (m Ω : ℝ), (0 : ℝ) < Ω → (m / √Ω) ^ (2 : ℕ) = m ^ (2 : ℕ) / Ω := And.intro @FRC.GravML.hbar_register (@FRC.Strong.dilution) /-- p21022 — 21:C7. Channel unity forces the spatial bias to equal the temporal one, $\gamma=1$, restoring the full light deflection $4Gm/c^2b$. -/ theorem p21022 : (∀ (β γ : ℚ), (((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) = (2 : ℚ) ↔ (2 : ℚ) * γ - β = (1 : ℚ)) ∧ ((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) - (2 : ℚ) = (2 / 3 : ℚ) * ((2 : ℚ) * γ - β - (1 : ℚ)) ∧ (γ = (1 : ℚ) → ((1 : ℚ) + γ) / (2 : ℚ) = (1 : ℚ) ∧ ((2 : ℚ) * γ - β = (1 : ℚ) → β = (1 : ℚ) ∧ ((2 : ℚ) + (2 : ℚ) * γ - β) / (3 : ℚ) = (1 : ℚ)))) ∧ ∀ (U : ℝ), |U| ≤ (1 / 2 : ℝ) → |Real.exp (-((2 : ℝ) * U)) - (((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ^ (2 : ℕ) - U ^ (3 : ℕ) / (6 : ℝ)| ≤ (3 : ℝ) * U ^ (4 : ℕ) ∧ |Real.exp ((2 : ℝ) * U) - ((1 : ℝ) + U / (2 : ℝ)) ^ (4 : ℕ) - U ^ (2 : ℕ) / (2 : ℝ)| ≤ (3 : ℝ) * |U| ^ (3 : ℕ) := And.intro @FRC.GravML.cover_forcing (@FRC.Strong.pn_series) /-- p21023 — 21:C8. The exponential isotropic metric by multiplicative composition, with $\beta=\gamma=1$: deflection, Shapiro delay, and perihelion at their observed values. -/ theorem p21023 : (∀ (β γ : ℚ), (((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) = (2 : ℚ) ↔ (2 : ℚ) * γ - β = (1 : ℚ)) ∧ ((2 : ℚ) - β + (2 : ℚ) * γ) / (3 / 2 : ℚ) - (2 : ℚ) = (2 / 3 : ℚ) * ((2 : ℚ) * γ - β - (1 : ℚ)) ∧ (γ = (1 : ℚ) → ((1 : ℚ) + γ) / (2 : ℚ) = (1 : ℚ) ∧ ((2 : ℚ) * γ - β = (1 : ℚ) → β = (1 : ℚ) ∧ ((2 : ℚ) + (2 : ℚ) * γ - β) / (3 : ℚ) = (1 : ℚ)))) ∧ ∀ (U : ℝ), |U| ≤ (1 / 2 : ℝ) → |Real.exp (-((2 : ℝ) * U)) - (((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ^ (2 : ℕ) - U ^ (3 : ℕ) / (6 : ℝ)| ≤ (3 : ℝ) * U ^ (4 : ℕ) ∧ |Real.exp ((2 : ℝ) * U) - ((1 : ℝ) + U / (2 : ℝ)) ^ (4 : ℕ) - U ^ (2 : ℕ) / (2 : ℝ)| ≤ (3 : ℝ) * |U| ^ (3 : ℕ) := And.intro @FRC.GravML.cover_forcing (@FRC.Strong.pn_series) /-- p21026 — 21:C11. The nonlinear completion forced: the exact cut-flux law (transfer antisymmetry) plus the winding grading forbid independent static self-sourcing, the clock-comparison cocycle makes the exponential reading unique (exactly the character $\gen^{-\Delta n}$, $e^{-u}$ its observer lift), and Deser's bootstrap does not apply because what gravitates is winding rate. -/ theorem p21026 : ∀ (a b : ℝ), Real.exp (-(a + b)) = Real.exp (-a) * Real.exp (-b) ∧ (∀ (U : ℝ), (-2 : ℝ) < U → U < (2 : ℝ) → Real.exp (-((2 : ℝ) * Real.artanh (U / (2 : ℝ)))) = ((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ∧ ((1 : ℝ) - (1 / 2 : ℝ)) / ((1 : ℝ) + (1 / 2 : ℝ)) ≠ (((1 : ℝ) - (1 / 2 : ℝ) / (2 : ℝ)) / ((1 : ℝ) + (1 / 2 : ℝ) / (2 : ℝ))) ^ (2 : ℕ) := @FRC.Strong.exponential_reading /-- p21027 — 21:C12. The exact saturating static profile and its slip core at $r_*=\sqrt{Gm}$: horizonless, operationally black at $r_f=r_s/\ln\Omega$ --- the exact statement the cut form, $4\pi r^{2}$ its [chart] reading; the $r_f$-anchored claims stated in the substrate coordinate, $r_*(\ln\Omega/2)^{2}$ Planck masses (master E10). -/ theorem p21027 : ∀ (M L Ω : ℝ), (0 : ℝ) < M → (0 : ℝ) < L → L = Real.log Ω → (0 : ℝ) < Ω → Real.exp ((2 : ℝ) * M / ((2 : ℝ) * M / L)) = Ω ∧ (√M < (2 : ℝ) * M / L ↔ (L / (2 : ℝ)) ^ (2 : ℕ) < M) ∧ ((2 : ℝ) * M / L < M ↔ (2 : ℝ) < L) := @FRC.Strong.operational_cut /-- p21030 — 21:C15. The radiative sector: the quarter-turn conjugate momentum makes the dynamics a wave equation: two helicity-$\pm2$ gravitons at speed $c$, quadrupole radiation; gauge leaves two polarisations. -/ theorem p21030 : ∀ (k : ℝ), (2 : ℝ) - (2 : ℝ) * Real.cos k = (4 : ℝ) * Real.sin (k / (2 : ℝ)) ^ (2 : ℕ) := @FRC.Strong.dispersion_symbol /-- p21033 — 21:C18. The primordial spectrum: $n_s=1$ the scale-dilation fixed point; the tilt's committed form $-\pi^{2}/\ln\Omega$, $\ln\Omega$ the e-fold count of the frame's scale range, the realisation of master L8, with the measured tilt its falsifier ($\tfrac12\ln\Omega$ excluded at $8.2\sigma$; the linearity condition undefined on a shell); the wrapped chart fixing the low large-angle power. -/ theorem p21033 : (∀ (n : ℝ), (∀ (k : ℝ), (0 : ℝ) < k → k ^ (3 : ℕ) * k ^ n = (1 : ℝ)) ↔ n = (-3 : ℝ)) ∧ 3481e-5 < Real.pi ^ (2 : ℕ) / 283.5 ∧ Real.pi ^ (2 : ℕ) / 283.5 < 3482e-5 ∧ 68e-3 * 42e-4 < 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 ∧ 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 < 69e-3 * 42e-4 ∧ 8.2 * 42e-4 < Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 ∧ Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 < 8.25 * 42e-4 := And.intro @FRC.Strong.scale_invariance_iff (@FRC.Chart.tilt_ledger) /-- p21042 — 21:X2. \textbf{No dark-matter particle.} The radial acceleration relation is a registration crossover of the resolution floor, not evidence for undetected mass: galactic dynamics require no dark sector beyond the floor already fixed by $\Omega$. -/ theorem p21042 : Filter.Tendsto (fun t => t / ((1 : ℝ) - Real.exp (-t))) (nhdsWithin (0 : ℝ) (Set.Ioi (0 : ℝ))) (nhds (1 : ℝ)) := @FRC.Strong.crossover_deep_limit /-- p21048 — 21:X8. \textbf{The weakness of gravity} is cardinality dilution, not a hierarchy to be tuned. -/ theorem p21048 : ∀ (m Ω : ℝ), (0 : ℝ) < Ω → (m / √Ω) ^ (2 : ℕ) = m ^ (2 : ℕ) / Ω := @FRC.Strong.dilution /-- p21049 — 21:P1. Strong-field signatures at or outside the photon sphere: shadow $+4.6\%$, eikonal ringdown $-4.4\%$ (the $(2,2,0)$ reading open, GW250114 the exposure; master E13, E14), ISCO frequency $-6.9\%$ with accretion efficiency $5.48\%$ (against $5.72\%$): one origin, jointly falsifiable, conditional on Theorem~\ref{thm:branch}'s inputs alone. -/ theorem p21049 : (∀ (Gm r : ℝ), (0 : ℝ) < Gm → (0 : ℝ) < r → (2 : ℝ) * Real.exp (1 : ℝ) * Gm ≤ r * Real.exp ((2 : ℝ) * Gm / r) ∧ (r * Real.exp ((2 : ℝ) * Gm / r) = (2 : ℝ) * Real.exp (1 : ℝ) * Gm ↔ r = (2 : ℝ) * Gm)) ∧ (1.0462 < (2 : ℝ) * Real.exp (1 : ℝ) / ((3 : ℝ) * √(3 : ℝ)) ∧ (2 : ℝ) * Real.exp (1 : ℝ) / ((3 : ℝ) * √(3 : ℝ)) < 1.0463 ∧ 0.9557 < (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ)) ∧ (3 : ℝ) * √(3 : ℝ) / ((2 : ℝ) * Real.exp (1 : ℝ)) < 0.9558 ∧ 2.46 < ((4 : ℝ) * Real.exp (1 : ℝ) - (6 : ℝ) * √(3 : ℝ)) * 5.12 ∧ ((4 : ℝ) * Real.exp (1 : ℝ) - (6 : ℝ) * √(3 : ℝ)) * 5.12 < 2.47) ∧ (∀ (r : ℝ), (2 : ℝ) < r → HasDerivAt (fun r => (2 : ℝ) / r + (2 : ℝ) * Real.log r - Real.log (r - (2 : ℝ))) ((r ^ (2 : ℕ) - (6 : ℝ) * r + (4 : ℝ)) / (r ^ (2 : ℕ) * (r - (2 : ℝ)))) r ∧ ((3 : ℝ) + √(5 : ℝ)) ^ (2 : ℕ) - (6 : ℝ) * ((3 : ℝ) + √(5 : ℝ)) + (4 : ℝ) = (0 : ℝ) ∧ (2 : ℝ) < (3 : ℝ) + √(5 : ℝ) ∧ ((3 : ℝ) + √(5 : ℝ) - (1 : ℝ)) / ((3 : ℝ) + √(5 : ℝ) - (2 : ℝ)) = ((3 : ℝ) + √(5 : ℝ)) / (4 : ℝ)) ∧ 547e-4 < (1 : ℝ) - √(Real.exp (-((2 : ℝ) / ((3 : ℝ) + √(5 : ℝ)))) * ((3 : ℝ) + √(5 : ℝ)) / (4 : ℝ)) ∧ (1 : ℝ) - √(Real.exp (-((2 : ℝ) / ((3 : ℝ) + √(5 : ℝ)))) * ((3 : ℝ) + √(5 : ℝ)) / (4 : ℝ)) < 548e-4 ∧ 571e-4 < (1 : ℝ) - √(8 / 9 : ℝ) ∧ (1 : ℝ) - √(8 / 9 : ℝ) < 572e-4 := And.intro @FRC.Strong.photon_sphere (And.intro @FRC.Strong.shadow_bracket (And.intro @FRC.Strong.isco (@FRC.Strong.isco_efficiency))) /-- p21050 — 21:P7. Floor-surface signatures: no prompt echoes (the exact profile horizonless with no reflecting surface, C12; the round-trip delay to $r_f$ carrying $e^{2u(r_f)}=\Omega$) and no evaporation bursts; a reported echo detection at the stated precision falsifies the construction. -/ theorem p21050 : ∀ (M L Ω : ℝ), (0 : ℝ) < M → (0 : ℝ) < L → L = Real.log Ω → (0 : ℝ) < Ω → Real.exp ((2 : ℝ) * M / ((2 : ℝ) * M / L)) = Ω ∧ (√M < (2 : ℝ) * M / L ↔ (L / (2 : ℝ)) ^ (2 : ℕ) < M) ∧ ((2 : ℝ) * M / L < M ↔ (2 : ℝ) < L) := @FRC.Strong.operational_cut /-- p21051 — 21:P2. Preferred-frame effects at $O(1/\sqrt\Omega)=O(10^{-62})$ ($3\times10^{-62}$ at $\Omega=1.3\times10^{123}$): the drive's in-principle signature, far below current $10^{-5}$ bounds. -/ theorem p21051 : 27e-63 < (1 : ℝ) / √13e122 ∧ (1 : ℝ) / √13e122 < 28e-63 := @FRC.Strong.preferred_frame_scale /-- p21052 — 21:P3. The weak-acceleration floor $a_0=cH_0/2\pi=1.04\times10^{-10}\,\mathrm{m\,s^{-2}}$ at the entailed $H_0=67.4$ \cite{entropy}, against the fitted $1.20\pm0.24\times10^{-10}$: $13\%$ low, $0.7\sigma$ of the systematic-dominated error, no free parameter; the $2\pi$ the dictionary's full cycle (14:B2), the one-cycle-per-period threshold the realisation 32:B3 with its discrete falsifier. -/ theorem p21052 : ∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67 := @FRC.Chart.floor_value /-- p21053 — 21:P4. The radial acceleration relation, $g_{\mathrm{obs}}=g_N/(1-e^{-\sqrt{g_N/a_0}})$, no fitted function beyond the barrier identification (B9), the form the data selected across the four observed acceleration decades, its approach to Newton the discriminant ($0.05$ at $g_N\approx5a_0$ against the simple rational interpolant); the deep limit gives the baryonic Tully--Fisher relation $v^4=GMa_0$. -/ theorem p21053 : (∀ (t : ℝ), (0 : ℝ) < t → (0 : ℝ) < (1 : ℝ) - Real.exp (-t) ∧ (1 : ℝ) ≤ t / ((1 : ℝ) - Real.exp (-t)) ∧ (t ≤ (1 : ℝ) → t / ((1 : ℝ) - Real.exp (-t)) ≤ (1 : ℝ) / ((1 : ℝ) - (3 : ℝ) * t / (4 : ℝ))) ∧ ∀ (G M r a₀ v : ℝ), (0 : ℝ) < r → (0 : ℝ) ≤ G * M → (0 : ℝ) ≤ a₀ → v ^ (2 : ℕ) = √(G * M / r ^ (2 : ℕ) * a₀) * r → v ^ (4 : ℕ) = G * M * a₀) ∧ Filter.Tendsto (fun t => (1 : ℝ) - Real.exp (-t)) Filter.atTop (nhds (1 : ℝ)) ∧ (∀ (w : ℝ), (0 : ℝ) < w → w < (1 : ℝ) → w * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) ^ (2 : ℕ) - (2 : ℝ) * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) + w = (0 : ℝ) ∧ (0 : ℝ) < ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w < (1 : ℝ) ∧ (1 : ℝ) < ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ∀ (x : ℝ), w * x ^ (2 : ℕ) - (2 : ℝ) * x + w = (0 : ℝ) → x = ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∨ x = ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w) ∧ 1.11966 < (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 1.11967 ∧ 1.17082 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) < 1.17083 ∧ 511e-4 < (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) ∧ (1 / 2 : ℝ) + √((1 / 4 : ℝ) + (1 / 5 : ℝ)) - (1 : ℝ) / ((1 : ℝ) - Real.exp (-√(5 : ℝ))) < 512e-4 := And.intro @FRC.Strong.crossover_limits (And.intro @FRC.Strong.crossover_newton_limit (And.intro @FRC.Strong.registration_root (@FRC.Strong.interpolant_discriminant))) /-- p21054 — 21:P5. The floor tracks the expansion, $a_0(z)\propto H(z)$ (BTFR zero-point $\propto E(z)^{1/4}$); high-$z$ rotation curves decisive. -/ theorem p21054 : ∀ (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < M → (0 : ℝ) < H (0 : ℝ) → (0 : ℝ) < H z → (∀ (z : ℝ), a z = c * H z / ((2 : ℝ) * Real.pi)) → (0 : ℝ) < v (0 : ℝ) → (0 : ℝ) < v z → (∀ (z : ℝ), v z ^ (4 : ℕ) = G * M * a z) → a z / a (0 : ℝ) = H z / H (0 : ℝ) ∧ v z / v (0 : ℝ) = (H z / H (0 : ℝ)) ^ (1 / 4 : ℝ) := @FRC.Chart.running_floor /-- p21055 — 21:P6. The 2PN periastron excess $\delta\dot\omega/\dot\omega\approx1.5\times10^{-6}$ for PSR~J0737$-$3039, today degenerate with the mass refit; decisive either way once an independent observable fixes $M_{\mathrm{tot}}$ at $10^{-6}$. Independent of the coherent-fraction falsifier of \citep{quantum}; the ledger carries both. -/ theorem p21055 : ∀ (U : ℝ), |U| ≤ (1 / 2 : ℝ) → |Real.exp (-((2 : ℝ) * U)) - (((1 : ℝ) - U / (2 : ℝ)) / ((1 : ℝ) + U / (2 : ℝ))) ^ (2 : ℕ) - U ^ (3 : ℕ) / (6 : ℝ)| ≤ (3 : ℝ) * U ^ (4 : ℕ) ∧ |Real.exp ((2 : ℝ) * U) - ((1 : ℝ) + U / (2 : ℝ)) ^ (4 : ℕ) - U ^ (2 : ℕ) / (2 : ℝ)| ≤ (3 : ℝ) * |U| ^ (3 : ℕ) := @FRC.Strong.pn_series /-- p21060 — 21:P8. The primordial tilt $n_s-1=-\pi^{2}/\ln\Omega=-0.0348$ [approx] at $\ln\Omega=283.5$ (the master's scale import), against Planck 2018 $-0.0351\pm0.0042$ ($+0.07\sigma$); $0.24\%$ per factor two in $S$; the neighbouring count $\tfrac12\ln\Omega$ excluded at $8.2\sigma$. -/ theorem p21060 : 3481e-5 < Real.pi ^ (2 : ℕ) / 283.5 ∧ Real.pi ^ (2 : ℕ) / 283.5 < 3482e-5 ∧ 68e-3 * 42e-4 < 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 ∧ 351e-4 - Real.pi ^ (2 : ℕ) / 283.5 < 69e-3 * 42e-4 ∧ 8.2 * 42e-4 < Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 ∧ Real.pi ^ (2 : ℕ) / (283.5 / (2 : ℝ)) - 351e-4 < 8.25 * 42e-4 := @FRC.Chart.tilt_ledger /-- p21062 — 21:C13. Area-law entropy $S=c_S'A_f/\ell_P^2$: the $\tfrac14$ the $Q_4$ gauge quotient counted on the shell ($S/A=\kap/\p $ exactly), the Carrier identity $S=(\Omega-1)/4$ at the coherence-horizon shell the same quarter (a consistency, not a closure); the count read as the coordinate area at the operational cut (B7); the identification of the entropy with the channel count (master D15); an exact merger area law $\Delta A=2M_1M_2$ on the count face of the mass; a phase-slip (Hawking-scaling) emission suppressed below one quantum per Hubble time. -/ theorem p21062 : (∀ (κ : ℕ), (4 : ℕ) * (κ * ((4 : ℕ) * κ + (2 : ℕ))) + (1 : ℕ) = ((4 : ℕ) * κ + (1 : ℕ)) ^ (2 : ℕ) ∧ κ * ((4 : ℕ) * κ + (2 : ℕ)) * ((4 : ℕ) * κ + (1 : ℕ)) = κ * (((4 : ℕ) * κ + (1 : ℕ)) * ((4 : ℕ) * κ + (2 : ℕ))) ∧ (4 : ℕ) * (κ * ((4 : ℕ) * κ + (2 : ℕ))) * ((4 : ℕ) * κ + (1 : ℕ)) = ((4 : ℕ) * κ + (1 : ℕ)) * ((4 : ℕ) * κ + (2 : ℕ)) * ((4 : ℕ) * κ)) ∧ (∀ (M₁ M₂ δ : ℤ), (M₁ + M₂) * (M₁ + M₂ + (1 : ℤ)) - M₁ * (M₁ + (1 : ℤ)) - M₂ * (M₂ + (1 : ℤ)) = (2 : ℤ) * M₁ * M₂ ∧ (M₁ + M₂ - δ) * (M₁ + M₂ - δ + (1 : ℤ)) - M₁ * (M₁ + (1 : ℤ)) - M₂ * (M₂ + (1 : ℤ)) = (2 : ℤ) * M₁ * M₂ - ((2 : ℤ) * (M₁ + M₂) + (1 : ℤ)) * δ + δ ^ (2 : ℕ) ∧ ((0 : ℤ) ≤ δ → δ ≤ (2 : ℤ) * (M₁ + M₂) + (1 : ℤ) → (M₁ + M₂ - δ) * (M₁ + M₂ - δ + (1 : ℤ)) - M₁ * (M₁ + (1 : ℤ)) - M₂ * (M₂ + (1 : ℤ)) ≤ (2 : ℤ) * M₁ * M₂) ∧ ((27811 : ℤ) + (1596 : ℤ)) * ((27811 : ℤ) + (1596 : ℤ) + (1 : ℤ)) - (27811 : ℤ) * ((27811 : ℤ) + (1 : ℤ)) - (1596 : ℤ) * ((1596 : ℤ) + (1 : ℤ)) = (88772712 : ℤ)) ∧ (∀ (rs L : ℝ), rs ≠ (0 : ℝ) → L ≠ (0 : ℝ) → (rs / L / rs) ^ (2 : ℕ) = (1 : ℝ) / L ^ (2 : ℕ)) ∧ 124e-7 < (1 : ℝ) / 283.5 ^ (2 : ℕ) ∧ (1 : ℝ) / 283.5 ^ (2 : ℕ) < 125e-7 := And.intro @FRC.GravML.count_face (And.intro @FRC.GravML.merger_area_law (And.intro @FRC.Strong.capacity_ratio (@FRC.Strong.capacity_ratio_numeral))) /-- p21064 — 21:C19. The registration crossover made exact: the killed walk is the noise sector, first passage the masking event, the window attribution the framed-rational tally ratio $g_N/f$, and the orbital response now derived (Theorem~\ref{thm:twoshift} with the registered-inertia identity); it rests on the masking barrier (B9) and the corpus's unified sampling clause (master D10), shared with \citep{quantum}. -/ theorem p21064 : (∀ (w : ℝ), (0 : ℝ) < w → w < (1 : ℝ) → w * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) ^ (2 : ℕ) - (2 : ℝ) * (((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w) + w = (0 : ℝ) ∧ (0 : ℝ) < ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w < (1 : ℝ) ∧ (1 : ℝ) < ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w ∧ ∀ (x : ℝ), w * x ^ (2 : ℕ) - (2 : ℝ) * x + w = (0 : ℝ) → x = ((1 : ℝ) - √((1 : ℝ) - w ^ (2 : ℕ))) / w ∨ x = ((1 : ℝ) + √((1 : ℝ) - w ^ (2 : ℕ))) / w) ∧ (∀ (t : ℝ), (0 : ℝ) < t → (0 : ℝ) < (1 : ℝ) - Real.exp (-t) ∧ (1 : ℝ) ≤ t / ((1 : ℝ) - Real.exp (-t)) ∧ (t ≤ (1 : ℝ) → t / ((1 : ℝ) - Real.exp (-t)) ≤ (1 : ℝ) / ((1 : ℝ) - (3 : ℝ) * t / (4 : ℝ))) ∧ ∀ (G M r a₀ v : ℝ), (0 : ℝ) < r → (0 : ℝ) ≤ G * M → (0 : ℝ) ≤ a₀ → v ^ (2 : ℕ) = √(G * M / r ^ (2 : ℕ) * a₀) * r → v ^ (4 : ℕ) = G * M * a₀) ∧ Filter.Tendsto (fun t => t / ((1 : ℝ) - Real.exp (-t))) (nhdsWithin (0 : ℝ) (Set.Ioi (0 : ℝ))) (nhds (1 : ℝ)) := And.intro @FRC.Strong.registration_root (And.intro @FRC.Strong.crossover_limits (@FRC.Strong.crossover_deep_limit)) set_option linter.defProp false in /-- p22005 — 22:A5. The window discipline, committed: the coherence horizon $\sqrt\Omega$, the decidability horizon $\Omega^{1/4}$, and the committed cardinality $\Omega\sim1.3\times10^{123}$ [chart] (the corpus's scale import, master A7) --- declared inputs of the programme, their cost recorded in the $\Omega$ ledger. -/ def p22005 := @FRC.Chart.omega_floors /-- p22033 — 22:C17. Exact Tsirelson saturation: the singlet law $E(\Delta)=\cos(\pi\Delta/40)$ [chart], $S=2(\zeta_8+\zeta_8^{-1})$, $S^2=8$, the exhaustive $80^3$ sweep never exceeding it [chart]; no-signalling and the composite reduction commute. -/ theorem p22033 : (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ)) ∧ ∀ (Δ : ℕ), (Complex.exp (↑((2 : ℝ) * Real.pi * ↑Δ / (80 : ℝ)) * Complex.I)).re = Real.cos (Real.pi * ↑Δ / (40 : ℝ)) := And.intro @FRC.Chart.tsirelson_real (@FRC.Chart.singlet_law) /-- p22035 — 22:C19. The gravitational channel entangles exactly, $C^2=\sin^2(\varphi/2)$ [chart], with the pure-channel complementarity $V^2+C^2=1$. -/ theorem p22035 : (∀ (φ : ℝ), (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) + Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / (2 : ℂ) = ↑(Real.cos (φ / (2 : ℝ))) ∧ (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) - Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / ((2 : ℂ) * Complex.I) = ↑(Real.sin (φ / (2 : ℝ))) ∧ Real.cos (φ / (2 : ℝ)) ^ (2 : ℕ) + Real.sin (φ / (2 : ℝ)) ^ (2 : ℕ) = (1 : ℝ) ∧ Real.sin (0 / 2 : ℝ) = (0 : ℝ)) ∧ ∀ (φ : ℝ), (0 : ℝ) < φ → φ < (2 : ℝ) * Real.pi → Real.sin (φ / (2 : ℝ)) ≠ (0 : ℝ) := And.intro @FRC.Chart.channel_chart (@FRC.Chart.channel_entangles) /-- p22041 — 22:C25. The measurement problem dissolved: Kochen--Specker poses no separate threat because values exist only as Subject-relative quotient phases, carried together with the Tsirelson strength $2\sqrt2$ [chart]. -/ theorem p22041 : FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ) := @FRC.Chart.tsirelson_real /-- p22050 — 22:X7. \textbf{The Tsirelson boundary} is attained as a ring identity, $S=2(\zeta_8+\zeta_8^{-1})=2\sqrt2$ [chart], so a relational finite substrate carries full quantum correlation strength, not merely quantum vocabulary. -/ theorem p22050 : FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ) := @FRC.Chart.tsirelson_real /-- p22052 — 22:P1. Gravitationally induced entanglement at exactly the Newtonian rate [chart], $V^2+C^2=1$ on the pure channel: equal force but unequal entanglement --- a source gravitates by its full mass while the systematic conditional phase, the calibrated discriminator, is carried by the coherent sectors alone, the fully incoherent channel separable at generic (nondegenerate) geometry. The one dated forward prediction. -/ theorem p22052 : ∀ (φ : ℝ), (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) + Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / (2 : ℂ) = ↑(Real.cos (φ / (2 : ℝ))) ∧ (Complex.exp (↑(φ / (2 : ℝ)) * Complex.I) - Complex.exp (-(↑(φ / (2 : ℝ)) * Complex.I))) / ((2 : ℂ) * Complex.I) = ↑(Real.sin (φ / (2 : ℝ))) ∧ Real.cos (φ / (2 : ℝ)) ^ (2 : ℕ) + Real.sin (φ / (2 : ℝ)) ^ (2 : ℕ) = (1 : ℝ) ∧ Real.sin (0 / 2 : ℝ) = (0 : ℝ) := @FRC.Chart.channel_chart /-- p22054 — 22:P3. The Tsirelson value $S=2\sqrt2$ exact [chart] and the network behaviour of complex (not real) quantum theory: vacuum dispersion, $S\neq2\sqrt2$, or non-quantum network behaviour each falsify. -/ theorem p22054 : FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹ = ↑√(2 : ℝ) ∧ (2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹) = ↑((2 : ℝ) * √(2 : ℝ)) ∧ ((2 : ℂ) * (FRC.Chart.zeta8 + FRC.Chart.zeta8⁻¹)) ^ (2 : ℕ) = (8 : ℂ) := @FRC.Chart.tsirelson_real /-- p22056 — 22:P5. Quantum computation succeeds as standard quantum mechanics prescribes at every accessible depth; the first deviation, if any, is quantised at the unit-core ceiling $k^*=408$ ($204$ for $\sqrt\Omega$) [chart], not gradual. -/ theorem p22056 : (∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → (2 : ℝ) ^ (408 : ℕ) < Ω ∧ Ω / (4 : ℝ) < (2 : ℝ) ^ (408 : ℕ) ∧ (2 : ℝ) ^ (204 : ℕ) < √Ω ∧ √Ω / (4 : ℝ) < (2 : ℝ) ^ (204 : ℕ)) ∧ ∀ (m : ℕ), ¬(2 : GaussianInt) ∣ FRC.QuantumML.gi ^ m * FRC.QuantumML.onePlusI := And.intro @FRC.Chart.ceiling_bracket (@FRC.QuantumML.gaussian_minimal) set_option linter.defProp false in /-- p22061 — 22:Z2. The committed $\Omega$ anchor and the binding floor: the carrier scale is fixed by the verified Riemann height through $\Omega^{1/4}$ [chart], and a single off-line zero below $\Omega^{1/4}$ falsifies from a desk. -/ def p22061 := @FRC.Chart.omega_floors set_option linter.defProp false in /-- p26010 — 26:B4. The continuum reading [chart]: the dilation generator $\HH=-\mathrm i(x\partial_x+\tfrac12)$ has $x^{-1/2+\mathrm i\nu}$ as eigenfunction of eigenvalue $\nu$ on $x>0$, so the frequency index is the spectrum of $\HH$ in the chart of the scale shift (20:E1). -/ def p26010 := @FRC.Chart.dilation_eigen /-- p26011 — 26:B5. The Gauss sum couples the two turns: multiplication by a unit permutes the units; $\sum_{t\neq0}\psi(tc)$ is $-1$ for $c\neq0$ and $P-1$ for $c=0$; $\sum_u\chi(u)=0$ for $\chi\neq1$; hence $\lvert g(\chi)\rvert^{2}=P$ for every nontrivial $\chi$ on the shell ($\Om$ on the Carrier). -/ theorem p26011 : (∀ {F : Type u_1} [Field F] [Fintype F] {R' : Type u_2} [CommRing R'] [IsDomain R'] {χ : MulChar F R'}, χ ≠ (1 : MulChar F R') → ∀ {ψ : AddChar F R'}, ψ.IsPrimitive → gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card F)) ∧ ∀ {F : Type u_3} [Field F] [Fintype F] {χ : MulChar F ℂ}, χ ≠ (1 : MulChar F ℂ) → ∀ {ψ : AddChar F ℂ}, ψ.IsPrimitive → gaussSum χ ψ * star (gaussSum χ ψ) = ↑(Fintype.card F) ∧ Complex.normSq (gaussSum χ ψ) = ↑(Fintype.card F) := And.intro @FRC.HorizonML.gauss_product (@FRC.Chart.gauss_modulus) /-- p26013 — 26:C2. The family's size and the table beyond the horizon [chart]: at the anchor $2^{204}<\sqrt\Om<2^{205}$, so the shells of the family $P^{2}<\Om$ have at most $205$ bits; $2^{102}<\Om^{1/4}<2^{103}$, so a decision table with one entry per $204$-bit input exceeds the absolute horizon and lies below $\sqrt\Om$. -/ theorem p26013 : ∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → (2 : ℝ) ^ (204 : ℕ) < √Ω ∧ √Ω < (2 : ℝ) ^ (205 : ℕ) ∧ (2 : ℝ) ^ (102 : ℕ) < √√Ω ∧ √√Ω < (2 : ℝ) ^ (103 : ℕ) := @FRC.Chart.family_bits /-- p27013 — 27:C1. 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). -/ theorem 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 : ℂ)) := And.intro @FRC.FieldsML.roots_inclusion (@FRC.FieldsML.wilson_weight_nonneg) /-- p27018 — 27:C6. 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. -/ theorem 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 : ℕ)) := @FRC.FieldsML.fermi_constant /-- p27019 — 27:C7. 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$). -/ theorem 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 : ℝ) := @FRC.FieldsML.area_law_positive /-- p27030 — 27:X7. \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. -/ theorem 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 : ℝ) := @FRC.FieldsML.area_law_positive /-- p27037 — 27:P3. \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. -/ theorem 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 : ℕ) := @FRC.FieldsML.running_near_miss /-- p27038 — 27:P4. \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. -/ theorem 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 : ℕ) := @FRC.FieldsML.proton_lifetime /-- p27039 — 27:P5. \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. -/ theorem 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 : ℚ) := @FRC.FieldsML.seesaw_band /-- p38010 — 38:B2. The radial ladder: shells at $R\sin(2a\pi/13)$ [chart]; capacity $4a<\p\Leftrightarrow a\le\kap$. -/ theorem p38010 : ∀ (R : ℝ), (0 : ℝ) < R → (0 : ℝ) < R * Real.sin ((2 : ℝ) * Real.pi / (13 : ℝ)) ∧ R * Real.sin ((2 : ℝ) * Real.pi / (13 : ℝ)) < R * Real.sin ((4 : ℝ) * Real.pi / (13 : ℝ)) ∧ R * Real.sin ((4 : ℝ) * Real.pi / (13 : ℝ)) < R * Real.sin ((6 : ℝ) * Real.pi / (13 : ℝ)) ∧ R * Real.sin ((6 : ℝ) * Real.pi / (13 : ℝ)) < R := @FRC.Chart.ladder_monotone /-- p38048 — 38:X3. \textbf{The acceleration floor $a_{0}=cH_{0}/2\pi$ is the drive seen in the chart}: the leak's cyclic rate is the drive's own, one cycle per drive period $\Om-1$ chronons $=2\pi/H_{0}$, and its acceleration face is the floor (C10; C11, the realisation); at the instance $a_{0}=c/(\Om-1)$. -/ theorem p38048 : ∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67 := @FRC.Chart.floor_value /-- p38049 — 38:P1. The registration floor $a_{0}=cH_{0}/2\pi$, read from the pair's $\kap$-free per-chronon leak rate (C11): parameter-free, tracking $H(z)$. Falsifier: a measured floor off $cH_{0}/2\pi$ beyond the $H_{0}$ uncertainty, or one not tracking $H(z)$ (\S\ref{sec:predictions}, item 5; the dark sector's L1). -/ theorem p38049 : (∀ (c H0 : ℝ), c = (299792458 : ℝ) → H0 = 674e2 / 30856775814913673e6 → 104e-12 < c * H0 / ((2 : ℝ) * Real.pi) ∧ c * H0 / ((2 : ℝ) * Real.pi) < 105e-12 ∧ 0.868 < c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 ∧ c * H0 / ((2 : ℝ) * Real.pi) / 12e-11 < 0.870 ∧ 0.65 < (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 ∧ (12e-11 - c * H0 / ((2 : ℝ) * Real.pi)) / 24e-12 < 0.67) ∧ ∀ (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ), (0 : ℝ) < c → (0 : ℝ) < G → (0 : ℝ) < M → (0 : ℝ) < H (0 : ℝ) → (0 : ℝ) < H z → (∀ (z : ℝ), a z = c * H z / ((2 : ℝ) * Real.pi)) → (0 : ℝ) < v (0 : ℝ) → (0 : ℝ) < v z → (∀ (z : ℝ), v z ^ (4 : ℕ) = G * M * a z) → a z / a (0 : ℝ) = H z / H (0 : ℝ) ∧ v z / v (0 : ℝ) = (H z / H (0 : ℝ)) ^ (1 / 4 : ℝ) := And.intro @FRC.Chart.floor_value (@FRC.Chart.running_floor) -- end keys end FRC.LedgerML /-! FrcLedger/Pnp.lean -/ /-! # 26-pnp — the paper module on Mathlib: the Gauss-sum modulus and the chart rows under the paper's name (16 October 2026) Rows of the predicate ledger of *P versus NP: Computation as Counting over Finite Relational Substrate* (tree `26-pnp-20260614`) whose content is read on the Gauss sum or against the continuum: the Gauss-sum product `g(χ)·g(χ⁻¹, ψ⁻¹) = p` (B5) in `FrcLedger/Theme/Horizon.lean` (`FRC.HorizonML`) and its modulus `|g(χ)|² = p` over the complex numbers (B5) in `FrcLedger/Theme/Chart.lean`; the family's bit length and the decision table beyond the absolute horizon at the scale import's anchor (C2) and the dilation generator's eigenfunction (B4) in `FrcLedger/Theme/Chart.lean` (`FRC.Chart`, the chart theme, where the reals live). Every name here is an alias; the exact content of the paper is the core's (`FrcCore/Pnp.lean` and the themes it cites). -/ namespace FRC.Pnp open Real /-! ## Old names (16 October 2026): every declaration of this module is an alias of a theme's (`FRC.HorizonML`, `FRC.Chart`), under the paper's name -/ /-- 26:B5 — the Gauss-sum product on a finite field into any domain (`FRC.HorizonML.gauss_product`, `Theme/Horizon.lean`). -/ theorem gauss_product {F : Type*} [Field F] [Fintype F] {R' : Type*} [CommRing R'] [IsDomain R'] {χ : MulChar F R'} (hχ : χ ≠ 1) {ψ : AddChar F R'} (hψ : ψ.IsPrimitive) : gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card F := FRC.HorizonML.gauss_product hχ hψ /-- 26:B5 — the Gauss-sum modulus over the complex numbers (`FRC.Chart.gauss_modulus`, `Theme/Chart.lean`). -/ theorem gauss_modulus {F : Type*} [Field F] [Fintype F] {χ : MulChar F ℂ} (hχ : χ ≠ 1) {ψ : AddChar F ℂ} (hψ : ψ.IsPrimitive) : gaussSum χ ψ * star (gaussSum χ ψ) = Fintype.card F ∧ Complex.normSq (gaussSum χ ψ) = Fintype.card F := FRC.Chart.gauss_modulus hχ hψ /-- 26:C2 [chart] — the family's bits and the table beyond the horizon (`FRC.Chart.family_bits`, `Theme/Chart.lean`). -/ theorem family_bits (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35) (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) : (2 : ℝ) ^ 204 < √Ω ∧ √Ω < (2 : ℝ) ^ 205 ∧ (2 : ℝ) ^ 102 < √(√Ω) ∧ √(√Ω) < (2 : ℝ) ^ 103 := FRC.Chart.family_bits Λ ℓP r S Ω hΛ hℓ hr2 hS hΩ /-- 26:B4 [chart] — the dilation generator's eigenfunction (`FRC.Chart.dilation_eigen`, `Theme/Chart.lean`). -/ theorem dilation_eigen (ν x : ℝ) (hx : 0 < x) : -Complex.I * ((x : ℂ) * deriv (fun t : ℝ => (t : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν)) x + (1 / 2 : ℂ) * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν)) = ν * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν) := FRC.Chart.dilation_eigen ν x hx -- Ledger predicates of 26-pnp (generated by make_predicates.py from docs/26-pnp/26-pnp-ledger.json; edit the ledger, not this section) set_option linter.defProp false in /-- 26:B4 (p26010) — The continuum reading [chart]: the dilation generator $\HH=-\mathrm i(x\partial_x+\tfrac12)$ has $x^{-1/2+\mathrm i\nu}$ as eigenfunction of eigenvalue $\nu$ on $x>0$, so the frequency index is the spectrum of $\HH$ in the chart of the scale shift (20:E1). -/ def p26010 := @FRC.LedgerML.p26010 /-- 26:B5 (p26011) — The Gauss sum couples the two turns: multiplication by a unit permutes the units; $\sum_{t\neq0}\psi(tc)$ is $-1$ for $c\neq0$ and $P-1$ for $c=0$; $\sum_u\chi(u)=0$ for $\chi\neq1$; hence $\lvert g(\chi)\rvert^{2}=P$ for every nontrivial $\chi$ on the shell ($\Om$ on the Carrier). -/ theorem p26011 : (∀ {F : Type u_1} [Field F] [Fintype F] {R' : Type u_2} [CommRing R'] [IsDomain R'] {χ : MulChar F R'}, χ ≠ (1 : MulChar F R') → ∀ {ψ : AddChar F R'}, ψ.IsPrimitive → gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card F)) ∧ ∀ {F : Type u_3} [Field F] [Fintype F] {χ : MulChar F ℂ}, χ ≠ (1 : MulChar F ℂ) → ∀ {ψ : AddChar F ℂ}, ψ.IsPrimitive → gaussSum χ ψ * star (gaussSum χ ψ) = ↑(Fintype.card F) ∧ Complex.normSq (gaussSum χ ψ) = ↑(Fintype.card F) := @FRC.LedgerML.p26011 /-- 26:C2 (p26013) — The family's size and the table beyond the horizon [chart]: at the anchor $2^{204}<\sqrt\Om<2^{205}$, so the shells of the family $P^{2}<\Om$ have at most $205$ bits; $2^{102}<\Om^{1/4}<2^{103}$, so a decision table with one entry per $204$-bit input exceeds the absolute horizon and lies below $\sqrt\Om$. -/ theorem p26013 : ∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → (2 : ℝ) ^ (204 : ℕ) < √Ω ∧ √Ω < (2 : ℝ) ^ (205 : ℕ) ∧ (2 : ℝ) ^ (102 : ℕ) < √√Ω ∧ √√Ω < (2 : ℝ) ^ (103 : ℕ) := @FRC.LedgerML.p26013 -- end ledger predicates end FRC.Pnp -- Ledger predicates: axioms (each predicate's, computed here) #print axioms FRC.Pnp.p26010 #print axioms FRC.Pnp.p26011 #print axioms FRC.Pnp.p26013