Rh.lean — FrcCore

1import FrcCore.Sum2import FrcCore.Instances3import FrcCore.Poly4import FrcCore.Theme.Extension5import FrcCore.Theme.Horizon6import FrcCore.Keys.Horizon7import FrcCore.Keys.Foundation89/-!10# FrcCore.Rh — the shell predicates of 20-rh with no axioms1112The exact arithmetic of *Riemann Hypothesis over Finite Holographic Substrate* (20-rh), block B and the `𝔽_p`13reading of the shell theorem, on the kernel alone. For every frame `(τ; 0, 1, g)` of capacity `κ`14(`p = 4κ + 1`): the zero-slot `Σ_{x≠0} x^k = 0` on the nonterminal exponents and `−1` on the full cycle (20:B4);15slot complementarity `k ↦ −g^k`, injective on the nontrivial spectral slots and onto `F^× ∖ {−1}` (20:B5);16the half-turn arithmetic `2⁻¹ = 2κ + 1 = −π` (20:B8) and the Subject constants `π = 2κ`, `i = g^{−κ} = −g^κ`,17`i² = −1`, `g^π = −1`, `e^{iπ} = −1` on every odd representative (20:B10); the scale-shift on the power18characters and its fixed-point count `(p − 1)·[(p − 1) ∣ r]` — the `𝔽_p` reading of 20:E1 and 20:E12 (iii); the Ramanujan sum19`c_p(n) = −1` off the origin in any shell carrying a root of unity of order `p` (20:B7); the quadratic20extension `F(η)`, `η² = ν`, as pairs of residues — the Klein four-group of conjugation and the half-turn21`z ↦ 1 − z` with its three fixed loci (20:B9, with Frobenius read as conjugation: `z^p = z̄` is decided on `𝔽₁₃`22here and proved for every prime shell on Mathlib), the critical line `Tr z = 1 ⟺ Re z = 2⁻¹` with its energy23`(2⁻¹)² − νb²` (20:B8), conjugation as inversion on the norm-one circle and the quarter-turn24conjugation-fixed and off the circle (20:B6); frame coincidence below the horizon — window products read25back exactly and a residue `m ≤ H` factors on the shell exactly when it factors as an integer, on the Subject26and on the Carrier alike (20:B2). On `𝔽₁₃` and `𝔽₅₃`, decided by the kernel: the phase circle of `𝔽₁₃(√2)`27has `14` points and Frobenius `z ↦ z^{13}` is conjugation on all `169` of them, the Ramanujan sums of28`𝔽₅₃` with `ω = 16` of order `13`, the constants of `𝔽₁₃(τ; 0, 1, 2)`, and the laboratory pair `(13, 233)`29(20:B1). No axioms.3031Since the ledger migration (task LM17) the quadratic extension is the extension theme's `FRC.Extension.Ext p ν`32(`Theme/Extension.lean`): 20-rh's pairs `Ext p`, with `ν` passed to each operation, became the one type with `ν` its33parameter, and the product, powers and the norm became its instances. The half-turn, the critical line and the readout34stay here on that type; `readout` takes `ν`. The sums, the counting lemmas and the deciders went to the frame theme.35Since task LM26 the shell theorem's clauses (the zero-slot, the half-turn `2⁻¹ = 2κ + 1`, the scale-shift's characters and36trace, the readout on the trace-one line and the slot index) live in the horizon theme (`Theme/Horizon.lean`), the home of3700:Z10. Every old name stays as an alias. Since task LM36 (20-rh's ledger file) the rest of the paper's shell arithmetic38lives there too: slot complementarity, the Subject constants, the Ramanujan sum, the half-turn, the Klein four-group, the39critical line and its fixed loci, the quarter-turn off the circle, frame coincidence and the values on `𝔽₁₃`, `𝔽₅₃` and40`(13, 233)`. This module keeps their old names as aliases, the frame of `𝔽₅₃`, and the predicate declarations, each the41alias of its key.42-/4344namespace FRC.Rh4546open FRC.Shell FRC.Shell.Frame4748variable {p : Nat} [Pos p]4950/-- A residue `l + 1 < p` is nonzero. -/51theorem ofNat_succ_ne_zero {l : Nat} (hl : l + 1 < p) : (ofNat (l + 1) : Shell p) ≠ 0 := fun h => by52  have := val_injective h53  rw [val_ofNat, val_zero, FRC.Nat.mod_eq_of_lt hl] at this54  exact Nat.noConfusion this5556/-! ## The frame of `𝔽₅₃` (00:C1) -/5758/-- 00:C1 on `𝔽₅₃`: the frame `(τ; 0, 1, 2)` of capacity `13`, and `ω = 2^4 = 16` of order `13`. -/59theorem frame53 : Frame 53 13 (2 : Shell 53) ∧ IsPrimitive (16 : Shell 53) 13 ∧ (2 : Shell 53) ^ 4 = 16 :=60  ⟨⟨rfl, Nat.zero_lt_succ 12, by decide⟩, by decide, by decide⟩616263/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/64section aliases65variable {κ : Nat} {g : Shell p}6667/-- `p ≡ 0` on the shell (20-rh's name; the lemma is `FRC.Shell.Frame.ofNat_self`). -/68theorem ofNat_p : (ofNat p : Shell p) = 0 :=69  FRC.Shell.Frame.ofNat_self7071/-- `n + p ≡ n` on the shell (20-rh's name; the lemma is `FRC.Shell.Frame.ofNat_add_self`). -/72theorem ofNat_add_p (n : Nat) : (ofNat (n + p) : Shell p) = ofNat n :=73  FRC.Shell.Frame.ofNat_add_self n7475/-- Counting where nothing satisfies the predicate. -/76theorem natCount_eq_zero (P : Nat → Prop) [DecidablePred P] : ∀ n, (∀ x, x < n → ¬ P x) → natCount P n = 0 :=77  FRC.Shell.Frame.natCount_eq_zero P7879/-- Counting through an equivalent predicate. -/80theorem natCount_congr (P Q : Nat → Prop) [DecidablePred P] [DecidablePred Q] :81    ∀ n, (∀ x, x < n → (P x ↔ Q x)) → natCount P n = natCount Q n :=82  FRC.Shell.Frame.natCount_congr P Q8384/-- `Σ_{l<n+1} f l = f 0 + Σ_{l<n} f (l + 1)`. -/85theorem sumRange_succ' (f : Nat → Shell p) : ∀ n, sumRange f (n + 1) = f 0 + sumRange (fun l => f (l + 1)) n :=86  FRC.Shell.sumRange_succ' f8788/-- The sum over the nonzero residues equals the sum over the powers of the drive: `x = g^m` reindexes. -/89theorem sum_units_eq_sum_pow (F : Frame p κ g) (f : Shell p → Shell p) :90    sumRange (fun l => f (ofNat (l + 1))) (p - 1) = sumRange (fun m => f (g ^ m)) (p - 1) :=91  FRC.Shell.Frame.sum_units_eq_sum_pow F f9293/-- 20:B4 — the zero-slot (20-rh's name; the theorem is `FRC.Horizon.zero_slot`, LM26). -/94theorem zero_slot (F : Frame p κ g) :95    (∀ k, 0 < k → k < p - 1 → sumRange (fun l => (ofNat (l + 1) : Shell p) ^ k) (p - 1) = 0) ∧96    sumRange (fun l => (ofNat (l + 1) : Shell p) ^ (p - 1)) (p - 1) = -1 :=97  FRC.Horizon.zero_slot F9899/-- 20:B8 — `2⁻¹ = 2κ + 1 = −π` (20-rh's name; the theorem is `FRC.Horizon.half_inverse`, LM26). -/100theorem half_inverse (F : Frame p κ g) :101    (2 : Shell p) * ofNat (2 * κ + 1) = 1 ∧ (ofNat (2 * κ + 1) : Shell p) = -(ofNat (2 * κ)) :=102  FRC.Horizon.half_inverse F103104/-- 20:E1, 20:E12 — the power characters under the scale-shift (20-rh's name; the theorem is105`FRC.Horizon.shift_power_character`, LM26). -/106theorem shift_power_character (r k : Nat) (x : Shell p) : (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k :=107  FRC.Horizon.shift_power_character r k x108109/-- 20:E12, 20:E1 — the fixed-point count of the scale-shift (20-rh's name; the theorem is `FRC.Horizon.shift_trace`,110LM26). -/111theorem shift_trace (F : Frame p κ g) (r : Nat) :112    natCount (fun x => x ≠ 0 ∧ g ^ r * ofNat x = ofNat x) p = if r % (p - 1) = 0 then p - 1 else 0 :=113  FRC.Horizon.shift_trace F r114115/-! The declarations moved to the horizon theme by task LM36 (`FRC.Horizon`, `Theme/Horizon.lean`), each under its old116name: slot complementarity, the Subject constants, the Ramanujan sum, frame coincidence and the laboratory pair. -/117118/-- 20:B5 — slot complementarity (20-rh's name; the theorem is `FRC.Horizon.slot_complementarity`, LM36). -/119theorem slot_complementarity (F : Frame p κ g) :120    (∀ i j, i < p - 1 → j < p - 1 → -(g ^ i) = -(g ^ j) → i = j) ∧121    (∀ k, 0 < k → k < p - 1 → -(g ^ k) ≠ 0 ∧ -(g ^ k) ≠ -1) ∧122    (∀ y : Shell p, y ≠ 0 → y ≠ -1 → ∃ k, 0 < k ∧ k < p - 1 ∧ -(g ^ k) = y) :=123  FRC.Horizon.slot_complementarity F124125/-- 20:B10 — `i = g^{−κ}` is `−g^κ` (20-rh's name; the theorem is `FRC.Horizon.quarter_turn_eq_pow`, LM36). -/126theorem quarter_turn_eq_pow (F : Frame p κ g) : g ^ (3 * κ) = quarterTurn g κ :=127  FRC.Horizon.quarter_turn_eq_pow F128129/-- 20:B10 — the Subject constants (20-rh's name; the theorem is `FRC.Horizon.subject_constants`, LM36). -/130theorem subject_constants (F : Frame p κ g) :131    (ofNat (2 * halfPeriod κ) : Shell p) = -1 ∧ g ^ (3 * κ) = quarterTurn g κ ∧132    quarterTurn g κ * quarterTurn g κ = -1 ∧ g ^ (2 * κ) = -1 ∧133    ∀ m : Nat, m % 2 = 1 → (g ^ m) ^ (m * (2 * κ)) = -1 :=134  FRC.Horizon.subject_constants F135136/-- 20:B10 [value] — the constants on `𝔽₁₃` (20-rh's name; the theorem is `FRC.Horizon.constants13`, LM36). -/137theorem constants13 :138    (2 : Shell 13) * 6 = -1 ∧ (2 : Shell 13) ^ 9 = 5 ∧ quarterTurn (2 : Shell 13) 3 = 5 ∧139    (5 : Shell 13) * 5 = -1 ∧ (2 : Shell 13) ^ 5 = 6 ∧ (2 : Shell 13) ^ 6 = -1 ∧140    (6 : Shell 13) ^ (5 * 6) = -1 :=141  FRC.Horizon.constants13142143/-- Powers reduce modulo the order (20-rh's name; the theorem is `FRC.Horizon.pow_mod_of_pow_eq_one`, LM36). -/144theorem pow_mod_of_pow_eq_one {q : Nat} [Pos q] {ω : Shell q} {m : Nat} (hm : 0 < m) (hω : ω ^ m = 1) (l : Nat) :145    ω ^ l = ω ^ (l % m) :=146  FRC.Horizon.pow_mod_of_pow_eq_one hm hω l147148/-- 20:B7 — the Ramanujan sum (20-rh's name; the theorem is `FRC.Horizon.ramanujan_sum`, LM36). -/149theorem ramanujan_sum {q : Nat} [Pos q] {κ' : Nat} {h : Shell q} (F : Frame q κ' h) {m : Nat} (hm : 0 < m)150    {ω : Shell q} (hω : IsPrimitive ω m) (n : Nat) (hn : n % m ≠ 0) :151    sumRange (fun a => ω ^ (n * (a + 1))) (m - 1) = -1 :=152  FRC.Horizon.ramanujan_sum F hm hω n hn153154/-- 20:B7 [value] — the Ramanujan sums of `𝔽₅₃` (20-rh's name; the theorem is `FRC.Horizon.ramanujan53`, LM36). -/155theorem ramanujan53 :156    (∀ n, n < 13 → 0 < n → sumRange (fun a => (16 : Shell 53) ^ (n * (a + 1))) 12 = -1) ∧157    sumRange (fun a => (16 : Shell 53) ^ (0 * (a + 1))) 12 = 12 :=158  FRC.Horizon.ramanujan53159160/-- `H ≤ H²` (20-rh's name; the theorem is `FRC.Horizon.le_mul_self`, LM36). -/161theorem le_mul_self (H : Nat) : H ≤ H * H :=162  FRC.Horizon.le_mul_self H163164/-- 20:B2 — the window reads back (20-rh's name; the theorem is `FRC.Horizon.window_readback`, LM36). -/165theorem window_readback {H : Nat} (hH : H * H < p) :166    (∀ m, m ≤ H → (ofNat m : Shell p).val = m) ∧167    ∀ a b, a ≤ H → b ≤ H → (ofNat a * ofNat b : Shell p).val = a * b :=168  FRC.Horizon.window_readback hH169170/-- 20:B2 — primality equals irreducibility in the window (20-rh's name; the theorem is171`FRC.Horizon.factorisation_iff`, LM36). -/172theorem factorisation_iff {H : Nat} (hH : H * H < p) (m : Nat) (hm : m ≤ H) :173    (∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (ofNat a * ofNat b : Shell p) = ofNat m) ↔174    ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a * b = m :=175  FRC.Horizon.factorisation_iff hH m hm176177/-- 20:B2 — frame coincidence (20-rh's name; the theorem is `FRC.Horizon.frame_coincidence`, LM36). -/178theorem frame_coincidence {Ω : Nat} [Pos Ω] {H : Nat} (hp : H * H < p) (hΩ : H * H < Ω) (m : Nat) (hm : m ≤ H) :179    (∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (ofNat a * ofNat b : Shell p) = ofNat m) ↔180    (∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (ofNat a * ofNat b : Shell Ω) = ofNat m) :=181  FRC.Horizon.frame_coincidence hp hΩ m hm182183/-- 20:B1 [value] — the laboratory pair (20-rh's name; the theorem is `FRC.Horizon.lab_pair`, LM36). -/184theorem lab_pair :185    13 * 13 < 233 ∧ 12 % 4 = 0 ∧ 232 % 4 = 0 ∧ 232 % 3 ≠ 0 ∧ (5 : Shell 13) * 5 = -1 ∧186    (89 : Shell 233) * 89 = -1 ∧ 232 % 12 ≠ 0 ∧ 3 * 3 < 13 ∧ 3 * 3 < 233 :=187  FRC.Horizon.lab_pair188189/-- 20-rh's quadratic extension: `FRC.Extension.Ext p ν`, its `ν` now a parameter of the type. -/190@[reducible] def Ext (p : Nat) [Pos p] (ν : Shell p) : Type := FRC.Extension.Ext p ν191192namespace Ext193variable {ν : Shell p}194open FRC.Extension.Ext (ofShell)195196theorem ext {z z' : Ext p ν} (h1 : z.re = z'.re) (h2 : z.im = z'.im) : z = z' :=197  FRC.Extension.Ext.ext h1 h2198199theorem re_congr {a b : Ext p ν} (h : a = b) : a.re = b.re :=200  FRC.Extension.Ext.re_congr h201202theorem im_congr {a b : Ext p ν} (h : a = b) : a.im = b.im :=203  FRC.Extension.Ext.im_congr h204205/-- Conjugation `a + bη ↦ a − bη` (Frobenius on the extension). -/206@[reducible] def conj (z : Ext p ν) : Ext p ν :=207  FRC.Extension.Ext.conj z208209/-- The trace `Tr(a + bη) = 2a`. -/210@[reducible] def trace (z : Ext p ν) : Shell p :=211  FRC.Extension.Ext.trace z212213/-- The norm `N(a + bη) = a² − νb²`. -/214@[reducible] def norm (z : Ext p ν) : Shell p :=215  FRC.Extension.Ext.norm z216217/-- Powers, by repeated multiplication. -/218@[reducible] def pow (z : Ext p ν) : Nat → Ext p ν :=219  FRC.Extension.Ext.pow z220221/-- 20:B6 — `z z̄ = N(z)`: conjugation is inversion on the norm-one circle. -/222theorem mul_conj (z : Ext p ν) : z * conj z = ofShell (norm z) :=223  FRC.Extension.Ext.mul_conj z224225/-- 20:B6 — on the circle `N(z) = 1` the conjugate is the inverse: `z z̄ = 1`. -/226theorem conj_inv_of_norm_one (z : Ext p ν) (hz : norm z = 1) : z * conj z = 1 :=227  FRC.Extension.Ext.conj_inv_of_norm_one z hz228229/-- 20:B9 — the fixed locus of conjugation is the prime meridian: `z̄ = z ⟺ b = 0`. -/230theorem fixed_conj (F : Frame p κ g) (z : Ext p ν) : conj z = z ↔ z.im = 0 :=231  FRC.Extension.Ext.fixed_conj F z232233/-- The functional-equation half-turn `ρ : z ↦ 1 − z` (20-rh's name; the definition is `FRC.Horizon.rho`, LM36). -/234@[reducible] def rho (z : Ext p ν) : Ext p ν := FRC.Horizon.rho z235236/-- `σ = ρ ∘ φ : z ↦ 1 − z̄` (20-rh's name; the definition is `FRC.Horizon.sigma`, LM36). -/237@[reducible] def sigma (z : Ext p ν) : Ext p ν := FRC.Horizon.sigma z238239/-- 20:B9 — the Klein four-group (20-rh's name; the theorem is `FRC.Horizon.klein_four`, LM36). -/240theorem klein_four (z : Ext p ν) :241    FRC.Extension.Ext.conj (FRC.Extension.Ext.conj z) = z ∧ FRC.Horizon.rho (FRC.Horizon.rho z) = z ∧242    FRC.Extension.Ext.conj (FRC.Horizon.rho z) = FRC.Horizon.rho (FRC.Extension.Ext.conj z) :=243  FRC.Horizon.klein_four z244245/-- 20:B8, 20:B9 — the finite critical line (20-rh's name; the theorem is `FRC.Horizon.critical_line`, LM36). -/246theorem critical_line {κ : Nat} {g : Shell p} (F : Frame p κ g) (z : Ext p ν) :247    (FRC.Extension.Ext.trace z = 1 ↔ z.re = ofNat (2 * κ + 1)) ∧248    (FRC.Horizon.sigma z = z ↔ z.re = ofNat (2 * κ + 1)) ∧249    ∀ b : Shell p, FRC.Extension.Ext.trace (⟨ofNat (2 * κ + 1), b⟩ : Ext p ν) = 1 :=250  FRC.Horizon.critical_line F z251252/-- 20:B9 — the fixed locus of the half-turn (20-rh's name; the theorem is `FRC.Horizon.fixed_half_turn`, LM36). -/253theorem fixed_half_turn {κ : Nat} {g : Shell p} (F : Frame p κ g) (z : Ext p ν) :254    (FRC.Horizon.rho z = z ↔ (FRC.Extension.Ext.conj z = z ∧ FRC.Horizon.sigma z = z)) ∧255    (FRC.Horizon.rho z = z ↔ z = ⟨ofNat (2 * κ + 1), 0⟩) :=256  FRC.Horizon.fixed_half_turn F z257258/-- 20:B8 — the energy on the critical line (20-rh's name; the theorem is `FRC.Horizon.norm_on_line`, LM36). -/259theorem norm_on_line {κ : Nat} {g : Shell p} (F : Frame p κ g) (z : Ext p ν) (hz : z.re = ofNat (2 * κ + 1)) :260    FRC.Extension.Ext.norm z = ofNat (2 * κ + 1) * ofNat (2 * κ + 1) + -(ν * (z.im * z.im)) ∧261    (2 : Shell p) * ofNat (2 * κ + 1) = 1 :=262  FRC.Horizon.norm_on_line F z hz263264/-- 20:B6 — the quarter-turn off the circle (20-rh's name; the theorem is `FRC.Horizon.quarter_turn_off_circle`,265LM36). -/266theorem quarter_turn_off_circle {κ : Nat} {g : Shell p} (F : Frame p κ g) (ν : Shell p) :267    FRC.Extension.Ext.conj (⟨quarterTurn g κ, 0⟩ : Ext p ν) = ⟨quarterTurn g κ, 0⟩ ∧268    FRC.Extension.Ext.norm (⟨quarterTurn g κ, 0⟩ : Ext p ν) = -1 ∧269    FRC.Extension.Ext.norm (⟨quarterTurn g κ, 0⟩ : Ext p ν) ≠ 1 :=270  FRC.Horizon.quarter_turn_off_circle F ν271272/-- 20:B6 [value] — the circle of `𝔽₁₃(√2)` (20-rh's name; the theorem is `FRC.Horizon.circle13`, LM36). -/273theorem circle13 :274    natCount (fun k => FRC.Extension.Ext.norm (⟨ofNat (k / 13), ofNat (k % 13)⟩ : FRC.Extension.Ext 13 2) = 1) 169 = 14 ∧275    (∀ k, k < 169 → (⟨ofNat (k / 13), ofNat (k % 13)⟩ : FRC.Extension.Ext 13 2) ^ 13 =276      FRC.Extension.Ext.conj ⟨ofNat (k / 13), ofNat (k % 13)⟩) ∧277    (∀ x : Nat, x < 13 → 0 < x → (ofNat x : Shell 13) * ofNat x ≠ 2) :=278  FRC.Horizon.circle13279280/-- 20-rh's product, the instance `z * w` of `FRC.Extension.Ext p ν`. -/281@[reducible] def mul (z w : Ext p ν) : Ext p ν := z * w282283/-- 20-rh's unit, `1`. -/284@[reducible] def one : Ext p ν := 1285286/-- 20:E12, 20:B8 — the spectral readout (20-rh's name; the definition is `FRC.Horizon.readout`, LM26). -/287@[reducible] def readout (ν : Shell p) (κ : Nat) (θ : Shell p) : Ext p ν := FRC.Horizon.readout ν κ θ288289/-- 20:E12 (ii) — every readout on the trace-one line (20-rh's name; the theorem is `FRC.Horizon.readout_on_line`, LM26). -/290theorem readout_on_line {κ : Nat} {g : Shell p} (F : Frame p κ g) (ν θ : Shell p) :291    trace (readout ν κ θ) = 1 ∧ (readout ν κ θ).re = ofNat (2 * κ + 1) ∧292    ∀ θ' : Shell p, readout ν κ θ = readout ν κ θ' → θ = θ' :=293  FRC.Horizon.readout_on_line F ν θ294295/-- 20:E12 — the slot index of a nontrivial slot (20-rh's name; the theorem is `FRC.Horizon.readout_slot_index`, LM26). -/296theorem readout_slot_index {κ : Nat} {g : Shell p} (F : Frame p κ g) (k : Nat) (hk1 : 1 ≤ k) (hk2 : k ≤ p - 2) :297    -(g ^ k) ≠ 0 ∧ -(g ^ k) ≠ -1 :=298  FRC.Horizon.readout_slot_index F k hk1 hk2299300end Ext301302/-- Bounded universal quantifiers, decided by search (no axioms). -/303@[reducible] def decForallLT (P : Nat → Prop) [DecidablePred P] : (n : Nat) → Decidable (∀ m, m < n → P m) :=304  FRC.Shell.decForallLT P305306@[reducible] def instDecForallLT (P : Nat → Prop) [DecidablePred P] (n : Nat) : Decidable (∀ m, m < n → P m) :=307  FRC.Shell.instDecForallLT P n308309/-- 20:F7 (Theorem closure), the foundation clauses: the wrap of the height reading and the return of the cycle310(00:A5), Finitude (00:A2), Observation (00:A4). Lives in the horizon theme since 13 October 2026. -/311theorem closure :312    (∀ {p : Nat} [Pos p] (T : Nat), (ofNat (T + p) : Shell p) = ofNat T) ∧313    (∀ {p : Nat} [Pos p], 2 ≤ p → ∀ y : Shell p, ∃ k, k < p ∧ FRC.Foundation.succIter (0 : Shell p) k = y) ∧314    (∀ {U : Type} (Ω : Nat) [Pos Ω] (ρ : U → Nat), (∀ u, ρ u < Ω) →315      ∃ ι : FRC.Foundation.Registered ρ → Shell Ω, ∀ a b, ι a = ι b → a = b) ∧316    (∀ {Ω o : Nat} [Pos Ω], o < Ω → ∀ ρ : Shell Ω → Nat, (∀ x, ρ x < o) → ∃ x y : Shell Ω, x ≠ y ∧ ρ x = ρ y) ∧317    (∀ {Ω o : Nat} [Pos Ω] (ρ : Shell Ω → Nat), (∀ x, ρ x < o) → (∀ x y, ρ x = ρ y → x = y) → Ω ≤ o) :=318  FRC.Horizon.closure319320/-- 20:F7, the laboratory instances of the closure (`FRC.Horizon.closure_lab`). -/321theorem closure_lab :322    (3 * 3 < 13 ∧ 13 < 5 * 5 ∧ 13 % 4 = 1 ∧ FRC.Nat.isPrime 3 ∧ FRC.Nat.isPrime 5 ∧ FRC.Nat.isPrime 13 ∧323      ∀ q, q < 5 → 3 < q → ¬ FRC.Nat.isPrime q) ∧324    (13 * 13 < 233 ∧ 233 < 17 * 17 ∧ 233 % 4 = 1 ∧ FRC.Nat.isPrime 13 ∧ FRC.Nat.isPrime 17 ∧ FRC.Nat.isPrime 233 ∧325      ∀ q, q < 17 → 13 < q → ¬ FRC.Nat.isPrime q) ∧326    (173 * 173 < 30089 ∧ 30089 < 179 * 179 ∧ 30089 % 4 = 1 ∧ FRC.Nat.isPrime 173 ∧ FRC.Nat.isPrime 179 ∧327      FRC.Nat.isPrime 30089 ∧ ∀ q, q < 179 → 173 < q → ¬ FRC.Nat.isPrime q) ∧328    (1549 * 1549 < 2408561 ∧ 2408561 < 1553 * 1553 ∧ 2408561 % 4 = 1 ∧ FRC.Nat.isPrime 1549 ∧ FRC.Nat.isPrime 1553 ∧329      FRC.Nat.isPrime 2408561 ∧ ∀ q, q < 1553 → 1549 < q → ¬ FRC.Nat.isPrime q) :=330  FRC.Horizon.closure_lab331332end aliases333334-- Ledger predicates of 20-rh (generated by make_predicates.py from docs/20-rh/20-rh-ledger.json; edit the ledger, not this section)335/-- 20:A2 (p00004) — Finitude: for any reading of capacity $R$ the registered Universe embeds in the shell of $R$ members, and among $R+1$ members two share a residue; the totality is finite, its cardinality $\Omega$. A theorem of the master ledger (00:A2), proved in the core, cited as the closure's first premise (F7). -/336theorem p00004 : And (∀ {U : Type} (R : Nat) [FRC.Pos R] (ρ : U → Nat), (∀ (u : U), @LT.lt Nat instLTNat (ρ u) R) → @Exists (@FRC.Foundation.Registered U ρ → FRC.Shell R) fun ι => ∀ (a b : @FRC.Foundation.Registered U ρ), @Eq (FRC.Shell R) (ι a) (ι b) → @Eq (@FRC.Foundation.Registered U ρ) a b) (And (∀ {U : Type} (R : Nat) (ρ : U → Nat), (∀ (u : U), @LT.lt Nat instLTNat (ρ u) R) → ∀ (f : Nat → U), @Exists Nat fun i => @Exists Nat fun j => And (@LT.lt Nat instLTNat i (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) R (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (And (@LT.lt Nat instLTNat j (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) R (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (And (@Ne Nat i j) (@Eq Nat (ρ (f i)) (ρ (f j)))))) (∀ (s K : Nat), @LE.le Nat instLENat (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) s → ∀ {N : Nat} [FRC.Pos N] (ρ : FRC.Shell N → Nat), (∀ (x : FRC.Shell N), @LT.lt Nat instLTNat (ρ x) (FRC.Logic.records s K)) → (∀ (x y : FRC.Shell N), @Eq Nat (ρ x) (ρ y) → @Eq (FRC.Shell N) x y) → And (@LE.le Nat instLENat N (FRC.Logic.records s K)) (@LT.lt Nat instLTNat (FRC.Logic.records s K) (@HPow.hPow Nat Nat Nat (@instHPow Nat Nat (@instPowNat Nat instNatPowNat)) s (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) K (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))) :=337  @FRC.Ledger.p00004338/-- 20:A3 (p00003) — Completeness: the registration of any totality is onto its registered Universe, so there is no outside and no host; two totalities each registered whole within the other have one count. A theorem of the master ledger (00:A3), proved in the core; the hypothesis of the Carrier is a statement about its own residues and nothing else. -/339theorem p00003 : (∀ {U : Type} (ρ : U → Nat) (a : FRC.Foundation.Registered ρ), ∃ u, FRC.Foundation.register ρ u = a) ∧ ∀ (m n : Nat) [FRC.Pos m] [FRC.Pos n] (f : FRC.Shell m → FRC.Shell n), (∀ (x y : FRC.Shell m), f x = f y → x = y) → ∀ (g : FRC.Shell n → FRC.Shell m), (∀ (x y : FRC.Shell n), g x = g y → x = y) → m = n :=340  @FRC.Ledger.p00003341/-- 20:A4 (p00197) — Observation: every observation is a registration by an embedded part of $o<\Omega$ states; every reading identifies two members, and a complete reading needs the whole count; one translation carries each member to each. A theorem of the master ledger (00:A4), proved in the core, cited as the closure's second premise (F7) and behind the horizon (Z1). -/342theorem p00197 : (∀ {Ω o : Nat} [FRC.Pos Ω], o < Ω → ∀ (ρ : FRC.Shell Ω → Nat), (∀ (x : FRC.Shell Ω), ρ x < o) → ∃ x y, x ≠ y ∧ ρ x = ρ y) ∧ (∀ {Ω o : Nat} [FRC.Pos Ω] (ρ : FRC.Shell Ω → Nat), (∀ (x : FRC.Shell Ω), ρ x < o) → (∀ (x y : FRC.Shell Ω), ρ x = ρ y → x = y) → Ω ≤ o) ∧ ∀ {Ω : Nat} [FRC.Pos Ω] (x y : FRC.Shell Ω), ∃ t, x + t = y ∧ ∀ (t' : FRC.Shell Ω), x + t' = y → t' = t :=343  @FRC.Ledger.p00197344/-- 20:B1 (p20008) — The two frames on one substrate: the Carrier chart $\F_\Omega$, held by no embedded observer, and the Subject $\Fp$ embedded with $\Omega\gg \p^{2}$; what they share is the quarter-turn core $Q_4$ and nothing else, on the laboratory pair $(13,233)$ the cycles $C_{12}$ and $C_{232}$ admit no projection ($12\nmid232$); hardness by register ($\p$-hard, $\Omega$-hard). -/345theorem p20008 : (13 : Nat) * (13 : Nat) < (233 : Nat) ∧ (12 : Nat) % (4 : Nat) = (0 : Nat) ∧ (232 : Nat) % (4 : Nat) = (0 : Nat) ∧ (232 : Nat) % (3 : Nat) ≠ (0 : Nat) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (-1 : FRC.Shell (233 : Nat)) ∧ (232 : Nat) % (12 : Nat) ≠ (0 : Nat) ∧ (3 : Nat) * (3 : Nat) < (13 : Nat) ∧ (3 : Nat) * (3 : Nat) < (233 : Nat) :=346  @FRC.Ledger.p20008347set_option linter.defProp false in348/-- 20:B2 (p20009) — Frame coincidence below the horizon: for $n\le\sqrt \p$ the residue $n$ is the same integer in $\Fp$ and $\F_\Omega$, and primality of $n$ equals irreducibility in the Subject chart; the Subject-realised primes $\Pi_\p$ are the primes to $\sqrt \p$. -/349def p20009 := @FRC.Ledger.p20009350/-- 20:B4 (p20011) — Zero-slot: $Z_\Omega(k)=\sum_{x\in\Fx{\Omega}}x^{k}$ vanishes on every nonterminal exponent $1\le k\le\Omega-2$ and equals $-1$ on the full cycle; the nonterminal slots are the universal mode basis. -/351theorem p20011 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (k : Nat), (0 : Nat) < k → k < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ k) (p - (1 : Nat)) = (0 : FRC.Shell p)) ∧ FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ (p - (1 : Nat))) (p - (1 : Nat)) = (-1 : FRC.Shell p) :=352  @FRC.Ledger.p20011353/-- 20:B5 (p20012) — Slot complementarity: $\Phi(k)=-\gen^{\,k}$ bijects the nontrivial spectral slots onto the nonterminal additive slots $\Fx{\Omega}\setminus\{-1\}$, the two removed points being $\mu_2$, the intertwiner the half-cycle element. -/354theorem p20012 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (i j : Nat), i < p - (1 : Nat) → j < p - (1 : Nat) → -g ^ i = -g ^ j → i = j) ∧ (∀ (k : Nat), (0 : Nat) < k → k < p - (1 : Nat) → -g ^ k ≠ (0 : FRC.Shell p) ∧ -g ^ k ≠ (-1 : FRC.Shell p)) ∧ ∀ (y : FRC.Shell p), y ≠ (0 : FRC.Shell p) → y ≠ (-1 : FRC.Shell p) → ∃ k, (0 : Nat) < k ∧ k < p - (1 : Nat) ∧ -g ^ k = y :=355  @FRC.Ledger.p20012356set_option linter.defProp false in357/-- 20:B6 (p20013) — Hermitian phase calculus on $K=\F_{\p^{2}}$: norm and trace $\Fp$-valued, the phase circle $U_{\p+1}$ of order $\p+1$ with Frobenius as inversion, the quarter-turn $\im$ Frobenius-fixed and off the circle ($\Nm(\im)=-1$), the trace-zero $\eta$ with $\eta^{2}=\nu$ a nonsquare, $\Tr(a+b\eta)=2a$, $\Nm=a^{2}-\nu b^{2}$. -/358def p20013 := @FRC.Ledger.p20013359/-- 20:B7 (p20014) — Flat ground state: the full-modulus Ramanujan sum $c_\p(n)\equiv-1$ for every $n\not\equiv0$; the mode at the spectral origin carries no prime information. -/360theorem p20014 : (∀ {q : Nat} [FRC.Pos q] {κ' : Nat} {h : FRC.Shell q}, FRC.Shell.Frame q κ' h → ∀ {m : Nat}, (0 : Nat) < m → ∀ {ω : FRC.Shell q}, ω.IsPrimitive m → ∀ (n : Nat), n % m ≠ (0 : Nat) → FRC.Shell.sumRange (fun a => ω ^ (n * (a + (1 : Nat)))) (m - (1 : Nat)) = (-1 : FRC.Shell q)) ∧ (∀ (n : Nat), n < (13 : Nat) → (0 : Nat) < n → FRC.Shell.sumRange (fun a => (16 : FRC.Shell (53 : Nat)) ^ (n * (a + (1 : Nat)))) (12 : Nat) = (-1 : FRC.Shell (53 : Nat))) ∧ FRC.Shell.sumRange (fun a => (16 : FRC.Shell (53 : Nat)) ^ ((0 : Nat) * (a + (1 : Nat)))) (12 : Nat) = (12 : FRC.Shell (53 : Nat)) :=361  @FRC.Ledger.p20014362set_option linter.defProp false in363/-- 20:B8 (p20015) — The finite critical line: the half-turn $2^{-1}=2\kp+1=-\pi$; $\Tr(z)=1$ exactly on the $\p$ points $z=2^{-1}+\eta\theta$, with energy $\Nm(z)=\tfrac14-\nu\theta^{2}$; de-framed, $2^{-1}/\p=(2\kp+1)/\p\to\half$ from above [chart]. -/364def p20015 := @FRC.Ledger.p20015365set_option linter.defProp false in366/-- 20:B9 (p20016) — The two agreement loci: the Klein four-group $\langle\phi,\rho\rangle$ of Frobenius and the functional-equation half-turn fixes exactly $\Fp$ (the prime meridian), $L_{1/2}$ (the critical line) and their meeting $\{2^{-1}\}$; no other line is fixed. -/367def p20016 := @FRC.Ledger.p20016368/-- 20:B10 (p20017) — The Subject constants on the shell: $\pi=2\kp$, $2\pi\equiv-1$, $\im=\gen^{-\kp}$, $\im^{2}\equiv-1$, $\E=\gen^{\,\im}$ on the odd lift, $\gen^{\,\pi}\equiv-1$, $\E^{\,\im\pi}\equiv-1$; on $\F_{13}$: $\gen=2$, $\im=5$, $\E=6$, $\pi=6$. -/369theorem p20017 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Shell.ofNat ((2 : Nat) * FRC.Shell.Frame.halfPeriod κ) = (-1 : FRC.Shell p) ∧ g ^ ((3 : Nat) * κ) = FRC.Shell.Frame.quarterTurn g κ ∧ FRC.Shell.Frame.quarterTurn g κ * FRC.Shell.Frame.quarterTurn g κ = (-1 : FRC.Shell p) ∧ g ^ ((2 : Nat) * κ) = (-1 : FRC.Shell p) ∧ ∀ (m : Nat), m % (2 : Nat) = (1 : Nat) → (g ^ m) ^ (m * ((2 : Nat) * κ)) = (-1 : FRC.Shell p)) ∧ ((2 : FRC.Shell (13 : Nat)) * (6 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (9 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.quarterTurn (2 : FRC.Shell (13 : Nat)) (3 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (5 : Nat) = (6 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (6 : Nat) = (-1 : FRC.Shell (13 : Nat)) ∧ (6 : FRC.Shell (13 : Nat)) ^ ((5 : Nat) * (6 : Nat)) = (-1 : FRC.Shell (13 : Nat))) ∧ FRC.Shell.Frame (13 : Nat) (3 : Nat) (2 : FRC.Shell (13 : Nat)) :=370  @FRC.Ledger.p20017371/-- 20:D5 (p20029) — The cells: the heights of a Carrier's cycle are its residues, residue $y$ the cell from $2\pi y$ to $2\pi(y+1)$; a cell is clean when its zeros lie on the line, which Turing's count decides from the labels below $\sqrt{y+1}$, and passes when the frame's reading certifies it. The hypothesis of the Carrier: every residue has a clean cell. -/372theorem p20029 : (∀ {α : Type} (fixed : α → Bool) (l : List α), (∀ (z : α), z ∈ l → fixed z = true) ↔ FRC.Horizon.fixedCount fixed l = l.length) ∧ ∀ (c n : Nat → Nat) (m : Nat), (∀ (y : Nat), y < m → c y ≤ n y) → ((∀ (y : Nat), y < m → c y = n y) ↔ FRC.Shell.Frame.sumTo c m = FRC.Shell.Frame.sumTo n m) :=373  @FRC.Ledger.p20029374set_option linter.defProp false in375/-- 20:D9 (p20083) — The finite negative control: on $\F_{13}(\sqrt2)$ the polynomial $((X-2)^{2}-2)((X+1)^{2}-2)$ has exactly the roots $2\pm\eta$, $-1\pm\eta$, of traces $4$, $4$, $11$, $11$ against the line's $1$, the root set closed under conjugation and under the half-turn; finitude, conjugation and the reflection force no root onto the line. -/376def p20083 := @FRC.Ledger.p20083377/-- 20:E1 (p20032) — The scale-evolution generator: on the shell the scale-shift $x\mapsto\gen^{\,r}x$ is a unitary permutation of $\Fx{\p}$ with the complex characters as eigenvectors; in the analytic chart [chart] the dilation group $U_r=e^{ir\Hh}$ has the self-adjoint generator $\Hh=-i(x\partial_x+\half)$ with generalised eigenfunctions $x^{-\bar\rho}$, $\rho=\half+i\gamma$, the symmetrizing $\half$ the half-turn of B8; the chart assignment is used nowhere as a shell identity. -/378theorem p20032 : (∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (r k : Nat) (x : FRC.Shell p), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r : Nat), FRC.Shell.Frame.natCount (fun x => x ≠ (0 : Nat) ∧ g ^ r * FRC.Shell.ofNat x = FRC.Shell.ofNat x) p = if r % (p - (1 : Nat)) = (0 : Nat) then p - (1 : Nat) else (0 : Nat) :=379  @FRC.Ledger.p20032380/-- 20:E12 (p20043) — \textbf{The shell theorem.} On every shell, with no hypothesis: (i) $v$ expands in the constant mode and the nonterminal modes of the quarter-turn meridian; (ii) every readout lies on $\Tr=1$, real part $2^{-1}=2\kp+1=-\pi$; (iii) the scale-shift has the modes as eigenvectors, eigenphases $2\pi j/(\p-1)$ independent of $v$. No off-line mode; true of every vector, the Davenport--Heilbronn vector included. -/381theorem p20043 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (k : Nat), (0 : Nat) < k → k < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ k) (p - (1 : Nat)) = (0 : FRC.Shell p)) ∧ FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ (p - (1 : Nat))) (p - (1 : Nat)) = (-1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (v : Nat → FRC.Shell p) {j : Nat}, j < p - (1 : Nat) → v j = FRC.Shell.sumRange (fun k => FRC.Horizon.modeCoeff g v k * (g ^ j) ^ k) (p - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (r k : Nat) (x : FRC.Shell p), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r k : Nat), ((g ^ r) ^ k) ^ (p - (1 : Nat)) = (1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r : Nat), FRC.Shell.Frame.natCount (fun x => x ≠ (0 : Nat) ∧ g ^ r * FRC.Shell.ofNat x = FRC.Shell.ofNat x) p = if r % (p - (1 : Nat)) = (0 : Nat) then p - (1 : Nat) else (0 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (ν θ : FRC.Shell p), (FRC.Horizon.readout ν κ θ).trace = (1 : FRC.Shell p) ∧ (FRC.Horizon.readout ν κ θ).re = FRC.Shell.ofNat ((2 : Nat) * κ + (1 : Nat)) ∧ ∀ (θ' : FRC.Shell p), FRC.Horizon.readout ν κ θ = FRC.Horizon.readout ν κ θ' → θ = θ') ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k : Nat), (1 : Nat) ≤ k → k ≤ p - (2 : Nat) → -g ^ k ≠ (0 : FRC.Shell p) ∧ -g ^ k ≠ (-1 : FRC.Shell p) :=382  @FRC.Ledger.p20043383set_option linter.defProp false in384/-- 20:F1 (p20047) — \textbf{Turing's count on the shell.} On every cell $C_y\le N^{\mathrm{crit}}_y\le\mathcal N_y$ (A7); the cell is clean when $\mathcal N_y=N^{\mathrm{crit}}_y$, and $C_y=\mathcal N_y$ certifies it, every zero simple. The shell estimates $\mathcal N$ by the comb count (Appendix~\ref{app:comb}; uncertified) and reads $C$ from the main sum's sign changes (A10), zeros on the line. An off-line zero is a phantom, $\mathcal N_y-N^{\mathrm{crit}}_y>0$. -/385def p20047 := @FRC.Ledger.p20047386set_option linter.defProp false in387/-- 20:F2 (p20081) — \textbf{The hypothesis on a hosted Carrier.} A cell is decided by the certificate of a shell reading it, an embedded Subject below the largest one, the host above; on the laboratory Carriers $233$, $30\,089$ and $2\,408\,561$ every cell of the cycle is clean, $1\,038$, $280\,186$ and $32\,984\,135$ zeros, all simple; the classical verification cleans every cell below $4.8\times10^{11}$ (A9). -/388def p20081 := @FRC.Ledger.p20081389set_option linter.defProp false in390/-- 20:F7 (p20079) — \textbf{The closure of the heights.} A height is a residue on the cycle of the shell that reads it, the largest shell is the Carrier's and there is no height beyond its cycle (A2); no embedded Subject reads the cycle whole (A4). The hypothesis of the Carrier is a statement about the residues of its cycle, one clause per residue. -/391def p20079 := @FRC.Ledger.p20079392-- end ledger predicates393394end FRC.Rh395