Theme/Zeros.lean — FrcCore

1import FrcCore.Theme.Horizon23/-!4# FrcCore.Theme.Zeros — the horizon theme's second file: the zeros of the shell (20-rh's rewrite, 17 October 2026; the5drive theorem and the circle, 18 October 2026)67The critical line as the energy domain (20:B12): the readout of the mode `k` at `θ = −g^k`, the drive about the8centre as the step `k ↦ k + 1`, the half-turn and the conjugation as the step `k ↦ k + π` across the line, the norm a9function of `k` alone, even under the half-turn. The dual of a vector with the Parseval identity (20:E13, the finite10Parseval identity, self-pairing `−1`); the parity `W² = −J` and the explicit formula, on the cycle and along the11meridian with the inversion on the residues (20:E14). The two agreement loci in the invariant-line form (20:B9): among12the `p(p + 1)` affine lines of the extension, `H_b = {Im z = b}` and `S_{c,a} = {Re z = a + c·Im z}`, conjugation keeps13`H_b` exactly when `b = 0` and `S_{c,a}` exactly when `c = 0`, the half-turn keeps `H_b` exactly when `b = 0` and14`S_{c,a}` exactly when `a = 2⁻¹`, so exactly two lines are kept by both, the meridian `H_0` and the critical line15`S_{0,2⁻¹}`. Frame coincidence on the critical line for every label of the Subject (20:B13): on two shells `p ≤ Ω` every16label `1 ≤ θ ≤ p − 2` reads back as the integer `θ` in both frames and is the readout of a nontrivial mode on the critical17line of each. These, with `readout_on_line` and `off_line_unregistered` (a point off both lines lies on no line kept by18both involutions), are the witnesses of the paper's Theorem noline (20:F10). The drive as an operator (20:E15, the19revision of 18 October 2026): orthogonal for the pairing of the cycle, its spectrum the `n` eigenvalues `g^k`, simple,20the readout minus the eigenvalue, the half-turn its negation, the modes isotropic; and the energy domain as a circle21(20:B14): the Cayley image `z/(1 − z)` of the critical line, where the norm does not vanish, of norm one, never `−1`,22injective, the centre at `1`, the conjugation the inversion. The declarations keep23the theme's namespace `FRC.Horizon`; the file is the theme's second core file, as `Theme/Ladder.lean` is its third,24within the file budget of gate G10. No axioms.25-/2627namespace FRC.Horizon2829open FRC.Shell FRC.Shell.Frame30open FRC.Extension (Ext)3132variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}3334section rewrite202610173536/-- 20:E12 (i) — the dual of a vector on the cycle: `v̂(k) = Σ_{l<n} v_l (g^l)^k`, the shell Fourier transform `W` on the37phase cycle (6:B5); the mode coefficient of `mode_expansion` is `c_k = −v̂(−k)`. -/38def dual (g : Shell p) (v : Nat → Shell p) (k : Nat) : Shell p :=39  sumRange (fun l => v l * (g ^ l) ^ k) (p - 1)4041/-- A product of two sums as a double sum: `(Σ_l a_l) (Σ_m b_m) = Σ_l Σ_m a_l b_m`. -/42theorem sum_mul_sum (a b : Nat → Shell p) (n m : Nat) :43    sumRange a n * sumRange b m = sumRange (fun l => sumRange (fun j => a l * b j) m) n := by44  rw [← sum_mul_right]45  apply sum_congr; intro l _46  exact (sum_mul_left b (a l) m).symm4748/-- 20:E12 (ii), 20:E13 — the Parseval identity on the cycle: `Σ_{k<n} v̂(k) c_k = Σ_{l<n} v_l²` with `c_k = −v̂(−k)` the mode49coefficient, that is `Σ_k v̂(k) v̂(−k) = −Σ_l v_l²`: the finite Parseval identity of the cycle, the self-pairing `−1` of50the power characters in place of the complex norm. -/51theorem parseval_cycle (F : Frame p κ g) (v : Nat → Shell p) :52    sumRange (fun k => dual g v k * modeCoeff g v k) (p - 1) = sumRange (fun l => v l * v l) (p - 1) := by53  have h1 : ∀ k, k < p - 1 → dual g v k * modeCoeff g v k54      = sumRange (fun l => sumRange (fun m => v l * v m * (g ^ (k * l) * -(g ^ ((p - 1 - m) * k)))) (p - 1)) (p - 1) := by55    intro k _56    unfold dual modeCoeff57    rw [sum_mul_sum]58    apply sum_congr; intro l _59    apply sum_congr; intro m _60    rw [← pow_mul, Nat.mul_comm l k]61    calc v l * g ^ (k * l) * (v m * -(g ^ ((p - 1 - m) * k)))62        = v l * (g ^ (k * l) * (v m * -(g ^ ((p - 1 - m) * k)))) := mul_assoc _ _ _63      _ = v l * (g ^ (k * l) * v m * -(g ^ ((p - 1 - m) * k))) := by rw [mul_assoc (g ^ (k * l))]64      _ = v l * (v m * g ^ (k * l) * -(g ^ ((p - 1 - m) * k))) := by rw [mul_comm (g ^ (k * l)) (v m)]65      _ = v l * (v m * (g ^ (k * l) * -(g ^ ((p - 1 - m) * k)))) := by rw [mul_assoc (v m)]66      _ = v l * v m * (g ^ (k * l) * -(g ^ ((p - 1 - m) * k))) := (mul_assoc _ _ _).symm67  rw [sum_congr (p - 1) h1,68    sum_comm (fun k l => sumRange (fun m => v l * v m * (g ^ (k * l) * -(g ^ ((p - 1 - m) * k)))) (p - 1)) (p - 1) (p - 1)]69  apply sum_congr; intro l hl70  rw [sum_comm (fun k m => v l * v m * (g ^ (k * l) * -(g ^ ((p - 1 - m) * k)))) (p - 1) (p - 1)]71  have h3 : ∀ m, m < p - 1 → sumRange (fun k => v l * v m * (g ^ (k * l) * -(g ^ ((p - 1 - m) * k)))) (p - 1)72      = v l * v m * (if l = m then 1 else 0) := fun m hm => by73    rw [sum_mul_left, F.dft_inverse hl hm]74  rw [sum_congr (p - 1) h3, sum_eq_single hl (fun m _ hne => by rw [ite_eq_right (fun e => hne e.symm), mul_zero]),75    ite_eq_left rfl, mul_one]7677/-- 20:E14, 20:E12 (v) — the explicit formula on the cycle: the count of `v` over the first `x` points of the cycle is the mode78sum, `Σ_{j<x} v_j = Σ_{k<n} c_k S_k(x)` with `S_k(x) = Σ_{j<x} (g^j)^k` the cumulative read of the mode `k`, and the79constant mode's read is the main term, `S_0(x) = x`. -/80theorem explicit_formula_cycle (F : Frame p κ g) (v : Nat → Shell p) {x : Nat} (hx : x ≤ p - 1) :81    sumRange v x = sumRange (fun k => modeCoeff g v k * sumRange (fun j => (g ^ j) ^ k) x) (p - 1) ∧82    sumRange (fun j => (g ^ j) ^ 0) x = ofNat x := by83  refine ⟨?_, ?_⟩84  · have h1 : sumRange v x = sumRange (fun j => sumRange (fun k => modeCoeff g v k * (g ^ j) ^ k) (p - 1)) x :=85      sum_congr x (fun j hj => mode_expansion F v (Nat.lt_of_lt_of_le hj hx))86    rw [h1, sum_comm (fun j k => modeCoeff g v k * (g ^ j) ^ k) (p - 1) x]87    apply sum_congr; intro k _88    exact sum_mul_left (fun j => (g ^ j) ^ k) (modeCoeff g v k) x89  · have e : ∀ j, j < x → (g ^ j) ^ 0 = (1 : Shell p) := fun j _ => rfl90    rw [sum_congr x e, sum_const, mul_one]9192/-- 20:E14, 20:E12 (iv) — the transform's square is the parity: `(W²)_{jl} = Σ_k g^{jk} g^{kl}` is `−1` when `j + l ≡ 0`93and `0` otherwise, `W² = −J`; with `F = iW` and `i² = −1`, `F² = J` and `F⁴ = 1` (6:B5). -/94theorem transform_square (F : Frame p κ g) (j l : Nat) :95    sumRange (fun k => g ^ (j * k) * g ^ (k * l)) (p - 1) = if (j + l) % (p - 1) = 0 then -1 else 0 := by96  have hterm : ∀ k, k < p - 1 → g ^ (j * k) * g ^ (k * l) = (g ^ ((j + l) % (p - 1))) ^ k := fun k _ => by97    rw [← pow_add, Nat.mul_comm k l, ← Nat.add_mul, pow_mul, F.pow_mod (j + l)]98  rw [sum_congr (p - 1) hterm]99  exact match Nat.decEq ((j + l) % (p - 1)) 0 with100    | .isTrue e => by101        rw [ite_eq_left e, e, pow_zero]102        have e1 : ∀ k, k < p - 1 → (1 : Shell p) ^ k = 1 := fun k _ => one_pow k103        rw [sum_congr (p - 1) e1, sum_const, mul_one, F.ofNat_n]104    | .isFalse ne => by105        rw [ite_eq_right ne]106        exact (F.principal_root _ (Nat.pos_of_ne_zero ne) (Nat.mod_lt _ F.n_pos)).2.1107108/-- 20:B12 (ii) — the drive about the centre: on the critical line the dilation `z ↦ 2⁻¹ + g (z − 2⁻¹)` carries the109readout of the mode `k` to the readout of the mode `k + 1`. -/110theorem drive_on_line (ν : Shell p) (κ k : Nat) :111    (⟨(readout ν κ (-(g ^ k))).re, g * (readout ν κ (-(g ^ k))).im⟩ : Ext p ν) = readout ν κ (-(g ^ (k + 1))) := by112  refine Ext.ext ?_ ?_113  · rfl114  · show g * -(g ^ k) = -(g ^ (k + 1))115    rw [← mul_neg, mul_comm, ← pow_succ]116117/-- 20:B12 (iii) — the half-turn `ρ : z ↦ 1 − z` and the conjugation agree on the critical line and carry the readout118of the mode `k` to the readout of the mode `k + π`, `π = 2κ`: the half-turn of the frequency cycle. -/119theorem reflection_on_line (F : Frame p κ g) (ν : Shell p) (k : Nat) :120    rho (readout ν κ (-(g ^ k))) = readout ν κ (-(g ^ (k + 2 * κ))) ∧121    Ext.conj (readout ν κ (-(g ^ k))) = readout ν κ (-(g ^ (k + 2 * κ))) := by122  have hpow : g ^ (k + 2 * κ) = -(g ^ k) := by123    rw [FRC.Shell.pow_add, F.half_period, ← mul_neg, mul_one]124  have hre : (1 : Shell p) + -(ofNat (2 * κ + 1)) = ofNat (2 * κ + 1) := by125    have h2 : (ofNat (2 * κ + 1) : Shell p) + ofNat (2 * κ + 1) = 1 := by126      rw [← two_mul', (half_inverse F).1]127    calc (1 : Shell p) + -(ofNat (2 * κ + 1))128        = (ofNat (2 * κ + 1) + ofNat (2 * κ + 1)) + -(ofNat (2 * κ + 1)) := by rw [h2]129      _ = ofNat (2 * κ + 1) := by rw [add_assoc, add_neg, add_zero]130  refine ⟨Ext.ext hre ?_, Ext.ext rfl ?_⟩131  · show - -(g ^ k) = -(g ^ (k + 2 * κ))132    rw [hpow, neg_neg]133  · show - -(g ^ k) = -(g ^ (k + 2 * κ))134    rw [hpow, neg_neg]135136/-- 20:B12 (iv) — the norm on the critical line (the paper's `N(z)`, the Hermitian form) is a function of the frequency137coordinate alone and is even under the half-turn: `N(z_k) = N(z_{k+π})`; the declaration keeps its name. -/138theorem line_energy_even (F : Frame p κ g) (ν : Shell p) (k : Nat) :139    Ext.norm (readout ν κ (-(g ^ k))) = Ext.norm (readout ν κ (-(g ^ (k + 2 * κ)))) := by140  have hpow : g ^ (k + 2 * κ) = -(g ^ k) := by141    rw [FRC.Shell.pow_add, F.half_period, ← mul_neg, mul_one]142  show ofNat (2 * κ + 1) * ofNat (2 * κ + 1) + -(ν * (-(g ^ k) * -(g ^ k))) =143    ofNat (2 * κ + 1) * ofNat (2 * κ + 1) + -(ν * (-(g ^ (k + 2 * κ)) * -(g ^ (k + 2 * κ))))144  rw [hpow, neg_neg, neg_mul_neg]145146/-- 20:B9, 20:F10, the invariant-line form — the affine lines of the extension are `H_b = {Im z = b}` (`p` lines) and147`S_{c,a} = {Re z = a + c·Im z}` (`p²` lines). Conjugation keeps `H_b` exactly when `b = 0` (the meridian) and `S_{c,a}`148exactly when `c = 0` (the lines of direction `η`); the half-turn keeps `H_b` exactly when `b = 0` and `S_{c,a}` exactly149when `a = 2⁻¹` (the lines through the centre). Hence a line kept by both is the meridian `H_0` or the critical line150`S_{0,2⁻¹}`: exactly two. -/151theorem invariant_lines (F : Frame p κ g) (ν : Shell p) :152    (∀ b : Shell p, (∀ z : Ext p ν, z.im = b → (Ext.conj z).im = b) ↔ b = 0) ∧153    (∀ c a : Shell p, (∀ z : Ext p ν, z.re = a + z.im * c → (Ext.conj z).re = a + (Ext.conj z).im * c) ↔ c = 0) ∧154    (∀ b : Shell p, (∀ z : Ext p ν, z.im = b → (rho z).im = b) ↔ b = 0) ∧155    (∀ c a : Shell p, (∀ z : Ext p ν, z.re = a + z.im * c → (rho z).re = a + (rho z).im * c) ↔156      a = ofNat (2 * κ + 1)) ∧157    (∀ b : Shell p, (∀ z : Ext p ν, z.im = b → (Ext.conj z).im = b) → (∀ z : Ext p ν, z.im = b → (rho z).im = b) →158      b = 0) ∧159    (∀ c a : Shell p, (∀ z : Ext p ν, z.re = a + z.im * c → (Ext.conj z).re = a + (Ext.conj z).im * c) →160      (∀ z : Ext p ν, z.re = a + z.im * c → (rho z).re = a + (rho z).im * c) → c = 0 ∧ a = ofNat (2 * κ + 1)) := by161  have hH : ∀ b : Shell p, (∀ z : Ext p ν, z.im = b → (Ext.conj z).im = b) ↔ b = 0 := fun b => by162    constructor163    · intro h164      have := h ⟨0, b⟩ rfl165      exact F.eq_zero_of_eq_neg this.symm166    · intro hb z hz167      show -z.im = b168      rw [hz, hb, neg_zero]169  have hS : ∀ c a : Shell p, (∀ z : Ext p ν, z.re = a + z.im * c → (Ext.conj z).re = a + (Ext.conj z).im * c) ↔ c = 0 :=170    fun c a => by171    constructor172    · intro h173      have := h ⟨a + 1 * c, 1⟩ rfl174      have h1 : a + 1 * c = a + -1 * c := this175      have h2 : 1 * c = -1 * c := by176        apply add_right_cancel (c := a)177        rw [add_comm (1 * c) a, add_comm (-1 * c) a]178        exact h1179      rw [one_mul, neg_one_mul] at h2180      exact F.eq_zero_of_eq_neg h2181    · intro hc z hz182      show z.re = a + -z.im * c183      rw [hc, mul_zero, add_zero] at hz184      rw [hc, mul_zero, add_zero]185      exact hz186  have hRH : ∀ b : Shell p, (∀ z : Ext p ν, z.im = b → (rho z).im = b) ↔ b = 0 := fun b => by187    constructor188    · intro h189      have := h ⟨0, b⟩ rfl190      exact F.eq_zero_of_eq_neg this.symm191    · intro hb z hz192      show -z.im = b193      rw [hz, hb, neg_zero]194  have hRS : ∀ c a : Shell p, (∀ z : Ext p ν, z.re = a + z.im * c → (rho z).re = a + (rho z).im * c) ↔195      a = ofNat (2 * κ + 1) := fun c a => by196    have hinv : (2 : Shell p) * ofNat (2 * κ + 1) = 1 := (half_inverse F).1197    constructor198    · intro h199      have := h ⟨a + 0 * c, 0⟩ rfl200      have h1 : 1 + -(a + 0 * c) = a + -0 * c := this201      rw [zero_mul, add_zero, neg_zero, zero_mul, add_zero] at h1202      apply F.mul_left_cancel F.two_ne_zero203      rw [hinv, two_mul']204      calc a + a = (1 + -a) + a := by rw [h1]205        _ = 1 := by rw [add_assoc, neg_add, add_zero]206    · intro ha z hz207      show 1 + -z.re = a + -z.im * c208      have h2 : (1 : Shell p) = a + a := by rw [ha, ← two_mul', hinv]209      rw [hz, h2, neg_add_rev, ← add_assoc, add_assoc a a, add_neg, add_zero, ← neg_mul]210  refine ⟨hH, hS, hRH, hRS, fun b h1 _ => (hH b).1 h1, fun c a h1 h2 => ⟨(hS c a).1 h1, (hRS c a).1 h2⟩⟩211212/-- 20:F10 (iii) — a point of the framed plane off both lines (`Im z ≠ 0` and `Re z ≠ 2⁻¹`) lies on no line kept by213both involutions: a horizontal line `H_b` through it kept by both has `b = 0`, against `Im z ≠ 0`; a line `S_{c,a}`214through it kept by both has `c = 0` and `a = 2⁻¹`, so `Re z = 2⁻¹`, against the hypothesis. The clause of Theorem noline215that the python check A18 tests point by point, derived from `invariant_lines`. -/216theorem off_line_unregistered (F : Frame p κ g) (ν : Shell p) (z : Ext p ν) (hz1 : z.im ≠ 0)217    (hz2 : z.re ≠ ofNat (2 * κ + 1)) :218    (∀ b : Shell p, z.im = b → (∀ w : Ext p ν, w.im = b → (Ext.conj w).im = b) →219      (∀ w : Ext p ν, w.im = b → (rho w).im = b) → False) ∧220    (∀ c a : Shell p, z.re = a + z.im * c →221      (∀ w : Ext p ν, w.re = a + w.im * c → (Ext.conj w).re = a + (Ext.conj w).im * c) →222      (∀ w : Ext p ν, w.re = a + w.im * c → (rho w).re = a + (rho w).im * c) → False) := by223  obtain ⟨-, -, -, -, h5, h6⟩ := invariant_lines F ν224  refine ⟨fun b hb hc hr => hz1 (hb.trans (h5 b hc hr)), fun c a hz hc hr => ?_⟩225  obtain ⟨hc0, ha⟩ := h6 c a hc hr226  apply hz2227  rw [hz, hc0, mul_zero, add_zero, ha]228229230/-! ### The dual on the residues, the explicit formula along the meridian, and the zeros of every label231(20:E14, 20:B13, 20:F10; the audit of 17 October 2026) -/232233/-- Fermat's inverse: a nonzero residue `y` has `y · y^{p−2} = y^{p−1} = 1`. -/234theorem pow_pred_inv (F : Frame p κ g) {y : Shell p} (hy : y ≠ 0) : y * y ^ (p - 2) = 1 := by235  have hp : p - 1 = (p - 2) + 1 := by236    have := F.one_lt_p237    match p, this with238    | k + 2, _ => rfl239  match F.eq_pow_of_ne_zero hy with240  | ⟨m, _, e⟩ =>241    rw [mul_comm, ← pow_succ, ← hp, ← e, pow_mul_comm, F.pow_n, one_pow]242243/-- 20:E14 — the geometric sum of a nonzero residue over the cycle, the self-pairing of the modes: `Σ_{k<p−1} u^k` is244`−1` when `u = 1` and `0` otherwise. -/245theorem geom_sum_unit (F : Frame p κ g) {u : Shell p} (hu : u ≠ 0) :246    sumRange (fun k => u ^ k) (p - 1) = if u = 1 then -1 else 0 := by247  match F.eq_pow_of_ne_zero hu with248  | ⟨m, hm, e⟩ =>249    rw [← e]250    match m, hm with251    | 0, _ =>252      rw [pow_zero, ite_eq_left rfl]253      have h1 : ∀ k, k < p - 1 → (fun k => (1 : Shell p) ^ k) k = (fun _ => (1 : Shell p)) k := fun k _ => one_pow k254      rw [sum_congr (p - 1) h1, sum_const, mul_one, F.ofNat_n]255    | m + 1, hm =>256      have hne : g ^ (m + 1) ≠ 1 := fun h1 => by257        have := F.pow_inj hm (Nat.lt_of_le_of_lt (Nat.zero_le _) hm) (h1.trans (pow_zero g).symm)258        exact Nat.succ_ne_zero m this259      rw [ite_eq_right hne]260      exact (F.principal_root (m + 1) (Nat.succ_pos m) hm).2.1261262/-- 20:E14 — the dual of a vector `w` on the nonzero residues (`w y` its value at the residue `y`, `1 ≤ y ≤ p − 1`):263`ŵ(k) = Σ_{y≠0} w(y) y^k`, the power sum of Theorem hp (i). -/264def dualRes (w : Nat → Shell p) (k : Nat) : Shell p :=265  sumRange (fun l => w (l + 1) * (ofNat (l + 1) : Shell p) ^ k) (p - 1)266267/-- 20:E14, 20:E12 (i) — the inversion on the residues: `w(y) = −Σ_{k<p−1} ŵ(k) y^{−k}` with `y^{−1} = y^{p−2}`, the sign the268self-pairing `−1` of the power characters (`geom_sum_unit`). -/269theorem inversion_res (F : Frame p κ g) (w : Nat → Shell p) {y : Nat} (hy0 : 0 < y) (hy : y < p) :270    w y = -(sumRange (fun k => dualRes w k * ((ofNat y : Shell p) ^ (p - 2)) ^ k) (p - 1)) := by271  have hyv : (ofNat y : Shell p).val = y := by rw [val_ofNat, FRC.Nat.mod_eq_of_lt hy]272  have hy' : (ofNat y : Shell p) ≠ 0 := fun h0 => by273    have := congrArg Shell.val h0274    rw [hyv, val_zero] at this275    exact Nat.ne_of_gt hy0 this276  have hyi : (ofNat y : Shell p) * (ofNat y : Shell p) ^ (p - 2) = 1 := pow_pred_inv F hy'277  have hyi' : (ofNat y : Shell p) ^ (p - 2) ≠ 0 := fun h0 => by278    rw [h0, mul_zero] at hyi279    exact F.one_ne_zero hyi.symm280  -- the double sum, summed first over the modes: `Σ_l w(l+1) Σ_k (x_l y⁻¹)^k`281  have h1 : sumRange (fun k => dualRes w k * ((ofNat y : Shell p) ^ (p - 2)) ^ k) (p - 1)282      = sumRange (fun l => w (l + 1) * sumRange (fun k => ((ofNat (l + 1) : Shell p) * (ofNat y : Shell p) ^ (p - 2)) ^ k) (p - 1)) (p - 1) := by283    have e : ∀ k, k < p - 1 → (fun k => dualRes w k * ((ofNat y : Shell p) ^ (p - 2)) ^ k) k284        = (fun k => sumRange (fun l => w (l + 1) * ((ofNat (l + 1) : Shell p) * (ofNat y : Shell p) ^ (p - 2)) ^ k) (p - 1)) k := by285      intro k _286      show dualRes w k * ((ofNat y : Shell p) ^ (p - 2)) ^ k = _287      unfold dualRes288      rw [← sum_mul_right]289      apply sum_congr; intro l _290      rw [mul_pow, mul_assoc]291    rw [sum_congr (p - 1) e, sum_comm (fun k l => w (l + 1) * ((ofNat (l + 1) : Shell p) * (ofNat y : Shell p) ^ (p - 2)) ^ k) (p - 1) (p - 1)]292    apply sum_congr; intro l _293    exact sum_mul_left (fun k => ((ofNat (l + 1) : Shell p) * (ofNat y : Shell p) ^ (p - 2)) ^ k) (w (l + 1)) (p - 1)294  -- the inner sum is `−1` at the residue `y` and `0` elsewhere295  have h2 : ∀ l, l < p - 1 → (fun l => w (l + 1) * sumRange (fun k => ((ofNat (l + 1) : Shell p) * (ofNat y : Shell p) ^ (p - 2)) ^ k) (p - 1)) l296      = (fun l => if l = y - 1 then -(w y) else (0 : Shell p)) l := by297    intro l hl298    show w (l + 1) * sumRange (fun k => ((ofNat (l + 1) : Shell p) * (ofNat y : Shell p) ^ (p - 2)) ^ k) (p - 1)299      = if l = y - 1 then -(w y) else (0 : Shell p)300    have hlp : l + 1 < p := by301      have h : l + 1 < p - 1 + 1 := Nat.succ_lt_succ hl302      rw [FRC.Nat.sub_add_cancel Pos.pos] at h303      exact h304    have hl1 : (ofNat (l + 1) : Shell p) ≠ 0 := fun h0 => by305      have := congrArg Shell.val h0306      rw [val_ofNat, val_zero, FRC.Nat.mod_eq_of_lt hlp] at this307      exact Nat.succ_ne_zero l this308    rw [geom_sum_unit F (F.mul_ne_zero hl1 hyi')]309    match Nat.decEq l (y - 1) with310    | isTrue hly =>311      have hly' : l + 1 = y := by rw [hly]; exact FRC.Nat.sub_add_cancel hy0312      rw [ite_eq_left hly, hly', ite_eq_left hyi, ← mul_neg, mul_one]313    | isFalse hly =>314      rw [ite_eq_right hly]315      have hne : (ofNat (l + 1) : Shell p) * (ofNat y : Shell p) ^ (p - 2) ≠ 1 := fun h1 => by316        have hx : (ofNat (l + 1) : Shell p) = ofNat y := by317          calc (ofNat (l + 1) : Shell p) = ofNat (l + 1) * ((ofNat y : Shell p) * (ofNat y : Shell p) ^ (p - 2)) := by rw [hyi, mul_one]318            _ = (ofNat (l + 1) * (ofNat y : Shell p) ^ (p - 2)) * ofNat y := by rw [mul_assoc, mul_comm ((ofNat y : Shell p) ^ (p - 2)), ← mul_assoc]319            _ = ofNat y := by rw [h1, one_mul]320        have hv := congrArg Shell.val hx321        rw [val_ofNat, val_ofNat, FRC.Nat.mod_eq_of_lt hy, FRC.Nat.mod_eq_of_lt hlp] at hv322        exact hly (by rw [← hv]; rfl)323      rw [ite_eq_right hne, mul_zero]324  have hy1 : y - 1 < p - 1 := by325    apply Nat.lt_of_succ_lt_succ326    show y - 1 + 1 < p - 1 + 1327    rw [FRC.Nat.sub_add_cancel hy0, FRC.Nat.sub_add_cancel Pos.pos]328    exact hy329  have h3 : ∀ l, l < p - 1 → l ≠ y - 1 → (fun l => if l = y - 1 then -(w y) else (0 : Shell p)) l = 0 :=330    fun l _ hne => ite_eq_right hne331  rw [h1, sum_congr (p - 1) h2, sum_eq_single hy1 h3, ite_eq_left rfl, neg_neg]332333/-- The cumulative read of the mode `k` along the meridian, `S_k(x) = Σ_{y≤x} y^{−k}` with `y^{−1} = y^{p−2}`. -/334def meridianRead (k x : Nat) : Shell p :=335  sumRange (fun l => ((ofNat (l + 1) : Shell p) ^ (p - 2)) ^ k) x336337/-- 20:E14 — the explicit formula along the meridian: for `x ≤ p − 1` the count of `w` over the positions `1, …, x` is338the mode sum, `Σ_{y≤x} w(y) = −Σ_{k<p−1} ŵ(k) S_k(x)`, and the constant mode's read is the main term, `S_0(x) = x`. -/339theorem explicit_formula_meridian (F : Frame p κ g) (w : Nat → Shell p) {x : Nat} (hx : x ≤ p - 1) :340    sumRange (fun l => w (l + 1)) x = -(sumRange (fun k => dualRes w k * (meridianRead k x : Shell p)) (p - 1)) ∧341    (meridianRead 0 x : Shell p) = ofNat x := by342  refine ⟨?_, ?_⟩343  · have h1 : ∀ l, l < x → (fun l => w (l + 1)) l344        = (fun l => -(sumRange (fun k => dualRes w k * ((ofNat (l + 1) : Shell p) ^ (p - 2)) ^ k) (p - 1))) l := by345      intro l hl346      have hlp : l + 1 < p := by347        have h : l + 1 < p - 1 + 1 := Nat.succ_lt_succ (Nat.lt_of_lt_of_le hl hx)348        rw [FRC.Nat.sub_add_cancel Pos.pos] at h349        exact h350      exact inversion_res F w (Nat.succ_pos l) hlp351    rw [sum_congr x h1, sum_neg]352    congr 1353    rw [sum_comm (fun l k => dualRes w k * ((ofNat (l + 1) : Shell p) ^ (p - 2)) ^ k) (p - 1) x]354    apply sum_congr; intro k _355    exact sum_mul_left (fun l => ((ofNat (l + 1) : Shell p) ^ (p - 2)) ^ k) (dualRes w k) x356  · unfold meridianRead357    have e : ∀ l, l < x → ((ofNat (l + 1) : Shell p) ^ (p - 2)) ^ 0 = (1 : Shell p) := fun l _ => rfl358    rw [sum_congr x e, sum_const, mul_one]359360/-- 20:B13, 20:F10 — every label other than `0` and `−1` is the readout of a nontrivial mode: `θ ≠ 0, −1` is `−g^k` for361some `1 ≤ k ≤ p − 2`; the label `−1` carries the constant mode `k = 0` and `0` is the centre. -/362theorem mode_at_label (F : Frame p κ g) {θ : Shell p} (hθ : θ ≠ 0) (hθ1 : θ ≠ -1) :363    ∃ k, 1 ≤ k ∧ k ≤ p - 2 ∧ -(g ^ k) = θ := by364  have hneg : -θ ≠ 0 := fun h0 => hθ (by rw [← neg_neg θ, h0, neg_zero])365  have hp : p - 1 = (p - 2) + 1 := by366    have := F.one_lt_p367    match p, this with368    | k + 2, _ => rfl369  match F.eq_pow_of_ne_zero hneg with370  | ⟨k, hk, e⟩ =>371    have hk0 : k ≠ 0 := fun h0 => hθ1 (by rw [h0, pow_zero] at e; rw [← neg_neg θ, ← e])372    refine ⟨k, Nat.pos_of_ne_zero hk0, ?_, by rw [e, neg_neg]⟩373    rw [hp] at hk374    exact Nat.le_of_lt_succ hk375376/-- 20:B13, 20:F10 — frame coincidence on the critical line for every zero of the Subject: on two shells `p ≤ Ω` (the377Subject's residues the Carrier's residues below `p`), every label `1 ≤ θ ≤ p − 2` reads back as the integer `θ` in both378frames, the point `2⁻¹ + ηθ` has trace one in both with the half-turn as its real part, and it is the readout of a379nontrivial mode in both: the Subject's zero at `θ` and the Carrier's zero at `θ` are one zero. -/380theorem line_coincidence_all {Ω : Nat} [Pos Ω] {κ' : Nat} {h : Shell Ω} (F : Frame p κ g) (F' : Frame Ω κ' h)381    (hpΩ : p ≤ Ω) (ν : Shell p) (ν' : Shell Ω) (θ : Nat) (hθ0 : 0 < θ) (hθ : θ + 1 < p) :382    (ofNat θ : Shell p).val = θ ∧ (ofNat θ : Shell Ω).val = θ ∧383    Ext.trace (readout ν κ (ofNat θ)) = 1 ∧ Ext.trace (readout ν' κ' (ofNat θ)) = 1 ∧384    (readout ν κ (ofNat θ)).re = ofNat (2 * κ + 1) ∧ (readout ν' κ' (ofNat θ)).re = ofNat (2 * κ' + 1) ∧385    (∃ k, 1 ≤ k ∧ k ≤ p - 2 ∧ -(g ^ k) = (ofNat θ : Shell p)) ∧386    (∃ k', 1 ≤ k' ∧ k' ≤ Ω - 2 ∧ -(h ^ k') = (ofNat θ : Shell Ω)) := by387  have hθp : θ < p := Nat.lt_of_succ_lt hθ388  have hθΩ : θ < Ω := Nat.lt_of_lt_of_le hθp hpΩ389  have v1 : (ofNat θ : Shell p).val = θ := by rw [val_ofNat, FRC.Nat.mod_eq_of_lt hθp]390  have v2 : (ofNat θ : Shell Ω).val = θ := by rw [val_ofNat, FRC.Nat.mod_eq_of_lt hθΩ]391  have n1 : (ofNat θ : Shell p) ≠ 0 := fun h0 => by392    have := congrArg Shell.val h0; rw [v1, val_zero] at this; exact Nat.ne_of_gt hθ0 this393  have n2 : (ofNat θ : Shell Ω) ≠ 0 := fun h0 => by394    have := congrArg Shell.val h0; rw [v2, val_zero] at this; exact Nat.ne_of_gt hθ0 this395  have m1 : (ofNat θ : Shell p) ≠ -1 := fun h1 => by396    have := congrArg Shell.val (h1.trans F.ofNat_n.symm)397    rw [v1, val_ofNat, FRC.Nat.mod_eq_of_lt (Nat.sub_lt Pos.pos Nat.one_pos)] at this398    have h2 : θ + 1 < p - 1 + 1 := by rw [FRC.Nat.sub_add_cancel Pos.pos]; exact hθ399    exact Nat.ne_of_lt (Nat.lt_of_succ_lt_succ h2) this400  have m2 : (ofNat θ : Shell Ω) ≠ -1 := fun h1 => by401    have := congrArg Shell.val (h1.trans F'.ofNat_n.symm)402    rw [v2, val_ofNat, FRC.Nat.mod_eq_of_lt (Nat.sub_lt Pos.pos Nat.one_pos)] at this403    have h2 : θ + 1 < Ω - 1 + 1 := by rw [FRC.Nat.sub_add_cancel Pos.pos]; exact Nat.lt_of_lt_of_le hθ hpΩ404    exact Nat.ne_of_lt (Nat.lt_of_succ_lt_succ h2) this405  exact ⟨v1, v2, (readout_on_line F ν (ofNat θ)).1, (readout_on_line F' ν' (ofNat θ)).1, rfl, rfl,406    mode_at_label F n1 m1, mode_at_label F' n2 m2⟩407408end rewrite20261017409410/-! ### The drive as an operator: the spectrum of the time evolution (20:E15), and the energy domain as a circle411(20:B14; the revision of 18 October 2026, reports/blueprint-20261018.md) -/412413section drive20261018414415/-- 20:E15 (i) — the drive is orthogonal for the pairing `⟨v, w⟩ = Σ_{l<n} v_l w_l` of the cycle: with the vectors read on416the phases (`v_l` the value at `g^l`), the drive `x ↦ g x` is `(Dv)_l = v_{l+1}` and its inverse `(D⁻¹w)_l = w_{l−1}`, and417`⟨Dv, w⟩ = ⟨v, D⁻¹w⟩`; `n = p − 1`, the indices mod `n`. -/418theorem drive_orthogonal (F : Frame p κ g) (v w : Nat → Shell p) :419    sumRange (fun l => v ((l + 1) % (p - 1)) * w l) (p - 1)420      = sumRange (fun l => v l * w ((l + (p - 2)) % (p - 1))) (p - 1) := by421  have hp : p - 1 = (p - 2) + 1 := by422    have := F.one_lt_p423    match p, this with424    | k + 2, _ => rfl425  have hn : 0 < (p - 2) + 1 := Nat.succ_pos _426  have e1 : ∀ l, l < p - 2 → (fun l => v ((l + 1) % (p - 2 + 1)) * w l) l = (fun l => v (l + 1) * w l) l := by427    intro l hl428    show v ((l + 1) % (p - 2 + 1)) * w l = v (l + 1) * w l429    rw [FRC.Nat.mod_eq_of_lt (Nat.succ_lt_succ hl)]430  have e2 : ∀ l, l < p - 2 → (fun l => v (l + 1) * w ((l + 1 + (p - 2)) % (p - 2 + 1))) l431      = (fun l => v (l + 1) * w l) l := by432    intro l hl433    show v (l + 1) * w ((l + 1 + (p - 2)) % (p - 2 + 1)) = v (l + 1) * w l434    rw [Nat.add_assoc, Nat.add_comm 1 (p - 2), FRC.Nat.mod_eq_sub_mod hn (Nat.le_add_left (p - 2 + 1) l),435      FRC.Nat.add_sub_cancel, FRC.Nat.mod_eq_of_lt (Nat.lt_succ_of_lt hl)]436  rw [hp, sumRange_succ, sumRange_succ']437  show sumRange (fun l => v ((l + 1) % (p - 2 + 1)) * w l) (p - 2) + v ((p - 2 + 1) % (p - 2 + 1)) * w (p - 2)438      = v 0 * w ((0 + (p - 2)) % (p - 2 + 1))439        + sumRange (fun l => v (l + 1) * w ((l + 1 + (p - 2)) % (p - 2 + 1))) (p - 2)440  rw [FRC.Nat.mod_self _ hn, Nat.zero_add, FRC.Nat.mod_eq_of_lt (Nat.lt_succ_self (p - 2)),441    sum_congr (p - 2) e1, sum_congr (p - 2) e2, add_comm]442443/-- 20:E15 (ii) — the spectrum of the drive is simple: the eigenvalues `g^0, …, g^{n−1}` of the `n` modes are distinct444(`pow_inj`, 26:B3); with `shift_power_character` (the modes are eigenvectors, `D x^k = g^k x^k`) the spectrum is the445`n = p − 1` nonzero residues, each once. -/446theorem spectrum_simple (F : Frame p κ g) {i j : Nat} (hi : i < p - 1) (hj : j < p - 1) (h : g ^ i = g ^ j) :447    i = j :=448  F.pow_inj hi hj h449450/-- 20:E15 (iv) — the readout is the spectral map: the mode `k` is read on the critical line at the label `−g^k`, minus451its eigenvalue under the drive. -/452theorem readout_eigen (ν : Shell p) (κ k : Nat) : (readout ν κ (-(g ^ k))).im = -(g ^ k) := rfl453454/-- 20:E15 (v), 20:B12 — the half-turn of the cycle negates the eigenvalue: `g^{k+π} = −g^k`, `π = 2κ`; the labels of the455critical line are the time domain read from `−1 = g^π` (Proposition line (v)). -/456theorem half_turn_negates (F : Frame p κ g) (k : Nat) : g ^ (k + 2 * κ) = -(g ^ k) := by457  rw [FRC.Shell.pow_add, F.half_period, ← mul_neg, mul_one]458459/-- 20:E15 (iii) — a mode other than the constant mode `0` and the Legendre mode `π = 2κ` has `g^{2k} ≠ 1`. -/460theorem mode_square_ne_one (F : Frame p κ g) {k : Nat} (hk : 0 < k) (hk2 : k < p - 1) (h2 : k ≠ 2 * κ) :461    g ^ (2 * k) ≠ 1 := by462  intro h1463  have hn : p - 1 = 2 * (2 * κ) := by rw [F.cap, FRC.Nat.add_sub_cancel]; exact Nat.mul_assoc 2 2 κ464  have h2pos : 0 < 2 := Nat.succ_pos 1465  rcases Nat.lt_or_ge k (2 * κ) with hlt | hge466  · have h2k : 2 * k < p - 1 := by rw [hn]; exact Nat.mul_lt_mul_of_pos_left hlt h2pos467    have := F.pow_inj h2k F.n_pos (h1.trans (pow_zero g).symm)468    exact Nat.ne_of_gt (Nat.mul_pos h2pos hk) this469  · have hgt : 2 * κ < k := Nat.lt_of_le_of_ne hge (Ne.symm h2)470    have hle : p - 1 ≤ 2 * k := by rw [hn]; exact Nat.mul_le_mul_left 2 hge471    have hsplit : 2 * k = (p - 1) + (2 * k - (p - 1)) := (FRC.Nat.add_sub_of_le hle).symm472    have hred : g ^ (2 * k) = g ^ (2 * k - (p - 1)) := by473      rw [hsplit, FRC.Shell.pow_add, F.pow_n, one_mul, ← hsplit]474    have hlt' : 2 * k - (p - 1) < p - 1 :=475      FRC.Nat.sub_lt_of_lt_add (by rw [← Nat.two_mul]; exact Nat.mul_lt_mul_of_pos_left hk2 h2pos) hle476    have hz := F.pow_inj hlt' F.n_pos ((hred.symm.trans h1).trans (pow_zero g).symm)477    have hle' : 2 * k ≤ 2 * (2 * κ) := by rw [← hn]; exact Nat.le_of_sub_eq_zero hz478    exact Nat.not_le_of_gt hgt (Nat.le_of_mul_le_mul_left hle' h2pos)479480/-- 20:E15 (iii) — the modes are isotropic for the pairing: the self-pairing of the mode `k`, `Σ_{l<n} (g^l)^k (g^l)^k =481Σ_{l<n} (g^{2k})^l`, vanishes when `g^{2k} ≠ 1` (`mode_square_ne_one`: every mode but `0` and `π`); so the reality of482the spectrum is not a consequence of the orthogonality, it is the drive being a scaling by a residue. -/483theorem modes_isotropic (F : Frame p κ g) {k : Nat} (h : g ^ (2 * k) ≠ 1) :484    sumRange (fun l => (g ^ l) ^ k * (g ^ l) ^ k) (p - 1) = 0 := by485  have e : ∀ l, l < p - 1 → (fun l => (g ^ l) ^ k * (g ^ l) ^ k) l = (fun l => (g ^ (2 * k)) ^ l) l := by486    intro l _487    show (g ^ l) ^ k * (g ^ l) ^ k = (g ^ (2 * k)) ^ l488    rw [← FRC.Shell.pow_add, Nat.two_mul, pow_mul_comm]489  rw [sum_congr (p - 1) e, geom_sum_unit F (F.pow_ne_zero (2 * k)), ite_eq_right h]490491/-- 20:B14 — the Cayley image of a point of the framed plane, `w = z/(1 − z)` written without division: on the critical492line `1 − z = z̄`, so `w = z/z̄ = z²/N(z)`, and `N(z)^{−1} = N(z)^{p−2}` (`pow_pred_inv`). -/493def cayley (z : Ext p ν) : Ext p ν := Ext.ofShell ((Ext.norm z) ^ (p - 2)) * (z * z)494495/-- 20:B14 — on the critical line the half-turn is the conjugation: `Tr z = 1` gives `1 − z = z̄`. -/496theorem rho_eq_conj_on_line (z : Ext p ν) (hz : Ext.trace z = 1) : rho z = Ext.conj z := by497  refine Ext.ext ?_ rfl498  show 1 + -z.re = z.re499  have h2 : z.re + z.re = 1 := hz500  calc (1 : Shell p) + -z.re = (z.re + z.re) + -z.re := by rw [h2]501    _ = z.re := by rw [add_assoc, add_neg, add_zero]502503/-- 20:B14 — on the critical line the norm does not vanish when `ν` is a nonsquare: `N(z) = c² − ν θ²` with `c = 2⁻¹`,504and `c² = ν θ²` forces `θ = c = 0` (`aniso_tx`), against `Tr z = 2c = 1`. -/505theorem norm_ne_zero_on_line (F : Frame p κ g) (hν : ¬IsSquare ν) (z : Ext p ν) (hz : Ext.trace z = 1) :506    Ext.norm z ≠ 0 := by507  intro h0508  have e : z.re * z.re = ν * (z.im * z.im) := by509    have h : z.re * z.re + -(ν * (z.im * z.im)) = 0 := h0510    calc z.re * z.re = z.re * z.re + -(ν * (z.im * z.im)) + ν * (z.im * z.im) := by511          rw [add_assoc, neg_add, add_zero]512      _ = ν * (z.im * z.im) := by rw [h, zero_add]513  have hre : z.re = 0 := (F.aniso_tx hν e).2514  have ht : z.re + z.re = 1 := hz515  rw [hre, add_zero] at ht516  exact F.one_ne_zero ht.symm517518/-- 20:B14 (i) — the Cayley image solves `w · (1 − z) = z` on the critical line, where the norm does not vanish519(`norm_ne_zero_on_line` for a nonsquare `ν`): the map `z ↦ z/(1 − z)`, as the paper writes it. -/520theorem cayley_spec (F : Frame p κ g) (z : Ext p ν) (hz : Ext.trace z = 1) (hN : Ext.norm z ≠ 0) :521    cayley z * rho z = z := by522  rw [rho_eq_conj_on_line z hz]523  show Ext.ofShell ((Ext.norm z) ^ (p - 2)) * (z * z) * Ext.conj z = z524  rw [Ext.mul_assoc, Ext.mul_assoc, Ext.mul_conj, Ext.mul_comm z, ← Ext.mul_assoc, Ext.ofShell_mul,525    mul_comm, pow_pred_inv F hN]526  exact Ext.one_mul z527528/-- 20:B14 — the Cayley map is injective on the critical line: two points with one image `w` satisfy529`z · (1 − z') = w · (1 − z) · (1 − z') = z' · (1 − z)`, whose coordinates reduce to `z = z'`. -/530theorem cayley_injective (F : Frame p κ g) (z z' : Ext p ν) (hz : Ext.trace z = 1) (hz' : Ext.trace z' = 1)531    (hN : Ext.norm z ≠ 0) (hN' : Ext.norm z' ≠ 0) (h : cayley z = cayley z') : z = z' := by532  have h1 := cayley_spec F z hz hN533  have h2 := cayley_spec F z' hz' hN'534  have e : z * rho z' = z' * rho z := by535    calc z * rho z' = cayley z * rho z * rho z' := by rw [h1]536      _ = cayley z' * rho z' * rho z := by rw [h, Ext.mul_assoc, Ext.mul_comm (rho z), ← Ext.mul_assoc]537      _ = z' * rho z := by rw [h2]538  have hre := Ext.re_congr e539  have him := Ext.im_congr e540  rw [Ext.mul_re, Ext.mul_re] at hre541  rw [Ext.mul_im, Ext.mul_im] at him542  change z.re * (1 + -z'.re) + ν * (z.im * -z'.im) = z'.re * (1 + -z.re) + ν * (z'.im * -z.im) at hre543  change z.re * -z'.im + z.im * (1 + -z'.re) = z'.re * -z.im + z'.im * (1 + -z.re) at him544  have lre : z.re * (1 + -z'.re) + ν * (z.im * -z'.im) = z.re + (-(z.re * z'.re) + -(ν * (z.im * z'.im))) :=545    Shell.Frame.RE.sound (Shell.Frame.look [z.re, z'.re, z.im, z'.im, ν])546      (.add (.mul (.var 0) (.add .one (.neg (.var 1)))) (.mul (.var 4) (.mul (.var 2) (.neg (.var 3)))))547      (.add (.var 0) (.add (.neg (.mul (.var 0) (.var 1))) (.neg (.mul (.var 4) (.mul (.var 2) (.var 3))))))548      (by decide +kernel)549  have rre : z'.re * (1 + -z.re) + ν * (z'.im * -z.im) = z'.re + (-(z.re * z'.re) + -(ν * (z.im * z'.im))) :=550    Shell.Frame.RE.sound (Shell.Frame.look [z.re, z'.re, z.im, z'.im, ν])551      (.add (.mul (.var 1) (.add .one (.neg (.var 0)))) (.mul (.var 4) (.mul (.var 3) (.neg (.var 2)))))552      (.add (.var 1) (.add (.neg (.mul (.var 0) (.var 1))) (.neg (.mul (.var 4) (.mul (.var 2) (.var 3))))))553      (by decide +kernel)554  have lim : z.re * -z'.im + z.im * (1 + -z'.re) = z.im + (-(z.re * z'.im) + -(z.im * z'.re)) :=555    Shell.Frame.RE.sound (Shell.Frame.look [z.re, z'.re, z.im, z'.im, ν])556      (.add (.mul (.var 0) (.neg (.var 3))) (.mul (.var 2) (.add .one (.neg (.var 1)))))557      (.add (.var 2) (.add (.neg (.mul (.var 0) (.var 3))) (.neg (.mul (.var 2) (.var 1)))))558      (by decide +kernel)559  have rim : z'.re * -z.im + z'.im * (1 + -z.re) = z'.im + (-(z.re * z'.im) + -(z.im * z'.re)) :=560    Shell.Frame.RE.sound (Shell.Frame.look [z.re, z'.re, z.im, z'.im, ν])561      (.add (.mul (.var 1) (.neg (.var 2))) (.mul (.var 3) (.add .one (.neg (.var 0)))))562      (.add (.var 3) (.add (.neg (.mul (.var 0) (.var 3))) (.neg (.mul (.var 2) (.var 1)))))563      (by decide +kernel)564  have hre' : z.re = z'.re := add_right_cancel (lre.symm.trans (hre.trans rre))565  have him' : z.im = z'.im := add_right_cancel (lim.symm.trans (him.trans rim))566  exact Ext.ext hre' him'567568/-- 20:B14 — the Cayley image of a point of the critical line is never `−1`: `w · (1 − z) = z` with `w = −1` reads569`−1 + z = z`, so `−1 = 0`. -/570theorem cayley_ne_neg_one (F : Frame p κ g) (z : Ext p ν) (hz : Ext.trace z = 1) (hN : Ext.norm z ≠ 0) :571    cayley z ≠ -1 := by572  intro hw573  have h := cayley_spec F z hz hN574  rw [hw] at h575  have hre := Ext.re_congr h576  have e : (-1 : Shell p) + z.re = z.re := by577    have : (-(1 : Shell p)) * (1 + -z.re) + ν * (-0 * -z.im) = z.re := hre578    rw [neg_zero, zero_mul, mul_zero, add_zero, neg_one_mul, neg_add_rev, neg_neg] at this579    exact this580  have h1 : (-1 : Shell p) = 0 := add_right_cancel (e.trans (zero_add z.re).symm)581  have h2 : (1 : Shell p) = 0 := by rw [← neg_neg (1 : Shell p), h1, neg_zero]582  exact F.one_ne_zero h2583584/-- 20:B14 (ii) — the Cayley image of a point of nonzero norm has norm one: `N(w) = N(z)^{2(p−2)} N(z)^2 = 1`; on the585critical line every point has a Cayley image on the unit circle `U_{p+1}` (`norm_ne_zero_on_line`). -/586theorem cayley_norm_one (F : Frame p κ g) (z : Ext p ν) (hN : Ext.norm z ≠ 0) : Ext.norm (cayley z) = 1 := by587  show Ext.norm (Ext.ofShell ((Ext.norm z) ^ (p - 2)) * (z * z)) = 1588  rw [Ext.norm_mul, Ext.norm_ofShell, Ext.norm_mul]589  have e : (Ext.norm z) ^ (p - 2) * (Ext.norm z) ^ (p - 2) * (Ext.norm z * Ext.norm z)590      = (Ext.norm z * (Ext.norm z) ^ (p - 2)) * (Ext.norm z * (Ext.norm z) ^ (p - 2)) :=591    Shell.Frame.RE.sound (Shell.Frame.look [Ext.norm z, (Ext.norm z) ^ (p - 2)])592      (.mul (.mul (.var 1) (.var 1)) (.mul (.var 0) (.var 0)))593      (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (by decide +kernel)594  rw [e, pow_pred_inv F hN, mul_one]595596/-- 20:B14 (iii) — the centre `2⁻¹` goes to `1`: the readout of the label `0` is the real point `2⁻¹`, of norm `4⁻¹`,597and its Cayley image is `N^{p−2} · N = 1`. -/598theorem cayley_centre (F : Frame p κ g) (ν : Shell p) : cayley (readout ν κ 0) = 1 := by599  have hc : (ofNat (2 * κ + 1) : Shell p) ≠ 0 := fun h0 => by600    have h := (half_inverse F).1601    rw [h0, mul_zero] at h602    exact F.one_ne_zero h.symm603  have hN : Ext.norm (readout ν κ 0) = ofNat (2 * κ + 1) * ofNat (2 * κ + 1) := by604    show ofNat (2 * κ + 1) * ofNat (2 * κ + 1) + -(ν * (0 * 0)) = ofNat (2 * κ + 1) * ofNat (2 * κ + 1)605    rw [mul_zero, mul_zero, neg_zero, add_zero]606  have hsq : readout ν κ 0 * readout ν κ 0 = Ext.ofShell (ofNat (2 * κ + 1) * ofNat (2 * κ + 1)) := by607    refine Ext.ext ?_ ?_608    · show ofNat (2 * κ + 1) * ofNat (2 * κ + 1) + ν * (0 * 0) = ofNat (2 * κ + 1) * ofNat (2 * κ + 1)609      rw [mul_zero, mul_zero, add_zero]610    · show ofNat (2 * κ + 1) * 0 + 0 * ofNat (2 * κ + 1) = 0611      rw [mul_zero, zero_mul, add_zero]612  show Ext.ofShell ((Ext.norm (readout ν κ 0)) ^ (p - 2)) * (readout ν κ 0 * readout ν κ 0) = 1613  rw [hsq, Ext.ofShell_mul, hN, mul_comm, pow_pred_inv F (mul_ne_zero F hc hc)]614  rfl615616/-- 20:B14 (iv) — the conjugation becomes the inversion: the Cayley image of `z̄` is the conjugate of the Cayley image617of `z`, and on the circle the conjugate is the inverse, `w · w̄ = 1`. -/618theorem cayley_conj (F : Frame p κ g) (z : Ext p ν) (hN : Ext.norm z ≠ 0) :619    cayley (Ext.conj z) = Ext.conj (cayley z) ∧ cayley z * Ext.conj (cayley z) = 1 := by620  refine ⟨?_, Ext.conj_inv_of_norm_one _ (cayley_norm_one F z hN)⟩621  have hNc : Ext.norm (Ext.conj z) = Ext.norm z := by622    show z.re * z.re + -(ν * (-z.im * -z.im)) = z.re * z.re + -(ν * (z.im * z.im))623    rw [neg_mul_neg]624  show Ext.ofShell ((Ext.norm (Ext.conj z)) ^ (p - 2)) * (Ext.conj z * Ext.conj z)625      = Ext.conj (Ext.ofShell ((Ext.norm z) ^ (p - 2)) * (z * z))626  have hc : Ext.conj (Ext.ofShell ((Ext.norm z) ^ (p - 2)) : Ext p ν) = Ext.ofShell ((Ext.norm z) ^ (p - 2)) :=627    Ext.ext rfl neg_zero628  rw [hNc, Ext.conj_mul, Ext.conj_mul, hc]629630end drive20261018631632end FRC.Horizon633