Theme/Chart.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Horizon34/-!5# FrcLedger.Theme.Chart — the chart theme: the readings against the continuum (ledger migration, task LM30)67The chart theme holds the readings of the finite results against the continuum, the only theme with the reals8(`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,9`ln_omega_ledger`), its cosmology and prediction rows: the10floor `a₀ = cH₀/2π` (00:L1), the octant record depth and its outputs (00:L3), the primordial tilt (00:L8) and the11running floor (00:P1). The chart's numerals — the speed of light, the megaparsec, the Julian year, the fitted12values and their errors — are declared data. The octant's theorems moved here from 14-entropy and the floor's13from 21-gravity (6 October 2026); those modules keep the old names as aliases.1415Classical (tier 2) on Mathlib's hierarchy. Every bracket is certified from `π` to six places (`Real.pi_gt_d6`,16`Real.pi_lt_d6`), `e` to nine (`Real.exp_one_gt_d9`, `Real.exp_one_lt_d9`) and the Taylor tail of `exp`17(`Real.exp_bound`, `Real.exp_bound'`). The realisation content behind each reading — that the octant is the18record depth, that the floor is the synchronisation threshold, that `ln Ω` is the tilt's e-fold count — is the19rows' realisation clause, not formal content.20-/2122namespace FRC.Chart2324open Real2526/-! ## The scale import's chart numerals (00:A7; 14:A1, C1) -/27section scale2829/-- 00:A7 [chart] — the scale import's numerals: with the fit's `Λ = 1.088 × 10⁻⁵² m⁻²` (Planck 2018) and the Planck30length `ℓ_P = 1.616255 × 10⁻³⁵ m` declared [data], the de Sitter radius `r_H = c/H_Λ`, `r_H² = 3/Λ`, gives31`S = π (r_H/ℓ_P)²` between `3.31` and `3.32 × 10¹²²` (the row's `3.3 × 10¹²²`) and `Ω = 4S + 1` between `1.32` and32`1.33 × 10¹²³` (the row's `1.3 × 10¹²³`). That the datum fixes the cardinality is the import; nothing here derives the33datum. -/34theorem scale_import (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35)35    (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) :36    (3.31e122 : ℝ) < S ∧ S < 3.32e122 ∧ (1.32e123 : ℝ) < Ω ∧ Ω < 1.33e123 := by37  have hpi1 := Real.pi_gt_d638  have hpi2 := Real.pi_lt_d639  have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by40    rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp41  subst hΛ hℓ42  have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity43  have hSlo : (3.3160599e122 : ℝ) < S := by44    rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith45  have hShi : S < (3.3160611e122 : ℝ) := by46    rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith47  subst hΩ48  refine ⟨by linarith, by linarith, by linarith, by linarith⟩4950set_option exponentiation.threshold 512 in51/-- 00:L8 [chart] — the ledger's `ln Ω = 283.5`, the numeral the tilt reads, derived from the scale import: with the52same `Λ`, `ℓ_P`, `r_H² = 3/Λ`, `S = π (r_H/ℓ_P)²` and `Ω = 4S + 1`, `ln Ω` lies between `283.50` and `283.51`. The53logarithm is bracketed by `409 ln 2` (`Real.log_two_gt_d9`, `log_two_lt_d9`) and `1 − 1/m ≤ ln m ≤ m − 1` on the54mantissa `m = Ω/2⁴⁰⁹`. -/55theorem ln_omega_ledger (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35)56    (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) :57    (283.50 : ℝ) < Real.log Ω ∧ Real.log Ω < 283.51 := by58  have hpi1 := Real.pi_gt_d659  have hpi2 := Real.pi_lt_d660  have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by61    rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp62  subst hΛ hℓ63  have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity64  have hSlo : (3.3160599e122 : ℝ) < S := by65    rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith66  have hShi : S < (3.3160611e122 : ℝ) := by67    rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith68  subst hΩ69  have hΩpos : (0 : ℝ) < 4 * S + 1 := by linarith70  have hmpos : (0 : ℝ) < (4 * S + 1) / 2 ^ 409 := by positivity71  have hlog : Real.log (4 * S + 1) = 409 * Real.log 2 + Real.log ((4 * S + 1) / 2 ^ 409) := by72    have e : (4 * S + 1 : ℝ) = 2 ^ 409 * ((4 * S + 1) / 2 ^ 409) := by field_simp73    conv_lhs => rw [e]74    rw [Real.log_mul (by positivity) (by positivity), Real.log_pow]; push_cast; ring75  have hl1 := Real.log_two_gt_d976  have hl2 := Real.log_two_lt_d977  have hm1 : (1.0032614 : ℝ) < (4 * S + 1) / 2 ^ 409 := by78    rw [lt_div_iff₀ (by positivity)]; norm_num; linarith79  have hm2 : (4 * S + 1) / 2 ^ 409 < (1.0032619 : ℝ) := by80    rw [div_lt_iff₀ (by positivity)]; norm_num; linarith81  have hup := Real.log_le_sub_one_of_pos hmpos82  have hlo := Real.one_sub_inv_le_log_of_pos hmpos83  have hinv : 1 / ((4 * S + 1) / 2 ^ 409) < 1 / (1.0032614 : ℝ) := one_div_lt_one_div_of_lt (by norm_num) hm184  rw [inv_eq_one_div] at hlo85  have hA : (0.00325 : ℝ) < Real.log ((4 * S + 1) / 2 ^ 409) := by86    have : (1 : ℝ) - 1 / 1.0032614 > 0.00325 := by norm_num87    linarith88  have hB : Real.log ((4 * S + 1) / 2 ^ 409) < (0.003262 : ℝ) := by linarith89  rw [hlog]90  exact ⟨by linarith, by linarith⟩9192set_option exponentiation.threshold 512 in93/-- 22:C14, P5 [chart] — **the granularity ceiling at the anchor**: with the scale import's `Ω = 4S + 1`94(`S = π (r_H/ℓ_P)²`, the same hypotheses as `scale_import`), `2⁴⁰⁸ < Ω` and `Ω/4 < 2⁴⁰⁸`, so the largest depth `k`95with `T(k) = 2^{k + [k odd]} < Ω` is `k* = 408` (the odd `409` would need `4 · 2⁴⁰⁸ < Ω`); and `2²⁰⁴ < √Ω`,96`√Ω/4 < 2²⁰⁴`, so at the coherence horizon `k* = 204`. Every quantity compared is below `Ω`. -/97theorem ceiling_bracket (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35)98    (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) :99    (2 : ℝ) ^ 408 < Ω ∧ Ω / 4 < (2 : ℝ) ^ 408 ∧ (2 : ℝ) ^ 204 < √Ω ∧ √Ω / 4 < (2 : ℝ) ^ 204 := by100  have hpi1 := Real.pi_gt_d6101  have hpi2 := Real.pi_lt_d6102  have hK : S = π * (3 / (Λ * ℓP ^ 2)) := by103    rw [hS, div_pow, hr2]; subst hΛ hℓ; field_simp104  subst hΛ hℓ105  have hKpos : (0 : ℝ) < 3 / (1.088e-52 * (1.616255e-35) ^ 2) := by positivity106  have hSlo : (3.3160599e122 : ℝ) < S := by107    rw [hK]; have := mul_lt_mul_of_pos_right hpi1 hKpos; norm_num at this ⊢; linarith108  have hShi : S < (3.3160611e122 : ℝ) := by109    rw [hK]; have := mul_lt_mul_of_pos_right hpi2 hKpos; norm_num at this ⊢; linarith110  subst hΩ111  have h1 : (2 : ℝ) ^ 408 < 4 * S + 1 := by norm_num; linarith112  have h2 : (4 * S + 1) / 4 < (2 : ℝ) ^ 408 := by norm_num; linarith113  have hΩpos : (0 : ℝ) < 4 * S + 1 := by linarith114  refine ⟨h1, h2, ?_, ?_⟩115  · rw [Real.lt_sqrt (by positivity)]116    calc ((2 : ℝ) ^ 204) ^ 2 = 2 ^ 408 := by norm_num117      _ < 4 * S + 1 := h1118  · have hsq : (√(4 * S + 1) / 4) ^ 2 < ((2 : ℝ) ^ 204) ^ 2 := by119      rw [div_pow, Real.sq_sqrt (le_of_lt hΩpos)]120      calc (4 * S + 1) / 4 ^ 2 = (4 * S + 1) / 4 / 4 := by ring121        _ < (2 : ℝ) ^ 408 / 4 := by122            exact div_lt_div_of_pos_right h2 (by norm_num)123        _ < (2 : ℝ) ^ 408 := by124            have : (0 : ℝ) < 2 ^ 408 := by positivity125            linarith126        _ = ((2 : ℝ) ^ 204) ^ 2 := by norm_num127    exact lt_of_pow_lt_pow_left₀ 2 (by positivity) hsq128129/-- 22:A5, Z2 [chart] — **the Ω ledger's floors**: every null channel's floor lies below the anchor — the Riemann130height `(3 × 10¹²)⁴ = 8.1 × 10⁴⁹` (the binding floor, through the decidability horizon `Ω^{1/4}`), the Sorkin and131Born tallies `10²²` (one floor, cited twice by the paper's ledger file), the granularity `2⁶⁰` — with the same hypotheses132as `scale_import`. -/133theorem omega_floors (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35)134    (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) :135    (3e12 : ℝ) ^ 4 = 8.1e49 ∧ (3e12 : ℝ) ^ 4 < Ω ∧ (1e22 : ℝ) < Ω ∧ (2 : ℝ) ^ 60 < Ω := by136  obtain ⟨-, -, hlo, -⟩ := scale_import Λ ℓP r S Ω hΛ hℓ hr2 hS hΩ137  refine ⟨by norm_num, ?_, ?_, ?_⟩ <;> norm_num <;> linarith138139end scale140141/-! ## 22-quantum: the Tsirelson value, the singlet law and the channel against the continuum (22:C17, X7, P3, C25;142C19, P1; 15 October 2026) -/143section quantum144145/-- The primitive eighth root `ζ₈ = e^{iπ/4}`. -/146noncomputable def zeta8 : ℂ := Complex.exp ((π / 4 : ℝ) * Complex.I)147148theorem zeta8_pow_four : zeta8 ^ 4 = -1 := by149  unfold zeta8150  rw [← Complex.exp_nat_mul]151  have : (4 : ℕ) * ((π / 4 : ℝ) * Complex.I) = (π : ℂ) * Complex.I := by push_cast; ring152  rw [this, Complex.exp_pi_mul_I]153154theorem zeta8_inv : zeta8⁻¹ = Complex.exp (-((π / 4 : ℝ) * Complex.I)) := by155  unfold zeta8; rw [← Complex.exp_neg]156157/-- 22:C17, X7, P3, C25 — **the Tsirelson value is `2√2`**: `ζ₈ + ζ₈⁻¹ = 2 cos(π/4) = √2`, so `S = 2(ζ₈ + ζ₈⁻¹) = 2√2`158as a real number and `S² = 8`. -/159theorem tsirelson_real :160    zeta8 + zeta8⁻¹ = (Real.sqrt 2 : ℂ) ∧ 2 * (zeta8 + zeta8⁻¹) = (2 * Real.sqrt 2 : ℝ) ∧161    (2 * (zeta8 + zeta8⁻¹)) ^ 2 = 8 := by162  have hcos : zeta8 + zeta8⁻¹ = 2 * Complex.cos ((π / 4 : ℝ) : ℂ) := by163    rw [zeta8_inv, Complex.two_cos, neg_mul]; rfl164  have hval : zeta8 + zeta8⁻¹ = (Real.sqrt 2 : ℂ) := by165    rw [hcos, ← Complex.ofReal_cos, Real.cos_pi_div_four]166    push_cast; ring167  refine ⟨hval, ?_, ?_⟩168  · rw [hval]; push_cast; ring169  · rw [hval]170    have : ((Real.sqrt 2 : ℝ) : ℂ) ^ 2 = 2 := by171      rw [← Complex.ofReal_pow, Real.sq_sqrt (by norm_num)]; push_cast; ring172    calc (2 * (Real.sqrt 2 : ℂ)) ^ 2 = 4 * ((Real.sqrt 2 : ℝ) : ℂ) ^ 2 := by ring173      _ = 8 := by rw [this]; norm_num174175/-- 22:C17 — the singlet law: the correlator at `Δ` setting steps is the real part of `ζ₈₀^Δ = e^{2πiΔ/80}`,176`E(Δ) = cos(πΔ/40)`. -/177theorem singlet_law (Δ : ℕ) :178    (Complex.exp ((2 * π * Δ / 80 : ℝ) * Complex.I)).re = Real.cos (π * Δ / 40) := by179  rw [Complex.exp_ofReal_mul_I_re]180  congr 1181  ring182183/-- 22:C19, P1 — the channel's chart: with the branch phase `φ`, the visibility `V = (x + x⁻¹)/2 = cos(φ/2)` and the184concurrence `C = (x − x⁻¹)/(2i) = sin(φ/2)` for `x = e^{iφ/2}`, so `V² + C² = 1` and `C² = sin²(φ/2)`; at `φ = 0`185the concurrence vanishes. -/186theorem channel_chart (φ : ℝ) :187    (Complex.exp ((φ / 2 : ℝ) * Complex.I) + Complex.exp (-((φ / 2 : ℝ) * Complex.I))) / 2 =188      (Real.cos (φ / 2) : ℂ) ∧189    (Complex.exp ((φ / 2 : ℝ) * Complex.I) - Complex.exp (-((φ / 2 : ℝ) * Complex.I))) / (2 * Complex.I) =190      (Real.sin (φ / 2) : ℂ) ∧191    Real.cos (φ / 2) ^ 2 + Real.sin (φ / 2) ^ 2 = 1 ∧ Real.sin (0 / 2) = 0 := by192  refine ⟨?_, ?_, Real.cos_sq_add_sin_sq _, by simp⟩193  · rw [Complex.ofReal_cos, Complex.cos, neg_mul]194  · rw [Complex.ofReal_sin, Complex.sin, neg_mul]195    have hI : Complex.I ≠ 0 := Complex.I_ne_zero196    field_simp197    linear_combination (Complex.exp ((φ / 2 : ℝ) * Complex.I) - Complex.exp (-((φ / 2 : ℝ) * Complex.I))) * Complex.I_sq198199/-- 22:C19 — the channel entangles: off the trivial phase, `0 < φ < 2π`, the concurrence `C = sin(φ/2)` is not zero. -/200theorem channel_entangles (φ : ℝ) (h0 : 0 < φ) (h1 : φ < 2 * π) : Real.sin (φ / 2) ≠ 0 :=201  ne_of_gt (Real.sin_pos_of_pos_of_lt_pi (by linarith) (by linarith))202203end quantum204205/-! ## 26-pnp: the carrier family, the table beyond the horizon and the dilation generator (26:C2, B4) -/206207section pnp208209set_option exponentiation.threshold 512 in210/-- 26:C2 [chart] — **the family's size and the table beyond the horizon**: with the scale import's `Ω = 4S + 1` (the211hypotheses of `scale_import`), `2²⁰⁴ < √Ω < 2²⁰⁵`, so the shells of the family `P² < Ω` have at most `205` bits, and212`2¹⁰² < Ω^{1/4} < 2¹⁰³`, so a decision table with one entry per input of `204` bits has `2²⁰⁴` entries, below `√Ω` and213beyond the absolute horizon `Ω^{1/4}` by more than `2¹⁰¹`. No numeral formed exceeds `Ω` (the largest is `2⁴⁰⁸`). -/214theorem family_bits (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35)215    (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) :216    (2 : ℝ) ^ 204 < √Ω ∧ √Ω < (2 : ℝ) ^ 205 ∧ (2 : ℝ) ^ 102 < √(√Ω) ∧ √(√Ω) < (2 : ℝ) ^ 103 := by217  obtain ⟨h1, h2, h3, -⟩ := ceiling_bracket Λ ℓP r S Ω hΛ hℓ hr2 hS hΩ218  have hΩpos : (0 : ℝ) < Ω := lt_trans (by positivity) h1219  -- `√Ω / 2 = √(Ω / 4) < 2²⁰⁴` from `Ω / 4 < 2⁴⁰⁸ = (2²⁰⁴)²`: the largest numeral formed is `2⁴⁰⁸ < Ω` (the G18 round of220  -- 16 October 2026: the first proof bounded `Ω` by a power of two above it, a numeral the corpus does not form)221  have hhalf : √Ω / 2 < (2 : ℝ) ^ 204 := by222    have e : √Ω / 2 = √(Ω / 4) := by223      rw [Real.sqrt_div' _ (by norm_num : (0 : ℝ) ≤ 4), show √(4 : ℝ) = 2 by224        rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.sqrt_sq (by norm_num)]]225    rw [e, Real.sqrt_lt' (by positivity)]226    calc Ω / 4 < (2 : ℝ) ^ 408 := h2227      _ = ((2 : ℝ) ^ 204) ^ 2 := by norm_num228  have h5 : √Ω < (2 : ℝ) ^ 205 := by229    have : (2 : ℝ) ^ 205 = 2 * 2 ^ 204 := by norm_num230    rw [this]; linarith231  refine ⟨h3, h5, ?_, ?_⟩232  · rw [Real.lt_sqrt (by positivity)]233    calc ((2 : ℝ) ^ 102) ^ 2 = 2 ^ 204 := by norm_num234      _ < √Ω := h3235  · rw [Real.sqrt_lt' (by positivity)]236    calc √Ω < (2 : ℝ) ^ 205 := h5237      _ < ((2 : ℝ) ^ 103) ^ 2 := by norm_num238239/-- 26:B5 — **the Gauss-sum modulus**: over `ℂ`, on a finite field `F`, for a nontrivial multiplicative character `χ`240and a primitive additive character `ψ`, `g(χ⁻¹, ψ⁻¹)` is the complex conjugate of `g(χ, ψ)` (Mathlib's241`star_gaussSum_eq`), so with the horizon theme's `gauss_product`, `g(χ) · conj g(χ) = |g(χ)|² = |F|`: on the prime242shell `𝔽_P`, `P`. -/243theorem gauss_modulus {F : Type*} [Field F] [Fintype F] {χ : MulChar F ℂ} (hχ : χ ≠ 1) {ψ : AddChar F ℂ}244    (hψ : ψ.IsPrimitive) :245    gaussSum χ ψ * star (gaussSum χ ψ) = Fintype.card F ∧ Complex.normSq (gaussSum χ ψ) = Fintype.card F := by246  have h := FRC.HorizonML.gauss_product hχ hψ247  rw [← star_gaussSum_eq] at h248  refine ⟨h, ?_⟩249  have h2 : (Complex.normSq (gaussSum χ ψ) : ℂ) = (Fintype.card F : ℂ) := by rw [← Complex.mul_conj, ← h]; rfl250  exact_mod_cast h2251252/-- 26:B4 [chart] — **the dilation generator**: `Ĥ = −i(x ∂ₓ + ½)` has `x^{−1/2 + iν}` as eigenfunction of eigenvalue253`ν` on `x > 0`; the frequency index is the spectrum of `Ĥ` in the continuum reading of the scale shift (20:E1). -/254theorem dilation_eigen (ν x : ℝ) (hx : 0 < x) :255    -Complex.I * ((x : ℂ) * deriv (fun t : ℝ => (t : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν)) x256      + (1 / 2 : ℂ) * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν))257      = ν * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν) := by258  set s : ℂ := -(1 / 2 : ℂ) + Complex.I * ν with hs259  have hx0 : (x : ℂ) ≠ 0 := by exact_mod_cast hx.ne'260  have hslit : (x : ℂ) ∈ Complex.slitPlane := Complex.ofReal_mem_slitPlane.2 hx261  have hd : HasDerivAt (fun t : ℝ => (t : ℂ) ^ s) (s * (x : ℂ) ^ (s - 1)) x :=262    (Complex.hasStrictDerivAt_cpow_const hslit).hasDerivAt.comp_ofReal263  rw [hd.deriv]264  have hpow : (x : ℂ) * (x : ℂ) ^ (s - 1) = (x : ℂ) ^ s := by265    rw [Complex.cpow_sub _ _ hx0, Complex.cpow_one, mul_div_cancel₀ _ hx0]266  have hcoef : -Complex.I * (s + 1 / 2) = ν := by267    rw [hs]; ring_nf; rw [Complex.I_sq]; ring268  calc -Complex.I * ((x : ℂ) * (s * (x : ℂ) ^ (s - 1)) + (1 / 2 : ℂ) * (x : ℂ) ^ s)269      = -Complex.I * (s + 1 / 2) * (x : ℂ) ^ s := by rw [← hpow]; ring270    _ = ν * (x : ℂ) ^ s := by rw [hcoef]271272end pnp273274/-! ## The octant record depth and its outputs (00:L3; 14:C5, C7, P3) -/275section octant276277/-- 00:L3, 14:C5 [chart] — the chart conversion of the octant: the count `S/2` out of the `4S`-cycle, read on278the meridian circle `2π r_H/c`, is the depth `(π/4) r_H/c`. -/279theorem octant_chart (S r c : ℝ) (hS : S ≠ 0) :280    (S / 2) / (4 * S) * (2 * π * r / c) = (π / 4) * r / c := by281  rcases eq_or_ne c 0 with rfl | hc282  · simp283  · field_simp284285/-- The octant's rate factor `tanh(3π/8)` is positive. -/286theorem tanh_octant_pos : 0 < tanh (3 * π / 8) := by287  rw [Real.tanh_eq_sinh_div_cosh]288  exact div_pos (Real.sinh_pos_iff.2 (by positivity)) (Real.cosh_pos _)289290/-- 00:L3, 14:P3 [ΛCDM] — the algebraic locus: with `t H_Λ = π/4` (the octant), `H_Λ = H₀ √Ω_Λ` and291`Ω_Λ = tanh²(3π/8)`, `t H₀ = (π/4)/tanh(3π/8)`; the numeral `0.950` is bracketed in `locus_bracket`. -/292theorem age_rate_locus (t H0 HΛ Ω : ℝ) (hoct : t * HΛ = π / 4) (hΛ : HΛ = H0 * √Ω)293    (hΩ : Ω = tanh (3 * π / 8) ^ 2) : t * H0 = (π / 4) / tanh (3 * π / 8) := by294  have hpos := tanh_octant_pos295  rw [hΩ, Real.sqrt_sq hpos.le] at hΛ296  rw [eq_div_iff hpos.ne', ← hoct, hΛ]; ring297298/-- 00:L3, 14:A8 [ΛCDM] — the rival chart's age identity as the import it is: in flat matter-plus-`Λ` the product of299the age and the asymptotic rate is `t₀H_Λ = (2/3) artanh √Ω_Λ`, a function of the one fitted parameter; outside300`[0, 1)` the value is junk. Moved here from 14-entropy (task LM30's repair, 7 October 2026), which keeps the name. -/301noncomputable def lcdmAge (Ω : ℝ) : ℝ := 2 / 3 * artanh (√Ω)302303/-- 00:L3, 14:C7, 14:X3 [ΛCDM] — the octant inversion: the rival chart's identity gives `t₀H_Λ = π/4` at304`Ω_Λ = tanh²(3π/8)` and, for `0 ≤ Ω_Λ < 1`, only there. Moved here from 14-entropy, which keeps the name. -/305theorem octant_inversion :306    lcdmAge (tanh (3 * π / 8) ^ 2) = π / 4 ∧307    ∀ Ω : ℝ, 0 ≤ Ω → Ω < 1 → lcdmAge Ω = π / 4 → Ω = tanh (3 * π / 8) ^ 2 := by308  have hpos := tanh_octant_pos309  constructor310  · unfold lcdmAge311    rw [Real.sqrt_sq hpos.le, Real.artanh_tanh]; ring312  · intro Ω h0 h1 h313    unfold lcdmAge at h314    have hart : artanh (√Ω) = 3 * π / 8 := by linarith315    have hΩ : √Ω ∈ Set.Ioo (-1 : ℝ) 1 := by316      refine ⟨by linarith [Real.sqrt_nonneg Ω], ?_⟩317      rw [Real.sqrt_lt' one_pos]; simpa using h1318    have := Real.tanh_artanh hΩ319    rw [hart] at this320    rw [this, Real.sq_sqrt h0]321322/-- `tanh x = (e^{2x} − 1)/(e^{2x} + 1)`. -/323theorem tanh_eq_exp_two_mul (x : ℝ) : tanh x = (exp (2 * x) - 1) / (exp (2 * x) + 1) := by324  rw [Real.tanh_eq, Real.exp_neg, two_mul, Real.exp_add]325  have h := Real.exp_pos x326  field_simp327328/-- The Taylor brackets of `e^t` at the two ends of `t = 3π/4 − 2`: seven terms of the series with the tail329bound of Mathlib's `Real.exp_bound`. -/330theorem exp_tail_bounds :331    (1.427884 : ℝ) < exp 0.356194 ∧ exp (0.35619475 : ℝ) < 1.4278857 := by332  constructor333  · have h := abs_le.1 (Real.exp_bound (x := 0.356194) (by rw [abs_of_pos (by norm_num)]; norm_num)334      (n := 7) (by norm_num))335    rw [abs_of_pos (by norm_num : (0 : ℝ) < 0.356194)] at h336    have h1 := h.1337    norm_num [Finset.sum_range_succ, Nat.factorial] at h1 ⊢338    linarith339  · have h := Real.exp_bound' (x := 0.35619475) (by norm_num) (by norm_num) (n := 7) (by norm_num)340    norm_num [Finset.sum_range_succ, Nat.factorial] at h ⊢341    linarith342343/-- `e^{3π/4}` bracketed: `10.55071 < e^{3π/4} < 10.55073`, from `π` to six places, `e` to nine, and the344Taylor tail. -/345theorem exp_three_pi_four_bounds : (10.55071 : ℝ) < exp (3 * π / 4) ∧ exp (3 * π / 4) < 10.55073 := by346  have hpi1 := Real.pi_gt_d6347  have hpi2 := Real.pi_lt_d6348  have he1 := Real.exp_one_gt_d9349  have he2 := Real.exp_one_lt_d9350  have ht := exp_tail_bounds351  have hsplit : exp (3 * π / 4) = exp 1 * exp 1 * exp (3 * π / 4 - 2) := by352    rw [← Real.exp_add, ← Real.exp_add]; congr 1; ring353  have hlo : exp 0.356194 < exp (3 * π / 4 - 2) := Real.exp_lt_exp.2 (by linarith)354  have hhi : exp (3 * π / 4 - 2) < exp 0.35619475 := Real.exp_lt_exp.2 (by linarith)355  have hpos : (0 : ℝ) < exp 1 := Real.exp_pos 1356  rw [hsplit]357  constructor358  · nlinarith [mul_pos hpos hpos, Real.exp_pos (3 * π / 4 - 2)]359  · nlinarith [mul_pos hpos hpos, Real.exp_pos (3 * π / 4 - 2)]360361/-- `tanh(3π/8)` bracketed: `0.82685 < tanh(3π/8) < 0.826851`, from `exp_three_pi_four_bounds`. -/362theorem tanh_octant_bounds : (0.82685 : ℝ) < tanh (3 * π / 8) ∧ tanh (3 * π / 8) < 0.826851 := by363  obtain ⟨hE1, hE2⟩ := exp_three_pi_four_bounds364  have htanh : tanh (3 * π / 8) = (exp (3 * π / 4) - 1) / (exp (3 * π / 4) + 1) := by365    rw [tanh_eq_exp_two_mul]; congr 2 <;> ring_nf366  have hden : (0 : ℝ) < exp (3 * π / 4) + 1 := by linarith367  constructor368  · rw [htanh, lt_div_iff₀ hden]; linarith369  · rw [htanh, div_lt_iff₀ hden]; linarith370371/-- 00:L3, 14:P3 — the locus's numeral bracketed: `0.9498 < (π/4)/tanh(3π/8) < 0.9499`, the paper's `0.950`. -/372theorem locus_bracket : (0.9498 : ℝ) < (π / 4) / tanh (3 * π / 8) ∧ (π / 4) / tanh (3 * π / 8) < 0.9499 := by373  obtain ⟨hl, hu⟩ := tanh_octant_bounds374  have hpi1 := Real.pi_gt_d6375  have hpi2 := Real.pi_lt_d6376  have hpos : (0 : ℝ) < tanh (3 * π / 8) := by linarith377  constructor378  · rw [lt_div_iff₀ hpos]; nlinarith379  · rw [div_lt_iff₀ hpos]; nlinarith380381/-- The locus to six places: `0.949866 < (π/4)/tanh(3π/8) < 0.949868`, for the rates read on it. -/382theorem locus_fine : (0.949866 : ℝ) < (π / 4) / tanh (3 * π / 8) ∧ (π / 4) / tanh (3 * π / 8) < 0.949868 := by383  obtain ⟨hl, hu⟩ := tanh_octant_bounds384  have hpi1 := Real.pi_gt_d6385  have hpi2 := Real.pi_lt_d6386  have hpos : (0 : ℝ) < tanh (3 * π / 8) := by linarith387  constructor388  · rw [lt_div_iff₀ hpos]; nlinarith389  · rw [div_lt_iff₀ hpos]; nlinarith390391/-- 00:L3, 14:C7, 14:X3 — the landing bracketed: `0.68368 < tanh²(3π/8) < 0.68369` (the numeral `0.684`) is392certified from `π` to six places, `e` to nine and the Taylor tail; and, with the Planck numerals393`0.685 ± 0.007` taken as data, the deviation lies between `0.18σ` and `0.19σ`. -/394theorem landing_bracket :395    (0.68368 : ℝ) < tanh (3 * π / 8) ^ 2 ∧ tanh (3 * π / 8) ^ 2 < 0.68369 ∧396    0.18 * 0.007 < 0.685 - tanh (3 * π / 8) ^ 2 ∧ 0.685 - tanh (3 * π / 8) ^ 2 < 0.19 * 0.007 := by397  obtain ⟨hl, hu⟩ := tanh_octant_bounds398  have hsq1 : (0.82685 : ℝ) ^ 2 < tanh (3 * π / 8) ^ 2 := by399    apply pow_lt_pow_left₀ hl (by norm_num) (by norm_num)400  have hsq2 : tanh (3 * π / 8) ^ 2 < (0.826851 : ℝ) ^ 2 := by401    apply pow_lt_pow_left₀ hu (by linarith) (by norm_num)402  norm_num at hsq1 hsq2403  refine ⟨by linarith, by linarith, by linarith, by linarith⟩404405/-- 00:L3 — the deviation fixed to the row's rounded `0.19σ`: between `0.186σ` and `0.19σ` below Planck's406`0.685 ± 0.007` (data). -/407theorem landing_fine :408    0.186 * 0.007 < 0.685 - tanh (3 * π / 8) ^ 2 ∧ 0.685 - tanh (3 * π / 8) ^ 2 < (0.19 * 0.007 : ℝ) := by409  obtain ⟨h1, h2, _, h4⟩ := landing_bracket410  exact ⟨by linarith, h4⟩411412/-- 00:L3 [chart] — the channel-1 consistency: read on the depth `t = 13.79` Gyr (the row's depth numeral, a Julian413year of `365.25` days; data), the locus `t H₀ = (π/4)/tanh(3π/8)` gives `67.35 < H₀ < 67.36` km s⁻¹ Mpc⁻¹ (the414megaparsec `3.0856775814913673 × 10¹⁹` km; data): the channel-1 rate `67.4` to `0.1 %` (14:P3, "a consistency, not a415prediction"). -/416theorem hubble_landing (t H0 : ℝ) (ht : t = 13.79e9 * (365.25 * 86400))417    (hloc : t * H0 = (π / 4) / tanh (3 * π / 8)) :418    (67.35 : ℝ) < H0 * 3.0856775814913673e19 ∧ H0 * 3.0856775814913673e19 < 67.36 := by419  obtain ⟨hl, hu⟩ := locus_fine420  have htpos : (0 : ℝ) < t := by rw [ht]; norm_num421  have hH : H0 = (π / 4) / tanh (3 * π / 8) / t := by422    rw [eq_div_iff htpos.ne', mul_comm, hloc]423  constructor424  · rw [hH, ht, div_mul_eq_mul_div, lt_div_iff₀ (by norm_num)]; nlinarith425  · rw [hH, ht, div_mul_eq_mul_div, div_lt_iff₀ (by norm_num)]; nlinarith426427/-- 00:L3, 14:P3 [chart] — the locus read on the fit-independent stellar age `t★ = 13.61 ± 0.34` Gyr (data; a Julian428year 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,429`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),430errors combined with `±1.7`, lies between `2.40σ` and `2.42σ` above it (the row's `2.4σ`). -/431theorem hubble_stellar (t H0 : ℝ) (ht : t = 13.61e9 * (365.25 * 86400))432    (hloc : t * H0 = (π / 4) / tanh (3 * π / 8)) :433    (68.24 : ℝ) < H0 * 3.0856775814913673e19 ∧ H0 * 3.0856775814913673e19 < 68.25 ∧434    (1.70 : ℝ) < H0 * 3.0856775814913673e19 * (0.34 / 13.61) ∧ H0 * 3.0856775814913673e19 * (0.34 / 13.61) < 1.71 ∧435    (2.40 : ℝ) < (73.0 - H0 * 3.0856775814913673e19) / √(1.7 ^ 2 + 1.0 ^ 2) ∧436    (73.0 - H0 * 3.0856775814913673e19) / √(1.7 ^ 2 + 1.0 ^ 2) < 2.42 := by437  obtain ⟨hl, hu⟩ := locus_fine438  have htpos : (0 : ℝ) < t := by rw [ht]; norm_num439  have hH : H0 = (π / 4) / tanh (3 * π / 8) / t := by440    rw [eq_div_iff htpos.ne', mul_comm, hloc]441  have h1 : (68.24 : ℝ) < H0 * 3.0856775814913673e19 := by442    rw [hH, ht, div_mul_eq_mul_div, lt_div_iff₀ (by norm_num)]; nlinarith443  have h2 : H0 * 3.0856775814913673e19 < (68.25 : ℝ) := by444    rw [hH, ht, div_mul_eq_mul_div, div_lt_iff₀ (by norm_num)]; nlinarith445  have hs1 : (1.9723 : ℝ) < √(1.7 ^ 2 + 1.0 ^ 2) := by446    rw [Real.lt_sqrt (by norm_num)]; norm_num447  have hs2 : √(1.7 ^ 2 + 1.0 ^ 2 : ℝ) < 1.9724 := by448    rw [Real.sqrt_lt' (by norm_num)]; norm_num449  have hspos : (0 : ℝ) < √(1.7 ^ 2 + 1.0 ^ 2) := by linarith450  refine ⟨h1, h2, by nlinarith, by nlinarith, ?_, ?_⟩451  · rw [lt_div_iff₀ hspos]; nlinarith452  · rw [div_lt_iff₀ hspos]; nlinarith453454end octant455456/-! ## The floor and its running (00:L1, P1; 21:P3) -/457section floor458459/-- 00:L1, 21:P3 — the weak-acceleration floor `a₀ = cH₀/2π` at the entailed `H₀ = 67.4 km s⁻¹ Mpc⁻¹` (the460speed of light and the megaparsec declared numerals [data]): `a₀` lies between `1.04` and `1.05 × 10⁻¹⁰ m s⁻²`;461against the fitted `1.20 × 10⁻¹⁰` it is between `13.0 %` and `13.2 %` low, and the deficit is between `0.65` and462`0.67` of the systematic `0.24 × 10⁻¹⁰` (the text's `13 %`, `0.7σ`). -/463theorem floor_value (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) :464    (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.05e-10 ∧465    (0.868 : ℝ) < c * H0 / (2 * π) / 1.2e-10 ∧ c * H0 / (2 * π) / 1.2e-10 < 0.870 ∧466    (0.65 : ℝ) < (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 ∧467    (1.2e-10 - c * H0 / (2 * π)) / 0.24e-10 < 0.67 := by468  have hpi1 := Real.pi_gt_d6469  have hpi2 := Real.pi_lt_d6470  subst hc hH471  have hA : (1.042e-10 : ℝ) < 299792458 * (67.4e3 / 3.0856775814913673e22) / (2 * π) := by472    rw [lt_div_iff₀ (by positivity)]; nlinarith473  have hB : 299792458 * (67.4e3 / 3.0856775814913673e22) / (2 * π) < (1.0423e-10 : ℝ) := by474    rw [div_lt_iff₀ (by positivity)]; nlinarith475  refine ⟨by linarith, by linarith, ?_, ?_, ?_, ?_⟩476  · rw [lt_div_iff₀ (by norm_num)]; linarith477  · rw [div_lt_iff₀ (by norm_num)]; linarith478  · rw [lt_div_iff₀ (by norm_num)]; linarith479  · rw [div_lt_iff₀ (by norm_num)]; linarith480481/-- 00:L1 — the floor fixed to the row's rounded `1.04 × 10⁻¹⁰`: at the channel-1 rate `H₀ = 67.4 km s⁻¹ Mpc⁻¹`,482`1.04 × 10⁻¹⁰ < a₀ < 1.045 × 10⁻¹⁰ m s⁻²`. -/483theorem floor_fine (c H0 : ℝ) (hc : c = 299792458) (hH : H0 = 67.4e3 / 3.0856775814913673e22) :484    (1.04e-10 : ℝ) < c * H0 / (2 * π) ∧ c * H0 / (2 * π) < 1.045e-10 := by485  have hpi1 := Real.pi_gt_d6486  have hpi2 := Real.pi_lt_d6487  subst hc hH488  constructor489  · rw [lt_div_iff₀ (by positivity)]; nlinarith490  · rw [div_lt_iff₀ (by positivity)]; nlinarith491492/-- 00:P1 [chart] — the running floor: if the floor is read at every redshift on the registered rate,493`a₀(z) = cH(z)/2π`, and the deep-regime Tully–Fisher law `v⁴ = G M a₀` holds at fixed baryonic mass `M`, then494`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 are495asked positive at `0` and `z` only. The law `v⁴ = G M a₀` is the deep regime's import. That the floor tracks the496registered rate (the gravity realisation, 00:D5) is the row's realisation clause, not formal content. -/497theorem running_floor (c G M : ℝ) (H a v : ℝ → ℝ) (z : ℝ) (hc : 0 < c) (hG : 0 < G) (hM : 0 < M)498    (h0 : 0 < H 0) (hz : 0 < H z) (ha : ∀ z, a z = c * H z / (2 * π)) (hv0 : 0 < v 0) (hvz : 0 < v z)499    (htf : ∀ z, v z ^ 4 = G * M * a z) :500    a z / a 0 = H z / H 0 ∧ v z / v 0 = (H z / H 0) ^ (1 / 4 : ℝ) := by501  have hpi := Real.pi_pos502  have hratio : a z / a 0 = H z / H 0 := by503    rw [ha z, ha 0]; field_simp504  refine ⟨hratio, ?_⟩505  have ha0 : 0 < a 0 := by rw [ha 0]; positivity506  have h4 : (v z / v 0) ^ 4 = H z / H 0 := by507    rw [div_pow, htf z, htf 0, ← hratio]; field_simp508  rw [← h4, show (1 / 4 : ℝ) = ((4 : ℕ) : ℝ)⁻¹ by norm_num]509  exact (Real.pow_rpow_inv_natCast (div_pos hvz hv0).le (by norm_num)).symm510511end floor512513/-! ## The radial ladder of the minimal pair (38:B2) -/514section ladder515516/-- 38:B2 [chart] — the radial ladder of the sky: the shell radii `R sin(2aπ/13)`, `a = 1, 2, 3`, are positive,517strictly increasing, and inside the rim `R` (the chart flattening of the latitude circles; the capacity `4a < p ⇔ a ≤ κ`518is the core's `FRC.Pair.window`). -/519theorem ladder_monotone (R : ℝ) (hR : 0 < R) :520    0 < R * Real.sin (2 * π / 13) ∧ R * Real.sin (2 * π / 13) < R * Real.sin (4 * π / 13) ∧521    R * Real.sin (4 * π / 13) < R * Real.sin (6 * π / 13) ∧ R * Real.sin (6 * π / 13) < R := by522  have hpi := Real.pi_pos523  have mono : ∀ x y : ℝ, 0 ≤ x → x < y → y ≤ π / 2 → Real.sin x < Real.sin y := fun x y hx hxy hy =>524    Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith) hy hxy525  refine ⟨mul_pos hR (Real.sin_pos_of_pos_of_lt_pi (by positivity) (by linarith)), ?_, ?_, ?_⟩526  · exact mul_lt_mul_of_pos_left (mono _ _ (by positivity) (by linarith) (by linarith)) hR527  · exact mul_lt_mul_of_pos_left (mono _ _ (by positivity) (by linarith) (by linarith)) hR528  · have h := mono (6 * π / 13) (π / 2) (by positivity) (by linarith) le_rfl529    rw [Real.sin_pi_div_two] at h530    calc R * Real.sin (6 * π / 13) < R * 1 := mul_lt_mul_of_pos_left h hR531      _ = R := mul_one R532533end ladder534535/-! ## The primordial tilt (00:L8) -/536section tilt537538/-- 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 magnitude539between `0.03481` and `0.03482` (the row's `−0.0348`); against Planck 2018's `−0.0351 ± 0.0042` (data) the540deviation is between `+0.068σ` and `+0.069σ` (the row's `+0.07σ`); the count `½ ln Ω` gives `−π²/(ln Ω/2)`, off541by between `8.2σ` and `8.25σ` (the row's exclusion at `8.2σ`). That `ln Ω` is the e-fold count of the frame's scale542range is the row's realisation clause, not formal content. -/543theorem tilt_ledger :544    (0.03481 : ℝ) < π ^ 2 / 283.5 ∧ π ^ 2 / 283.5 < 0.03482 ∧545    (0.068 * 0.0042 : ℝ) < 0.0351 - π ^ 2 / 283.5 ∧ 0.0351 - π ^ 2 / 283.5 < 0.069 * 0.0042 ∧546    (8.2 * 0.0042 : ℝ) < π ^ 2 / (283.5 / 2) - 0.0351 ∧ π ^ 2 / (283.5 / 2) - 0.0351 < 8.25 * 0.0042 := by547  have hpi1 := Real.pi_gt_d6548  have hpi2 := Real.pi_lt_d6549  have hsq1 : (3.141592 : ℝ) ^ 2 < π ^ 2 := pow_lt_pow_left₀ hpi1 (by norm_num) (by norm_num)550  have hsq2 : π ^ 2 < (3.141593 : ℝ) ^ 2 := pow_lt_pow_left₀ hpi2 (by linarith) (by norm_num)551  norm_num at hsq1 hsq2552  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩553  · rw [lt_div_iff₀ (by norm_num)]; linarith554  · rw [div_lt_iff₀ (by norm_num)]; linarith555  · have : π ^ 2 / 283.5 < (0.0351 - 0.068 * 0.0042 : ℝ) := by rw [div_lt_iff₀ (by norm_num)]; norm_num; linarith556    linarith557  · have : (0.0351 - 0.069 * 0.0042 : ℝ) < π ^ 2 / 283.5 := by rw [lt_div_iff₀ (by norm_num)]; norm_num; linarith558    linarith559  · have : (8.2 * 0.0042 + 0.0351 : ℝ) < π ^ 2 / (283.5 / 2) := by rw [lt_div_iff₀ (by norm_num)]; norm_num; linarith560    linarith561  · have : π ^ 2 / (283.5 / 2) < (8.25 * 0.0042 + 0.0351 : ℝ) := by rw [div_lt_iff₀ (by norm_num)]; norm_num; linarith562    linarith563564/-- 00:L8 — the e-fold count of the frame's scale range: from `1/√Ω` to `√Ω` the logarithm spans `ln Ω`. -/565theorem efold_count (Ω : ℝ) (hΩ : 0 < Ω) : Real.log (√Ω / (1 / √Ω)) = Real.log Ω := by566  have hs : 0 < √Ω := Real.sqrt_pos.2 hΩ567  have e : √Ω / (1 / √Ω) = Ω := by568    rw [div_div_eq_mul_div, div_one, Real.mul_self_sqrt hΩ.le]569  rw [e]570571end tilt572573/-! ## 20-rh: the complex characters of the cycle, the characters as eigenvectors of the scale-shift, and the von574Mangoldt weight (20:E1, E12, E13, C5, C2; task LM36)575576Moved here from 20-rh's `FrcLedger/Rh.lean` under the same names; that module keeps the old names as aliases. The577exact shell arithmetic of the same rows is the horizon theme's (`Theme/Horizon.lean`, `FRC.HorizonML`). -/578579section characters580581open Complex Finset582583variable {n : ℕ} [NeZero n]584585/-- The `j`-th chart mode of the cycle `C_n`: `χ_j(m) = e^{2πi·jm/n}`. On the shell, `m` is the discrete586logarithm of the residue `g^m` and `n = p − 1`. -/587noncomputable def chi (j m : ZMod n) : ℂ := ZMod.stdAddChar (j * m)588589/-- The coefficient of `v` on the mode `χ_j`: `⟨v, χ_j⟩ = Σ_m v(m) χ_j(m)̄`. -/590noncomputable def coef (v : ZMod n → ℂ) (j : ZMod n) : ℂ := ∑ m, v m * (starRingEnd ℂ) (chi j m)591592lemma chi_conj (j m : ZMod n) : (starRingEnd ℂ) (chi j m) = ZMod.stdAddChar (-(j * m)) := by593  rw [chi, AddChar.map_neg_eq_conj]594595/-- 20:E13 — orthogonality of the chart modes: `Σ_m χ_j(m) χ_k(m)̄ = n·[j = k]`, each of squared norm596`n = p − 1` (with `chi_inversion`, the `p − 1` characters are an orthogonal basis of `ℂ^{F^×}`; the orthonormal597system is `χ_j/√n`). -/598theorem chi_orthogonal (j k : ZMod n) :599    ∑ m, chi j m * (starRingEnd ℂ) (chi k m) = if j = k then (n : ℂ) else 0 := by600  have : ∀ m, chi j m * (starRingEnd ℂ) (chi k m) = ZMod.stdAddChar (m * (j - k)) := fun m => by601    rw [chi_conj, chi, ← AddChar.map_add_eq_mul]602    congr 1; ring603  simp_rw [this]604  rw [AddChar.sum_mulShift _ (ZMod.isPrimitive_stdAddChar n), ZMod.card]605  simp only [sub_eq_zero]606  split_ifs <;> simp607608/-- 20:E12, 20:E1 — clause (iii): the scale-shift `m ↦ m + 1` (the residue `g^m ↦ g^{m+1}`) has every chart mode609as an eigenvector, with eigenphase `e^{2πi·j/n}` independent of the vector: `χ_j(m + 1) = e^{2πi j/n} χ_j(m)`. -/610theorem chi_shift (j m : ZMod n) :611    chi j (m + 1) = ZMod.stdAddChar j * chi j m ∧612    ZMod.stdAddChar (j : ZMod n) = Complex.exp (2 * Real.pi * I * j.val / n) := by613  constructor614  · rw [chi, chi, mul_add, mul_one, AddChar.map_add_eq_mul, mul_comm]615  · rw [ZMod.stdAddChar_apply, ZMod.toCircle_apply]616617/-- 20:E12, 20:E13 — clause (i): Fourier inversion on the cycle, `v = (1/n) Σ_j ⟨v, χ_j⟩ χ_j`, with the constant618mode carrying the mean, `⟨v, χ_0⟩ = Σ_m v(m)`, so the nontrivial modes carry `v − v̄·1`. -/619theorem chi_inversion (v : ZMod n → ℂ) :620    (∀ m, v m = (n : ℂ)⁻¹ * ∑ j, coef v j * chi j m) ∧ coef v 0 = ∑ m, v m ∧621    ∀ m, v m - (n : ℂ)⁻¹ * ∑ m', v m' = (n : ℂ)⁻¹ * ∑ j ∈ univ.erase 0, coef v j * chi j m := by622  have hn : (n : ℂ) ≠ 0 := by exact_mod_cast NeZero.ne n623  have hkey : ∀ m, ∑ j, coef v j * chi j m = (n : ℂ) * v m := by624    intro m625    simp only [coef, sum_mul]626    rw [sum_comm]627    have : ∀ m', ∑ j, v m' * (starRingEnd ℂ) (chi j m') * chi j m628        = v m' * ∑ j, chi j m * (starRingEnd ℂ) (chi j m') := fun m' => by629      rw [mul_sum]; exact sum_congr rfl fun j _ => by ring630    simp_rw [this]631    have horth : ∀ m', ∑ j, chi j m * (starRingEnd ℂ) (chi j m') = if m' = m then (n : ℂ) else 0 := by632      intro m'633      have : ∀ j, chi j m * (starRingEnd ℂ) (chi j m') = ZMod.stdAddChar (j * (m - m')) := fun j => by634        rw [chi_conj, chi, ← AddChar.map_add_eq_mul]635        congr 1; ring636      simp_rw [this]637      rw [AddChar.sum_mulShift _ (ZMod.isPrimitive_stdAddChar n), ZMod.card]638      by_cases h : m' = m639      · subst h; simp640      · rw [ite_eq_right (fun e => h (sub_eq_zero.1 e).symm), ite_eq_right h]; simp641    simp_rw [horth]642    simp [mul_comm]643  have hmean : coef v 0 = ∑ m, v m := by644    simp only [coef, chi, zero_mul, AddChar.map_zero_eq_one, map_one, mul_one]645  refine ⟨fun m => ?_, hmean, fun m => ?_⟩646  · rw [hkey, ← mul_assoc, inv_mul_cancel₀ hn, one_mul]647  · have hsplit := sum_erase_add univ (fun j => coef v j * chi j m) (mem_univ 0)648    rw [hkey] at hsplit649    have h0 : coef v 0 * chi 0 m = ∑ m', v m' := by650      rw [hmean, chi, zero_mul, AddChar.map_zero_eq_one, mul_one]651    rw [h0] at hsplit652    have : ∑ j ∈ univ.erase 0, coef v j * chi j m = (n : ℂ) * v m - ∑ m', v m' := by653      linear_combination hsplit654    rw [this, mul_sub, ← mul_assoc, inv_mul_cancel₀ hn, one_mul]655656/-- 20:E13, 20:C5 — Parseval on the cycle: `Σ_j |⟨v, χ_j⟩|² = n Σ_m |v(m)|²`; the chart modes are complete. -/657theorem chi_parseval (v : ZMod n → ℂ) :658    ∑ j, normSq (coef v j) = n * ∑ m, normSq (v m) := by659  have h := (chi_inversion v).1660  apply Complex.ofReal_injective661  push_cast662  simp_rw [← Complex.mul_conj]663  have hc : ∀ j, (starRingEnd ℂ) (coef v j) = ∑ m, (starRingEnd ℂ) (v m) * chi j m := fun j => by664    simp only [coef, map_sum, map_mul, Complex.conj_conj]665  calc ∑ j, coef v j * (starRingEnd ℂ) (coef v j)666      = ∑ j, ∑ m, (starRingEnd ℂ) (v m) * (coef v j * chi j m) := by667        refine sum_congr rfl fun j _ => ?_668        rw [hc, mul_sum]; exact sum_congr rfl fun m _ => by ring669    _ = ∑ m, (starRingEnd ℂ) (v m) * ∑ j, coef v j * chi j m := by670        rw [sum_comm]; exact sum_congr rfl fun m _ => by rw [mul_sum]671    _ = ∑ m, (starRingEnd ℂ) (v m) * ((n : ℂ) * v m) := by672        refine sum_congr rfl fun m _ => ?_673        congr 1674        have hn : (n : ℂ) ≠ 0 := by exact_mod_cast NeZero.ne n675        have := h m676        rw [this, ← mul_assoc, mul_inv_cancel₀ hn, one_mul]677    _ = (n : ℂ) * ∑ m, v m * (starRingEnd ℂ) (v m) := by678        rw [mul_sum]; exact sum_congr rfl fun m _ => by ring679680/-- 20:C5 — mean-square flatness: for a mean-removed vector `u ≠ 0` on the cycle (`Σ_m u(m) = 0`), the681normalised correlations `r_j = |⟨u, χ_j⟩|/(‖u‖ ‖χ_j‖)` with the nonconstant modes satisfy `Σ_{j≠0} r_j² = 1`682exactly, so their mean square over the `n − 1 = p − 2` nonconstant modes is `1/(p − 2)`: the root-mean-square683correlation is `1/√(p − 2)`. -/684theorem flatness (u : ZMod n → ℂ) (hmean : ∑ m, u m = 0) (hu : u ≠ 0) :685    ∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m)) = 1 ∧686    (∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m))) / ((n : ℝ) - 1) = 1 / ((n : ℝ) - 1) := by687  have hpos : 0 < ∑ m, normSq (u m) := by688    obtain ⟨m, hm⟩ : ∃ m, u m ≠ 0 := by689      by_contra h; push Not at h; exact hu (funext h)690    exact sum_pos' (fun m _ => normSq_nonneg _) ⟨m, mem_univ _, normSq_pos.2 hm⟩691  have hn : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n)692  have hden : (n : ℝ) * ∑ m, normSq (u m) ≠ 0 := (mul_pos hn hpos).ne'693  have h0 : coef u 0 = 0 := by rw [(chi_inversion u).2.1, hmean]694  have hsplit := sum_erase_add univ (fun j => normSq (coef u j)) (mem_univ 0)695  rw [chi_parseval, h0, normSq_zero, add_zero] at hsplit696  have h1 : ∑ j ∈ univ.erase 0, normSq (coef u j) / (n * ∑ m, normSq (u m)) = 1 := by697    rw [← sum_div, hsplit, div_self hden]698  exact ⟨h1, by rw [h1]⟩699700end characters701702section eigen703704/-- 20:E12, 20:E1 — the multiplicative characters of the shell are eigenvectors of the scale-shift in the705abstract reading: `χ(g^r x) = χ(g)^r χ(x)` for every `χ : F^× →* ℂ^×`. -/706theorem character_eigen {F : Type*} [Field F] (χ : Fˣ →* ℂˣ) (g x : Fˣ) (r : ℕ) : χ (g ^ r * x) = χ g ^ r * χ x := by707  rw [map_mul, map_pow]708709end eigen710711/-! ## The resonance: the von Mangoldt weight (row C2) -/712713section resonance714715open ArithmeticFunction Finset716717/-- 20:C2 — `Λ = μ ∗ log` exactly on the divisor lattice: `Λ(n) = Σ_{d ∣ n} μ(d) log(n/d)`; and the support of718`Λ` is the prime powers. (Hardy's limit `R_L → (φ(n)/n) Λ(n)` is the import A3.) -/719theorem vonMangoldt_moebius (m : ℕ) :720    vonMangoldt m = ∑ d ∈ m.divisors, (moebius d : ℝ) * Real.log ((m : ℝ) / d) ∧721    (vonMangoldt m ≠ 0 ↔ IsPrimePow m) := by722  refine ⟨?_, vonMangoldt_ne_zero_iff⟩723  rw [← moebius_mul_log_eq_vonMangoldt, mul_apply,724    Nat.sum_divisorsAntidiagonal (fun a b => (moebius : ArithmeticFunction ℝ) a * ArithmeticFunction.log b)]725  refine sum_congr rfl fun d hd => ?_726  simp only [intCoe_apply, log_apply]727  rw [Nat.cast_div (Nat.dvd_of_mem_divisors hd) (by728    exact_mod_cast (Nat.pos_of_mem_divisors hd).ne')]729730end resonance731732/-! ## The strip (20:D8): the Euler product excludes zeros with real part at least one, and the functional equation733confines the nontrivial zeros to the open strip, in orbits of the Klein four-group `s ↦ 1 − s`, `s ↦ s̄` (13 October 2026). -/734section strip735736open ComplexConjugate737738/-- A zero of `ζ` with real part at most zero is a trivial zero `−2(n+1)`: at `s' = 1 − s` the functional equation reads739`ζ s = 2 (2π)^{−s'} Γ(s') cos(π s'/2) ζ(s')` with `Re s' ≥ 1`, where `ζ(s') ≠ 0` (the Euler product), so `cos(π s'/2) = 0`,740`s'` an odd integer and `s` an even integer `≤ 0`; `s = 0` is excluded by `ζ 0 = −1/2`. -/741theorem zero_re_nonpos_trivial {s : ℂ} (h0 : riemannZeta s = 0) (hre : s.re ≤ 0) :742    ∃ n : ℕ, s = -2 * (n + 1) := by743  have hs0 : s ≠ 0 := fun h => by rw [h, riemannZeta_zero] at h0; norm_num at h0744  set s' := 1 - s with hs'745  have hre' : 1 ≤ s'.re := by simp only [hs', Complex.sub_re, Complex.one_re]; linarith746  have hne : ∀ n : ℕ, s' ≠ -n := fun n h => by747    have := congrArg Complex.re h748    simp only [Complex.neg_re, Complex.natCast_re] at this749    have : (0 : ℝ) ≤ n := Nat.cast_nonneg n750    linarith751  have hne1 : s' ≠ 1 := fun h => hs0 (by rw [hs'] at h; linear_combination -h)752  have hfe := riemannZeta_one_sub hne hne1753  have h1s : 1 - s' = s := by rw [hs']; ring754  rw [h1s, h0] at hfe755  have hz : riemannZeta s' ≠ 0 := riemannZeta_ne_zero_of_one_le_re hre'756  have hΓ : Complex.Gamma s' ≠ 0 := Complex.Gamma_ne_zero_of_re_pos (by linarith)757  have hpow : (2 * (Real.pi : ℂ)) ^ (-s') ≠ 0 := by758    rw [Complex.cpow_ne_zero_iff]; left759    exact mul_ne_zero two_ne_zero (Complex.ofReal_ne_zero.2 Real.pi_ne_zero)760  have hcos : Complex.cos ((Real.pi : ℂ) * s' / 2) = 0 := by761    have h := hfe.symm762    simp only [mul_eq_zero, two_ne_zero, false_or, hpow, hΓ, hz, or_false] at h763    exact h764  obtain ⟨k, hk⟩ := Complex.cos_eq_zero_iff.1 hcos765  have hπ : (Real.pi : ℂ) ≠ 0 := Complex.ofReal_ne_zero.2 Real.pi_ne_zero766  have hs'k : s' = 2 * k + 1 := by767    have : (Real.pi : ℂ) * s' = (Real.pi : ℂ) * (2 * k + 1) := by linear_combination 2 * hk768    exact mul_left_cancel₀ hπ this769  have hsk : s = -2 * k := by rw [← h1s, hs'k]; ring770  have hk0 : 0 ≤ k := by771    have := congrArg Complex.re hsk772    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 this773    have : (0 : ℝ) ≤ k := by linarith774    exact_mod_cast this775  have hk1 : k ≠ 0 := fun h => hs0 (by rw [hsk, h]; simp)776  refine ⟨(k - 1).toNat, ?_⟩777  have hk1' : 1 ≤ k := by omega778  have : ((k - 1).toNat : ℤ) = k - 1 := Int.toNat_of_nonneg (by omega)779  rw [hsk]780  have hcast : ((((k - 1).toNat : ℕ) : ℂ)) = (k : ℂ) - 1 := by781    rw [← Int.cast_natCast, this]; push_cast; ring782  rw [hcast]; ring783784/-- 20:D8, the strip: a nontrivial zero of `ζ` lies in the open strip `0 < Re s < 1`, and its Klein-four orbit under785`s ↦ 1 − s` and `s ↦ s̄` consists of zeros: `Re s < 1` by the Euler product (`riemannZeta_ne_zero_of_one_le_re`),786`0 < Re s` by the functional equation with the Euler product on the reflected side, `ζ(1 − s) = 0` by the functional787equation (`riemannZeta_one_sub`) and `ζ(s̄) = 0` by `riemannZeta_conj`. -/788theorem zeros_in_strip {s : ℂ} (h0 : riemannZeta s = 0) (htriv : ¬∃ n : ℕ, s = -2 * (n + 1)) (h1 : s ≠ 1) :789    0 < s.re ∧ s.re < 1 ∧ riemannZeta (1 - s) = 0 ∧ riemannZeta (conj s) = 0 := by790  have hlt : s.re < 1 := by791    by_contra h792    exact riemannZeta_ne_zero_of_one_le_re (not_lt.1 h) h0793  have hpos : 0 < s.re := by794    by_contra h795    exact htriv (zero_re_nonpos_trivial h0 (not_lt.1 h))796  refine ⟨hpos, hlt, ?_, ?_⟩797  · have hne : ∀ n : ℕ, s ≠ -n := fun n h => by798      have := congrArg Complex.re h799      simp only [Complex.neg_re, Complex.natCast_re] at this800      have : (0 : ℝ) ≤ n := Nat.cast_nonneg n801      linarith802    rw [riemannZeta_one_sub hne h1, h0, mul_zero]803  · rw [riemannZeta_conj, h0, map_zero]804805end strip806807/-! ## Turing's count (20:F1; 15 October 2026): the completed zeta is real on the line, and a sign change of it between808two heights is a zero of `ζ` on the line between them — the analytic half of the certificate, whose finite half is809`FRC.Horizon.turing_chain`, `turing_equal`, `turing_phantom`. -/810section turing811812open ComplexConjugate813814theorem line_ne_zero (t : ℝ) : (1 / 2 + t * Complex.I : ℂ) ≠ 0 := by815  intro h816  have := congrArg Complex.re h817  simp at this818819theorem line_ne_one (t : ℝ) : (1 / 2 + t * Complex.I : ℂ) ≠ 1 := by820  intro h821  have := congrArg Complex.re h822  norm_num at this823824/-- The factor `π^{−w/2} Γ(w/2)` does not vanish for `Re w > 0`. -/825theorem scale_ne_zero {w : ℂ} (hw : 0 < w.re) :826    ((Real.pi : ℂ) ^ (-w / 2) * Complex.Gamma (w / 2)) ≠ 0 := by827  refine mul_ne_zero ?_ ?_828  · exact Complex.cpow_ne_zero_iff.mpr (Or.inl (by exact_mod_cast Real.pi_ne_zero))829  · exact Complex.Gamma_ne_zero_of_re_pos (by simp; linarith)830831/-- 20:F1 — `Λ(w) = ζ(w) π^{−w/2} Γ(w/2)` for `Re w > 0` (Mathlib's `riemannZeta_eq_completedRiemannZeta₀` with832`completedRiemannZeta_eq`). -/833theorem completed_eq_mul {w : ℂ} (hw : 0 < w.re) :834    completedRiemannZeta w = riemannZeta w * ((Real.pi : ℂ) ^ (-w / 2) * Complex.Gamma (w / 2)) := by835  have hw0 : w ≠ 0 := fun h => by simp [h] at hw836  rw [riemannZeta_eq_completedRiemannZeta₀ hw0, ← completedRiemannZeta_eq, div_mul_cancel₀ _ (scale_ne_zero hw)]837838/-- 20:F1 — `Λ(s̄) = conj Λ(s)` for `Re s > 0`: `ζ`, `Γ` and the real power commute with conjugation. -/839theorem completed_conj {s : ℂ} (hs : 0 < s.re) :840    completedRiemannZeta (conj s) = conj (completedRiemannZeta s) := by841  have hs' : 0 < (conj s).re := by simpa using hs842  rw [completed_eq_mul hs', completed_eq_mul hs, map_mul, map_mul, riemannZeta_conj, ← Complex.Gamma_conj]843  congr 2844  · have h1 : (-(conj s) / 2 : ℂ) = conj (-s / 2) := by rw [map_div₀, map_neg, map_ofNat]845    have hπ : (Real.pi : ℂ).arg ≠ Real.pi := by846      rw [Complex.arg_ofReal_of_nonneg Real.pi_pos.le]; exact Real.pi_ne_zero.symm847    rw [h1, Complex.cpow_conj _ _ hπ, Complex.conj_ofReal]848  · congr 1; rw [map_div₀, map_ofNat]849850/-- 20:F1 — the completed zeta is real on the line: `1 − s = s̄` there, so `Λ(s) = Λ(1 − s) = Λ(s̄) = conj Λ(s)`. -/851theorem completed_im_line (t : ℝ) : (completedRiemannZeta (1 / 2 + t * Complex.I)).im = 0 := by852  set s : ℂ := 1 / 2 + t * Complex.I with hs853  have hre : 0 < s.re := by simp [hs]854  have h1 : conj s = 1 - s := by855    apply Complex.ext <;> simp [hs]; norm_num856  have h2 : conj (completedRiemannZeta s) = completedRiemannZeta s := by857    rw [← completed_conj hre, h1, completedRiemannZeta_one_sub]858  exact Complex.conj_eq_iff_im.mp h2859860/-- The real part of the completed zeta along the line is continuous in the height. -/861theorem continuous_line_re :862    Continuous (fun t : ℝ => (completedRiemannZeta (1 / 2 + t * Complex.I)).re) := by863  have hline : Continuous (fun t : ℝ => (1 / 2 + t * Complex.I : ℂ)) := by fun_prop864  refine Complex.continuous_re.comp (continuous_iff_continuousAt.mpr fun t => ?_)865  exact ContinuousAt.comp (f := fun t : ℝ => (1 / 2 + t * Complex.I : ℂ)) (g := completedRiemannZeta)866    (differentiableAt_completedZeta (line_ne_zero t) (line_ne_one t)).continuousAt hline.continuousAt867868/-- 20:F1 — Turing's count, the analytic clause: a sign change of `Re Λ(1/2 + it)` between the heights `a < b` is869a zero of `ζ` on the line strictly between them (the intermediate value theorem on the real function870`completed_im_line`, divided by the non-vanishing factor `scale_ne_zero`). Each certified sign change of the871package's main sum is such a zero; the finite count is `FRC.Horizon.turing_chain`. -/872theorem zero_of_sign_change {a b : ℝ} (hab : a < b)873    (h : (completedRiemannZeta (1 / 2 + a * Complex.I)).re * (completedRiemannZeta (1 / 2 + b * Complex.I)).re < 0) :874    ∃ t : ℝ, a < t ∧ t < b ∧ riemannZeta (1 / 2 + t * Complex.I) = 0 := by875  set f : ℝ → ℝ := fun t => (completedRiemannZeta (1 / 2 + t * Complex.I)).re with hf876  have hc : ContinuousOn f (Set.Icc a b) := continuous_line_re.continuousOn877  have key : ∀ t : ℝ, f t = 0 → riemannZeta (1 / 2 + t * Complex.I) = 0 := by878    intro t ht879    have hre : 0 < (1 / 2 + t * Complex.I : ℂ).re := by simp880    have hΛ : completedRiemannZeta (1 / 2 + t * Complex.I) = 0 :=881      Complex.ext (by simpa [hf] using ht) (by simpa using completed_im_line t)882    have := completed_eq_mul hre883    rw [hΛ] at this884    exact (mul_eq_zero.mp this.symm).resolve_right (scale_ne_zero hre)885  rcases mul_neg_iff.mp h with ⟨ha, hb⟩ | ⟨ha, hb⟩886  · obtain ⟨t, ⟨hta, htb⟩, hft⟩ := intermediate_value_Ioo' hab.le hc ⟨hb, ha⟩887    exact ⟨t, hta, htb, key t hft⟩888  · obtain ⟨t, ⟨hta, htb⟩, hft⟩ := intermediate_value_Ioo hab.le hc ⟨ha, hb⟩889    exact ⟨t, hta, htb, key t hft⟩890891end turing892893end FRC.Chart894