Rh.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Horizon3import FrcLedger.Theme.Chart4import FrcLedger.Keys.Chart5import FrcLedger.Keys.Horizon67/-!8# 20-rh — Riemann Hypothesis over Finite Holographic Substrate: the shell predicates in Lean (2026-09-19)910The exact arithmetic of the paper's block B, the constants of its Subject register, and the two character11readings of the shell theorem — rows B2, B4–B10 (B8's shell clauses), C2's identity `Λ = μ ∗ log`, C5, E1's shell12clause, E12 (i) and (iii), and E13's orthogonality, inversion and Parseval — proved for every shell: an arbitrary13finite field `F` with `4κ + 1` elements and a primitive root `g`, or `ZMod p` where the prime is needed, and, for14the analytic identities, over any integral domain or over `ℂ`; the laboratory pair `(13, 233)` of B1 decided.15Classical (tier 2) on Mathlib's hierarchy; the shell arithmetic is also in the core (`FrcCore/Rh.lean`) with no axioms.1617Since the ledger migration (task LM36, 7 October 2026) the theorems live in the themes: the exact shell arithmetic in18the horizon theme (`FrcLedger/Theme/Horizon.lean`, `FRC.HorizonML`), and the complex characters of the cycle, the19characters as eigenvectors and the von Mangoldt weight in the chart theme (`FrcLedger/Theme/Chart.lean`, `FRC.Chart`).20The old names below are aliases, and the predicate declarations are the aliases of their keys.21-/2223namespace FRC.Rh2425/-! ## Old names (ledger migration, task LM36): the theorems moved to the horizon theme (`FRC.HorizonML`) and the chart26theme (`FRC.Chart`), each under its old name -/2728open Finset2930section shell3132variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]3334/-- 20:B4 — 20-rh's name; the theorem is `FRC.HorizonML.zero_slot` (task LM36). -/35theorem zero_slot :36    (∀ k, 1 ≤ k → k ≤ Fintype.card F - 2 → ∑ x : Fˣ, ((x : F) ^ k) = 0) ∧37    ∑ x : Fˣ, ((x : F) ^ (Fintype.card F - 1)) = -1 := by38  apply FRC.HorizonML.zero_slot <;> assumption3940omit [DecidableEq F] in41/-- 20:B5 — 20-rh's name; the theorem is `FRC.HorizonML.slot_complementarity` (task LM36). -/42theorem slot_complementarity (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) :43    Set.InjOn (fun k : ℕ => -(g ^ k)) (Set.Icc 1 (Fintype.card F - 2)) ∧44    (fun k : ℕ => -(g ^ k)) '' Set.Icc 1 (Fintype.card F - 2) = {y : F | y ≠ 0 ∧ y ≠ -1} := by45  apply FRC.HorizonML.slot_complementarity <;> assumption4647end shell4849section ramanujan5051variable {R : Type*} [CommRing R] [IsDomain R]5253/-- 20:B7 — 20-rh's name; the theorem is `FRC.HorizonML.ramanujan_sum` (task LM36). -/54theorem ramanujan_sum {p : ℕ} (hp : 0 < p) {ω : R} (hω : IsPrimitiveRoot ω p) (n : ℕ) :55    (¬ p ∣ n → ∑ a ∈ Ico 1 p, ω ^ (a * n) = -1) ∧56    (p ∣ n → ∑ a ∈ Ico 1 p, ω ^ (a * n) = ((p - 1 : ℕ) : R)) := by57  apply FRC.HorizonML.ramanujan_sum <;> assumption5859end ramanujan6061section constants6263variable {F : Type*} [Field F] [Fintype F]6465/-- 20:B8, 20:B10 — 20-rh's name; the theorem is `FRC.HorizonML.half_turn` (task LM36). -/66theorem half_turn (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) :67    (2 : F) * ((2 * κ : ℕ) : F) = -1 ∧ (2 : F) * ((2 * κ + 1 : ℕ) : F) = 1 ∧68    ((2 * κ + 1 : ℕ) : F) = -((2 * κ : ℕ) : F) ∧ (2 : F)⁻¹ = ((2 * κ + 1 : ℕ) : F) := by69  apply FRC.HorizonML.half_turn <;> assumption7071/-- 20:B10 — 20-rh's name; the theorem is `FRC.HorizonML.subject_constants` (task LM36). -/72theorem subject_constants (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)73    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) :74    (2 : F) * ((2 * κ : ℕ) : F) = -1 ∧ g ^ (3 * κ) = -(g ^ κ) ∧ (g ^ (3 * κ)) ^ 2 = -1 ∧75    g ^ (2 * κ) = -1 ∧ ∀ m : ℕ, m % 2 = 1 → (g ^ m) ^ (m * (2 * κ)) = -1 := by76  apply FRC.HorizonML.subject_constants <;> assumption7778/-- 20:B10 [value] — 20-rh's name; the theorem is `FRC.HorizonML.constants13` (task LM36). -/79theorem constants13 :80    (2 : ZMod 13) * 6 = -1 ∧ (2 : ZMod 13) ^ 9 = 5 ∧ (5 : ZMod 13) ^ 2 = -1 ∧ (2 : ZMod 13) ^ 5 = 6 ∧81    (2 : ZMod 13) ^ 6 = -1 ∧ (6 : ZMod 13) ^ (5 * 6) = -1 := by82  apply FRC.HorizonML.constants13 <;> assumption8384end constants8586section extension8788variable {F : Type*} [Field F] (ν : F)8990local notation "K" => QuadraticAlgebra F ν 09192/-- 20:B9 — 20-rh's name; the theorem is `FRC.HorizonML.klein_four` (task LM36). -/93theorem klein_four (z : K) :94    star (star z) = z ∧ (1 - (1 - z)) = z ∧ star (1 - z) = 1 - star z := by95  apply FRC.HorizonML.klein_four <;> assumption9697/-- 20:B9 — 20-rh's name; the theorem is `FRC.HorizonML.fixed_frobenius` (task LM36). -/98theorem fixed_frobenius (h2 : (2 : F) ≠ 0) (z : K) : star z = z ↔ z.im = 0 := by99  apply FRC.HorizonML.fixed_frobenius <;> assumption100101/-- 20:B8, 20:B9 — 20-rh's name; the theorem is `FRC.HorizonML.trace_eq_one_iff` (task LM36). -/102theorem trace_eq_one_iff (h2 : (2 : F) ≠ 0) (z : K) :103    (QuadraticAlgebra.trace z = 1 ↔ z.re = 2⁻¹) ∧ (1 - star z = z ↔ z.re = 2⁻¹) := by104  apply FRC.HorizonML.trace_eq_one_iff <;> assumption105106/-- 20:B9 — 20-rh's name; the theorem is `FRC.HorizonML.fixed_half_turn` (task LM36). -/107theorem fixed_half_turn (h2 : (2 : F) ≠ 0) (z : K) :108    (1 - z = z ↔ z = ⟨2⁻¹, 0⟩) ∧ (z.im = 0 ∧ z.re = 2⁻¹ ↔ z = ⟨2⁻¹, 0⟩) := by109  apply FRC.HorizonML.fixed_half_turn <;> assumption110111/-- 20:B8 — 20-rh's name; the theorem is `FRC.HorizonML.norm_on_line` (task LM36). -/112theorem norm_on_line (z : K) (hz : z.re = 2⁻¹) :113    QuadraticAlgebra.norm z = (4 : F)⁻¹ - ν * z.im ^ 2 := by114  apply FRC.HorizonML.norm_on_line <;> assumption115116/-- 20:E12, 20:B8 — 20-rh's name; the theorem is `FRC.HorizonML.readout_on_line` (task LM36). -/117theorem readout_on_line (h2 : (2 : F) ≠ 0) (θ : F) :118    QuadraticAlgebra.trace (FRC.HorizonML.readout ν θ) = 1 ∧ (FRC.HorizonML.readout ν θ).re = 2⁻¹ ∧119    Function.Injective (FRC.HorizonML.readout ν) := by120  apply FRC.HorizonML.readout_on_line <;> assumption121122variable [Fintype F] [DecidableEq F]123124/-- 20:B8 — 20-rh's name; the theorem is `FRC.HorizonML.card_critical_line` (task LM36). -/125theorem card_critical_line (h2 : (2 : F) ≠ 0) :126    (univ.filter (fun z : K => QuadraticAlgebra.trace z = 1)).card = Fintype.card F := by127  apply FRC.HorizonML.card_critical_line <;> assumption128129omit [DecidableEq F] in130/-- 20:E12 — 20-rh's name; the theorem is `FRC.HorizonML.readout_slot_index` (task LM36). -/131theorem readout_slot_index (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (k : ℕ)132    (hk1 : 1 ≤ k) (hk2 : k ≤ Fintype.card F - 2) : -(g ^ k) ≠ 0 ∧ -(g ^ k) ≠ -1 := by133  apply FRC.HorizonML.readout_slot_index <;> assumption134135end extension136137section frobenius138139variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] {p : ℕ} [hp : Fact p.Prime] [CharP F p]140  (hcard : Fintype.card F = p) (ν : F) [hν : Fact (¬ IsSquare ν)]141142local notation "K" => QuadraticAlgebra F ν 0143144omit [DecidableEq F] in145include hcard in146/-- 20:B6 — 20-rh's name; the theorem is `FRC.HorizonML.frobenius_eq_star` (task LM36). -/147theorem frobenius_eq_star (z : K) : z ^ p = star z := by148  apply FRC.HorizonML.frobenius_eq_star <;> assumption149150omit [DecidableEq F] in151include hcard in152/-- 20:B6 — 20-rh's name; the theorem is `FRC.HorizonML.norm_eq_pow` (task LM36). -/153theorem norm_eq_pow (z : K) : algebraMap F K (QuadraticAlgebra.norm z) = z ^ (p + 1) := by154  apply FRC.HorizonML.norm_eq_pow <;> assumption155156include hcard in157/-- 20:B6 — 20-rh's name; the theorem is `FRC.HorizonML.phase_circle` (task LM36). -/158theorem phase_circle :159    (univ.filter (fun z : K => QuadraticAlgebra.norm z = 1)).card = p + 1 ∧160    ∀ z : K, QuadraticAlgebra.norm z = 1 → star z = z⁻¹ := by161  apply FRC.HorizonML.phase_circle <;> assumption162163omit [DecidableEq F] in164include hcard in165/-- 20:B6 — 20-rh's name; the theorem is `FRC.HorizonML.quarter_turn_off_circle` (task LM36). -/166theorem quarter_turn_off_circle (i : F) (hi : i ^ 2 = -1) :167    star (algebraMap F K i) = algebraMap F K i ∧ QuadraticAlgebra.norm (algebraMap F K i) = -1 ∧168    QuadraticAlgebra.norm (algebraMap F K i) ≠ 1 := by169  apply FRC.HorizonML.quarter_turn_off_circle <;> assumption170171end frobenius172173section spectrum174175variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]176177/-- 20:E1, 20:E12 — 20-rh's name; the theorem is `FRC.HorizonML.scale_shift` (task LM36). -/178theorem scale_shift (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (r : ℕ) :179    Function.Bijective (fun x : Fˣ => (Units.mk0 g (hg.ne_zero (Nat.sub_ne_zero_of_lt Fintype.one_lt_card))) ^ r * x) ∧180    (∀ (k : ℕ) (x : F), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧181    (univ.filter (fun x : Fˣ => g ^ r * (x : F) = x)).card =182      if (Fintype.card F - 1) ∣ r then Fintype.card F - 1 else 0 := by183  apply FRC.HorizonML.scale_shift <;> assumption184185/-- 20:E12, 20:E13 — 20-rh's name; the theorem is `FRC.HorizonML.power_characters_not_orthonormal` (task LM36). -/186theorem power_characters_not_orthonormal (h2 : (2 : F) ≠ 0) (j : ℕ) :187    ∑ x : Fˣ, ((x : F) ^ j * (x : F) ^ j) ≠ 1 := by188  apply FRC.HorizonML.power_characters_not_orthonormal <;> assumption189190omit [Fintype F] [DecidableEq F] in191/-- 20:E12, 20:E1 — 20-rh's name; the theorem is `FRC.Chart.character_eigen` (task LM36). -/192theorem character_eigen (χ : Fˣ →* ℂˣ) (g x : Fˣ) (r : ℕ) : χ (g ^ r * x) = χ g ^ r * χ x := by193  apply FRC.Chart.character_eigen <;> assumption194195end spectrum196197section characters198199open Complex200201variable {n : ℕ} [NeZero n]202203/-- 20:E13 — 20-rh's name; the theorem is `FRC.Chart.chi_orthogonal` (task LM36). -/204theorem chi_orthogonal (j k : ZMod n) :205    ∑ m, FRC.Chart.chi j m * (starRingEnd ℂ) (FRC.Chart.chi k m) = if j = k then (n : ℂ) else 0 := by206  apply FRC.Chart.chi_orthogonal <;> assumption207208/-- 20:E12, 20:E1 — 20-rh's name; the theorem is `FRC.Chart.chi_shift` (task LM36). -/209theorem chi_shift (j m : ZMod n) :210    FRC.Chart.chi j (m + 1) = ZMod.stdAddChar j * FRC.Chart.chi j m ∧211    ZMod.stdAddChar (j : ZMod n) = Complex.exp (2 * Real.pi * I * j.val / n) := by212  apply FRC.Chart.chi_shift <;> assumption213214/-- 20:E12, 20:E13 — 20-rh's name; the theorem is `FRC.Chart.chi_inversion` (task LM36). -/215theorem chi_inversion (v : ZMod n → ℂ) :216    (∀ m, v m = (n : ℂ)⁻¹ * ∑ j, FRC.Chart.coef v j * FRC.Chart.chi j m) ∧ FRC.Chart.coef v 0 = ∑ m, v m ∧217    ∀ m, v m - (n : ℂ)⁻¹ * ∑ m', v m' = (n : ℂ)⁻¹ * ∑ j ∈ univ.erase 0, FRC.Chart.coef v j * FRC.Chart.chi j m := by218  apply FRC.Chart.chi_inversion <;> assumption219220/-- 20:E13, 20:C5 — 20-rh's name; the theorem is `FRC.Chart.chi_parseval` (task LM36). -/221theorem chi_parseval (v : ZMod n → ℂ) :222    ∑ j, normSq (FRC.Chart.coef v j) = n * ∑ m, normSq (v m) := by223  apply FRC.Chart.chi_parseval <;> assumption224225/-- 20:C5 — 20-rh's name; the theorem is `FRC.Chart.flatness` (task LM36). -/226theorem flatness (u : ZMod n → ℂ) (hmean : ∑ m, u m = 0) (hu : u ≠ 0) :227    ∑ j ∈ univ.erase 0, normSq (FRC.Chart.coef u j) / (n * ∑ m, normSq (u m)) = 1 ∧228    (∑ j ∈ univ.erase 0, normSq (FRC.Chart.coef u j) / (n * ∑ m, normSq (u m))) / ((n : ℝ) - 1) = 1 / ((n : ℝ) - 1) := by229  apply FRC.Chart.flatness <;> assumption230231end characters232233section resonance234235open ArithmeticFunction236237/-- 20:C2 — 20-rh's name; the theorem is `FRC.Chart.vonMangoldt_moebius` (task LM36). -/238theorem vonMangoldt_moebius (m : ℕ) :239    vonMangoldt m = ∑ d ∈ m.divisors, (moebius d : ℝ) * Real.log ((m : ℝ) / d) ∧240    (vonMangoldt m ≠ 0 ↔ IsPrimePow m) := by241  apply FRC.Chart.vonMangoldt_moebius <;> assumption242243end resonance244245section strip246247open ComplexConjugate248249/-- 20:D8 — 20-rh's name; the theorem is `FRC.Chart.zeros_in_strip`: a nontrivial zero of `ζ` lies in the open strip250`0 < Re s < 1`, and `1 − s` and `s̄` are zeros. -/251theorem zeros_in_strip {s : ℂ} (h0 : riemannZeta s = 0) (htriv : ¬∃ n : ℕ, s = -2 * (n + 1)) (h1 : s ≠ 1) :252    0 < s.re ∧ s.re < 1 ∧ riemannZeta (1 - s) = 0 ∧ riemannZeta (conj s) = 0 :=253  FRC.Chart.zeros_in_strip h0 htriv h1254255/-- 20:F1 — 20-rh's name; the theorem is `FRC.Chart.zero_of_sign_change`: a sign change of the real completed zeta256`Re Λ(1/2 + it)` between two heights is a zero of `ζ` on the line between them (Turing's count, the analytic clause). -/257theorem zero_of_sign_change {a b : ℝ} (hab : a < b)258    (h : (completedRiemannZeta (1 / 2 + a * Complex.I)).re * (completedRiemannZeta (1 / 2 + b * Complex.I)).re < 0) :259    ∃ t : ℝ, a < t ∧ t < b ∧ riemannZeta (1 / 2 + t * Complex.I) = 0 :=260  FRC.Chart.zero_of_sign_change hab h261262end strip263264section coincidence265266/-- 20:B2 — 20-rh's name; the theorem is `FRC.HorizonML.window_readback` (task LM36). -/267theorem window_readback {q : ℕ} [NeZero q] {H : ℕ} (hH : H * H < q) :268    (∀ m, m ≤ H → ((m : ZMod q)).val = m) ∧269    ∀ a b, a ≤ H → b ≤ H → ((a : ZMod q) * b).val = a * b := by270  apply FRC.HorizonML.window_readback <;> assumption271272/-- 20:B2 — 20-rh's name; the theorem is `FRC.HorizonML.prime_iff_window_irreducible` (task LM36). -/273theorem prime_iff_window_irreducible {q : ℕ} [NeZero q] {H : ℕ} (hH : H * H < q) (m : ℕ) (hm2 : 2 ≤ m)274    (hmH : m ≤ H) :275    Nat.Prime m ↔ ¬ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ a ≤ H ∧ b ≤ H ∧ (a : ZMod q) * b = m := by276  apply FRC.HorizonML.prime_iff_window_irreducible <;> assumption277278/-- 20:B2 — 20-rh's name; the theorem is `FRC.HorizonML.sqrt_sq_lt_prime` (task LM36). -/279theorem sqrt_sq_lt_prime {p : ℕ} (hp : p.Prime) : Nat.sqrt p * Nat.sqrt p < p := by280  apply FRC.HorizonML.sqrt_sq_lt_prime <;> assumption281282end coincidence283284section lab285286/-- 20:B1 [value] — 20-rh's name; the theorem is `FRC.HorizonML.lab_pair` (task LM36). -/287theorem lab_pair :288    13 * 13 < 233 ∧ Nat.gcd 12 232 = 4 ∧ (5 : ZMod 13) ^ 2 = -1 ∧ (89 : ZMod 233) ^ 2 = -1 ∧ ¬ 12 ∣ 232 := by289  apply FRC.HorizonML.lab_pair <;> assumption290291/-- 20:B1 — 20-rh's name; the theorem is `FRC.HorizonML.no_cycle_projection` (task LM36). -/292theorem no_cycle_projection :293    ¬ ∃ f : Multiplicative (ZMod 232) →* Multiplicative (ZMod 12), Function.Surjective f := by294  apply FRC.HorizonML.no_cycle_projection <;> assumption295296end lab297298-- Ledger predicates of 20-rh (generated by make_predicates.py from docs/20-rh/20-rh-ledger.json; edit the ledger, not this section)299set_option linter.defProp false in300/-- 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). -/301def p20008 := @FRC.LedgerML.p20008302/-- 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$. -/303theorem p20009 : And (∀ {q : Nat} [@NeZero Nat (@MulZeroClass.toZero Nat Nat.instMulZeroClass) q] {H : Nat}, @LT.lt Nat instLTNat (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) H H) q → And (∀ (m : Nat), @LE.le Nat instLENat m H → @Eq Nat (@ZMod.val q (@Nat.cast (ZMod q) (@AddMonoidWithOne.toNatCast (ZMod q) (@AddGroupWithOne.toAddMonoidWithOne (ZMod q) (@Ring.toAddGroupWithOne (ZMod q) (@CommRing.toRing (ZMod q) (ZMod.commRing q))))) m)) m) (∀ (a b : Nat), @LE.le Nat instLENat a H → @LE.le Nat instLENat b H → @Eq Nat (@ZMod.val q (@HMul.hMul (ZMod q) (ZMod q) (ZMod q) (@instHMul (ZMod q) (@Distrib.toMul (ZMod q) (@instDistribOfSemiring (ZMod q) (@CommSemiring.toSemiring (ZMod q) (@CommRing.toCommSemiring (ZMod q) (ZMod.commRing q)))))) (@Nat.cast (ZMod q) (@AddMonoidWithOne.toNatCast (ZMod q) (@AddGroupWithOne.toAddMonoidWithOne (ZMod q) (@Ring.toAddGroupWithOne (ZMod q) (@CommRing.toRing (ZMod q) (ZMod.commRing q))))) a) (@Nat.cast (ZMod q) (@AddMonoidWithOne.toNatCast (ZMod q) (@AddGroupWithOne.toAddMonoidWithOne (ZMod q) (@Ring.toAddGroupWithOne (ZMod q) (@CommRing.toRing (ZMod q) (ZMod.commRing q))))) b))) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) a b))) (And (∀ {q : Nat} [@NeZero Nat (@MulZeroClass.toZero Nat Nat.instMulZeroClass) q] {H : Nat}, @LT.lt Nat instLTNat (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) H H) q → ∀ (m : Nat), @LE.le Nat instLENat (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) m → @LE.le Nat instLENat m H → Iff (Nat.Prime m) (Not (∃ a b, And (@LE.le Nat instLENat (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) a) (And (@LE.le Nat instLENat (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) b) (And (@LE.le Nat instLENat a H) (And (@LE.le Nat instLENat b H) (@Eq (ZMod q) (@HMul.hMul (ZMod q) (ZMod q) (ZMod q) (@instHMul (ZMod q) (@Distrib.toMul (ZMod q) (@instDistribOfSemiring (ZMod q) (@CommSemiring.toSemiring (ZMod q) (@CommRing.toCommSemiring (ZMod q) (ZMod.commRing q)))))) (@Nat.cast (ZMod q) (@AddMonoidWithOne.toNatCast (ZMod q) (@AddGroupWithOne.toAddMonoidWithOne (ZMod q) (@Ring.toAddGroupWithOne (ZMod q) (@CommRing.toRing (ZMod q) (ZMod.commRing q))))) a) (@Nat.cast (ZMod q) (@AddMonoidWithOne.toNatCast (ZMod q) (@AddGroupWithOne.toAddMonoidWithOne (ZMod q) (@Ring.toAddGroupWithOne (ZMod q) (@CommRing.toRing (ZMod q) (ZMod.commRing q))))) b)) (@Nat.cast (ZMod q) (@AddMonoidWithOne.toNatCast (ZMod q) (@AddGroupWithOne.toAddMonoidWithOne (ZMod q) (@Ring.toAddGroupWithOne (ZMod q) (@CommRing.toRing (ZMod q) (ZMod.commRing q))))) m)))))))) (∀ {p : Nat}, Nat.Prime p → @LT.lt Nat instLTNat (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) p.sqrt p.sqrt) p)) :=304  @FRC.LedgerML.p20009305set_option linter.defProp false in306/-- 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. -/307def p20011 := @FRC.LedgerML.p20011308/-- 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. -/309theorem p20012 : ∀ {F : Type u_1} [Field F] [Fintype F] (g : F), 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 | y ≠ (0 : F) ∧ y ≠ (-1 : F)} :=310  @FRC.LedgerML.p20012311set_option linter.defProp false in312/-- 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}$. -/313def p20013 := @FRC.LedgerML.p20013314/-- 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. -/315theorem p20014 : ∀ {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ}, (0 : ℕ) < p → ∀ {ω : R}, IsPrimitiveRoot ω p → ∀ (n : ℕ), (¬p ∣ n → ∑ a ∈ Finset.Ico (1 : ℕ) p, ω ^ (a * n) = (-1 : R)) ∧ (p ∣ n → ∑ a ∈ Finset.Ico (1 : ℕ) p, ω ^ (a * n) = ↑(p - (1 : ℕ))) :=316  @FRC.LedgerML.p20014317set_option linter.defProp false in318/-- 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]. -/319def p20015 := @FRC.LedgerML.p20015320/-- 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. -/321theorem p20016 : (∀ {F : Type u_1} [Field F] (ν : F) (z : QuadraticAlgebra F ν (0 : F)), star (star z) = z ∧ (1 : QuadraticAlgebra F ν (0 : F)) - ((1 : QuadraticAlgebra F ν (0 : F)) - z) = z ∧ star ((1 : QuadraticAlgebra F ν (0 : F)) - z) = (1 : QuadraticAlgebra F ν (0 : F)) - star z) ∧ (∀ {F : Type u_2} [Field F] (ν : F), (2 : F) ≠ (0 : F) → ∀ (z : QuadraticAlgebra F ν (0 : F)), star z = z ↔ z.im = (0 : F)) ∧ (∀ {F : Type u_3} [Field F] (ν : F), (2 : F) ≠ (0 : F) → ∀ (z : QuadraticAlgebra F ν (0 : F)), (QuadraticAlgebra.trace z = (1 : F) ↔ z.re = (2 : F)⁻¹) ∧ ((1 : QuadraticAlgebra F ν (0 : F)) - star z = z ↔ z.re = (2 : F)⁻¹)) ∧ ∀ {F : Type u_4} [Field F] (ν : F), (2 : F) ≠ (0 : F) → ∀ (z : QuadraticAlgebra F ν (0 : F)), ((1 : QuadraticAlgebra F ν (0 : F)) - z = z ↔ z = { re := (2 : F)⁻¹, im := (0 : F) }) ∧ (z.im = (0 : F) ∧ z.re = (2 : F)⁻¹ ↔ z = { re := (2 : F)⁻¹, im := (0 : F) }) :=322  @FRC.LedgerML.p20016323/-- 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$. -/324theorem p20017 : (∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → (2 : F) * ↑((2 : ℕ) * κ) = (-1 : F) ∧ g ^ ((3 : ℕ) * κ) = -g ^ κ ∧ (g ^ ((3 : ℕ) * κ)) ^ (2 : ℕ) = (-1 : F) ∧ g ^ ((2 : ℕ) * κ) = (-1 : F) ∧ ∀ (m : ℕ), m % (2 : ℕ) = (1 : ℕ) → (g ^ m) ^ (m * ((2 : ℕ) * κ)) = (-1 : F)) ∧ (2 : ZMod (13 : ℕ)) * (6 : ZMod (13 : ℕ)) = (-1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (9 : ℕ) = (5 : ZMod (13 : ℕ)) ∧ (5 : ZMod (13 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (5 : ℕ) = (6 : ZMod (13 : ℕ)) ∧ (2 : ZMod (13 : ℕ)) ^ (6 : ℕ) = (-1 : ZMod (13 : ℕ)) ∧ (6 : ZMod (13 : ℕ)) ^ ((5 : ℕ) * (6 : ℕ)) = (-1 : ZMod (13 : ℕ)) :=325  @FRC.LedgerML.p20017326set_option linter.defProp false in327/-- 20:D8 (p20080) — The strip: the Euler product excludes zeros with real part at least one, and the functional equation confines the nontrivial zeros to the open strip in Klein-four orbits of size two on the line and four off it; the Davenport--Heilbronn vector, without the product, is not multiplicative and has an off-line zero. No core witness: the statement is analytic. -/328def p20080 := @FRC.LedgerML.p20080329set_option linter.defProp false in330/-- 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. -/331def p20032 := @FRC.LedgerML.p20032332set_option linter.defProp false in333/-- 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. -/334def p20043 := @FRC.LedgerML.p20043335set_option linter.defProp false in336/-- 20:E13 (p20044) — Shell-basis completeness is not a clause of E12: the $\p-1$ complex characters are an orthogonal basis of $\mathbb C^{\Fx{\p}}$ ($\lVert\chi_j\rVert^{2}=\p-1$; finite Parseval), true of every vector, the trivial character carrying the mean $\psi(\p-1)/(\p-1)$; the $\Fp$-valued power characters are never orthonormal and do not expand $v$; completeness for the zero set of $\zeta$ is D5, a different clause. -/337def p20044 := @FRC.LedgerML.p20044338set_option linter.defProp false in339/-- 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$. -/340def p20047 := @FRC.LedgerML.p20047341-- end ledger predicates342343end FRC.Rh344