import Mathlib /-! Generated by `lean/make_web.py` from `FrcLedger/Theme.Fields.lean` with `FrcLedger/Theme/Horizon`, `FrcLedger/Theme/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 /-! FrcLedger/Theme.Fields.lean -/ /-! # 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