Theme/Observation.lean — FrcCore

1import FrcCore.Theme.Quantum2import FrcCore.Theme.Quadratic34/-!5# FrcCore.Theme.Observation — the quantum theme: the single-system formalism in the shadow (22-quantum, 15 October 2026)67The observation formalism of 22-quantum read on a prime shell `𝔽_q`, the Carrier chart of the ledger `ℤ[ζ_d]` (the8reduction `ζ ↦ v`, 22:C9): a winding of the Object cycle is a power map, the drive multiplies it by a scalar, the forced9basis of a core of order `d` is the character table of `C_d`, and the Born weights are the character sums.1011* characters are power maps, pairwise distinct (`power_maps`, 22:C1); the drive's eigenvalues are distinct and a12  winding acquires the weight `k` per chronon (`stationary`, 22:C2);13* orthogonality `d δ`, the bilinear Parseval identity and the Lüders projector (`orthogonality`, `parseval`,14  `lueders`, 22:C3, C5); the selection rule `r ≡ k (mod d)` (`selection`, 22:C4); the pair count as a double sum and the15  pure-winding weight `d² [r ≡ k]` (`pair_count`, `pure_winding_weight`, 22:C7);16* the reduction: the shadow of the group ring `ℕ[C_n]` is a ring map, additive and multiplicative, and silent about17  magnitude (`reduce_add`, `reduce_mul`, `reduce_wrap`, 22:C9);18* the unique window lift (`window_lift`, 22:C10) and the wrap (`wrap_quantised`, 22:X8, P2);19* the forced complex sector: the shared core of two framed shells contains `Q₄`, it is `Q₄` when the capacities are20  coprime, and a shell `p ≡ 3 (mod 4)` has no quarter-turn (`shared_core`, `no_quarter_turn`, 22:C13);21* classicality is the index of the core (`classicality_index`, 22:C24);22* the quarter-turn transport trichotomy (`transport_trichotomy`, 22:C27);23* conjugation is inversion: the Frobenius is the only non-trivial automorphism of `𝔽_{p²}` over `𝔽_p`, it inverts the24  norm-one torus, and exponent negation inverts the phase cycle (`frobenius_unique`, `torus_conj_inv`,25  `exponent_negation`, 22:C6).2627No axioms.28-/2930namespace FRC.Observation3132open FRC.Shell33open FRC.Shell.Prime34open FRC.Quantum3536variable {q : Nat} [Pos q]3738/-! ## Powers of an element of order `n` -/3940/-- The powers `x⁰, …, x^{n−1}` of an element of order `n` are distinct. -/41theorem pow_inj_of_order (hq : FRC.Nat.isPrime q) {x : Shell q} {n : Nat} (hx : HasOrder x n) {i j : Nat}42    (hi : i < n) (hj : j < n) (h : x ^ i = x ^ j) : i = j := by43  have hx0 : x ≠ 0 := fun e => by44    have h1 := hx.2.145    rw [e] at h146    match n, hx.1, h1 with47    | k + 1, _, h1 => rw [pow_succ, mul_zero] at h1; exact one_ne_zero hq h1.symm48  have key : ∀ {i j : Nat}, i ≤ j → j < n → x ^ i = x ^ j → i = j := by49    intro i j hij hj h50    have e1 : x ^ i * x ^ (j - i) = x ^ i * 1 := by rw [← pow_add, FRC.Nat.add_sub_of_le hij, mul_one, h]51    have e2 : x ^ (j - i) = 1 := mul_left_cancel hq (pow_ne_zero hq hx0 i) e152    match Nat.decEq (j - i) 0 with53    | .isTrue h0 => exact Nat.le_antisymm hij (Nat.le_of_sub_eq_zero h0)54    | .isFalse h0 =>55      exact absurd e2 (hx.2.2 _ (Nat.lt_of_le_of_lt (Nat.sub_le j i) hj) (Nat.pos_of_ne_zero h0))56  exact match Nat.lt_or_ge i j with57    | .inl hlt => key (Nat.le_of_lt hlt) hj h58    | .inr hge => (key hge hi h.symm).symm5960/-- A power reduces modulo the order: `x^c = x^{c mod n}`. -/61theorem pow_mod_order {x : Shell q} {n : Nat} (hx : HasOrder x n) (c : Nat) : x ^ c = x ^ (c % n) := by62  match FRC.Nat.mod_spec n hx.1 c with63  | ⟨k, hk⟩ => conv => lhs; rw [hk, pow_add, pow_mul, hx.2.1, one_pow, one_mul]6465/-- `x^a = x^b` exactly when `a ≡ b (mod n)`, for `x` of order `n`. -/66theorem pow_eq_pow_iff_mod (hq : FRC.Nat.isPrime q) {x : Shell q} {n : Nat} (hx : HasOrder x n) (a b : Nat) :67    x ^ a = x ^ b ↔ a % n = b % n := by68  constructor69  · intro h70    rw [pow_mod_order hx a, pow_mod_order hx b] at h71    exact pow_inj_of_order hq hx (Nat.mod_lt a hx.1) (Nat.mod_lt b hx.1) h72  · intro h; rw [pow_mod_order hx a, pow_mod_order hx b, h]7374/-- `x^a = 1` exactly when `a % n = 0`. -/75theorem pow_eq_one_iff_mod (hq : FRC.Nat.isPrime q) {x : Shell q} {n : Nat} (hx : HasOrder x n) (a : Nat) :76    x ^ a = 1 ↔ a % n = 0 := by77  have := pow_eq_pow_iff_mod hq hx a 078  rw [pow_zero, FRC.Nat.zero_mod] at this; exact this7980/-! ## 22:C1, C2 — characters are power maps; stationary states are the windings -/8182/-- 22:C1 — the characters of the Object cycle are the power maps `u ↦ u^k`: each is multiplicative, and for a cycle83generated by `ζ` of order `n` the maps of distinct windings `k, k' < n` differ (at the generator). -/84theorem power_maps (hq : FRC.Nat.isPrime q) {ζ : Shell q} {n : Nat} (hζ : HasOrder ζ n) :85    (∀ (u v : Shell q) (k : Nat), (u * v) ^ k = u ^ k * v ^ k) ∧86    ∀ k k', k < n → k' < n → k ≠ k' → ζ ^ k ≠ ζ ^ k' :=87  ⟨fun u v k => mul_pow u v k, fun k k' hk hk' hne e => hne (pow_inj_of_order hq hζ hk hk' e)⟩8889/-- 22:C2 — the windings are the drive's eigenvectors: `ψ_k(g u) = g^k ψ_k(u)`, the eigenvalue `g^k` is the weight90`k` per chronon, and the eigenvalues of the windings `k < n` are distinct for a drive `g` of order `n` on the cycle. -/91theorem stationary (hq : FRC.Nat.isPrime q) {g : Shell q} {n : Nat} (hg : HasOrder g n) :92    (∀ (u : Shell q) (k : Nat), (g * u) ^ k = g ^ k * u ^ k) ∧93    ∀ k k', k < n → k' < n → g ^ k = g ^ k' → k = k' :=94  ⟨fun u k => mul_pow g u k, fun k k' hk hk' e => pow_inj_of_order hq hg hk hk' e⟩9596/-- 22:C1 — every `n`-th root of unity is a power of a given element of order `n` (the root bound of `Xⁿ − 1`; the proof of97`FRC.Quantum.absorbed` with the generator replaced by any element of order `n`). -/98theorem roots_of_order (hq : FRC.Nat.isPrime q) {x : Shell q} {n : Nat} (hx : HasOrder x n) (y : Shell q)99    (hy : y ^ n = 1) : ∃ k, k < n ∧ y = x ^ k := by100  have hn : 0 < n := hx.1101  have hx0 : x ≠ 0 := fun e => by102    have h1 := hx.2.1103    rw [e] at h1104    match n, hx.1, h1 with105    | k + 1, _, h1 => rw [pow_succ, mul_zero] at h1; exact one_ne_zero hq h1.symm106  match decExistsLT (fun k => y = x ^ k) n with107  | .isTrue h => exact h108  | .isFalse h =>109    exfalso110    have hdist : ∀ i j, i < n → j < n → x ^ i = x ^ j → i = j := fun i j hi hj e =>111      pow_inj_of_order hq hx hi hj e112    let r : Nat → Shell q := fun i => if i < n then x ^ i else y113    have hr : ∀ i j, i ≤ n → j ≤ n → r i = r j → i = j := fun i j hi hj e => by114      change (if i < n then x ^ i else y) = (if j < n then x ^ j else y) at e115      match Nat.decLt i n, Nat.decLt j n with116      | .isTrue hi', .isTrue hj' =>117        have e' : x ^ i = x ^ j := by118          have := e; rw [ite_eq_left hi', ite_eq_left hj'] at this; exact this119        exact hdist i j hi' hj' e'120      | .isTrue hi', .isFalse hj' =>121        have e' : x ^ i = y := by122          have := e; rw [ite_eq_left hi', ite_eq_right hj'] at this; exact this123        exact absurd ⟨i, hi', e'.symm⟩ h124      | .isFalse hi', .isTrue hj' =>125        have e' : y = x ^ j := by126          have := e; rw [ite_eq_right hi', ite_eq_left hj'] at this; exact this127        exact absurd ⟨j, hj', e'⟩ h128      | .isFalse hi', .isFalse hj' =>129        exact (Nat.le_antisymm hi (Nat.not_lt.1 hi')).trans (Nat.le_antisymm hj (Nat.not_lt.1 hj')).symm130    have hroot : ∀ i, i ≤ n → Poly.eval (Poly.xn1 n : Poly q) n (r i) = 0 := fun i _ => by131      rw [Poly.eval_xn1 hn]132      match Nat.decLt i n with133      | .isTrue hi' =>134        show (if i < n then x ^ i else y) ^ n + -1 = 0135        rw [ite_eq_left hi', ← pow_mul, Nat.mul_comm, pow_mul, hx.2.1, one_pow, add_neg]136      | .isFalse hi' => show (if i < n then x ^ i else y) ^ n + -1 = 0; rw [ite_eq_right hi', hy, add_neg]137    have hz := Poly.root_bound_of (fun h => Prime.mul_eq_zero hq h) n (Poly.xn1 n) (Poly.xn1_bound n) r hr hroot n138    rw [Poly.xn1_top] at hz139    exact Prime.one_ne_zero hq hz140141/-- 22:C1 — the characters are the power maps: a multiplicative map `χ` on the cycle `⟨ζ⟩` of order `n`142(`χ(ζ^a ζ^b) = χ(ζ^a) χ(ζ^b)`, `χ 1 = 1`) is `u ↦ u^k` for one `k < n`, `χ(ζ^j) = (ζ^j)^k` for every `j`. -/143theorem character_is_power_map (hq : FRC.Nat.isPrime q) {ζ : Shell q} {n : Nat} (hζ : HasOrder ζ n)144    (χ : Shell q → Shell q) (hmul : ∀ a b : Nat, χ (ζ ^ a * ζ ^ b) = χ (ζ ^ a) * χ (ζ ^ b)) (h1 : χ 1 = 1) :145    ∃ k : Nat, k < n ∧ ∀ j : Nat, χ (ζ ^ j) = (ζ ^ j) ^ k := by146  have hpow : ∀ j : Nat, χ (ζ ^ j) = (χ ζ) ^ j := by147    intro j148    induction j with149    | zero => rw [pow_zero, pow_zero]; exact h1150    | succ j ih =>151      rw [pow_succ]152      have := hmul j 1153      rw [pow_one] at this154      rw [this, ih, pow_succ]155  have hn : (χ ζ) ^ n = 1 := by rw [← hpow, hζ.2.1]; exact h1156  obtain ⟨k, hk, e⟩ := roots_of_order hq hζ (χ ζ) hn157  exact ⟨k, hk, fun j => by rw [hpow, e, ← pow_mul, Nat.mul_comm, pow_mul]⟩158159/-- 22:C2 — the stationary states are the winding modes: a function `ψ` on the cycle `⟨g⟩` of order `n` that the160drive scales, `ψ(g · g^j) = λ ψ(g^j)` for every `j`, is `ψ(g^j) = ψ(1) (g^j)^k` for one winding `k < n` with161`λ = g^k` when `ψ 1 ≠ 0`, and vanishes on the cycle when `ψ 1 = 0`. -/162theorem stationary_modes (hq : FRC.Nat.isPrime q) {g : Shell q} {n : Nat} (hg : HasOrder g n)163    (ψ : Shell q → Shell q) {lam : Shell q} (hψ : ∀ j : Nat, ψ (g * g ^ j) = lam * ψ (g ^ j)) :164    (ψ 1 = 0 → ∀ j : Nat, ψ (g ^ j) = 0) ∧165    (ψ 1 ≠ 0 → ∃ k : Nat, k < n ∧ lam = g ^ k ∧ ∀ j : Nat, ψ (g ^ j) = ψ 1 * (g ^ j) ^ k) := by166  have hpow : ∀ j : Nat, ψ (g ^ j) = lam ^ j * ψ 1 := by167    intro j168    induction j with169    | zero => rw [pow_zero, pow_zero, one_mul]170    | succ j ih => rw [pow_succ, Shell.mul_comm (g ^ j) g, hψ j, ih, pow_succ, Shell.mul_comm (lam ^ j) lam,171        Shell.mul_assoc]172  refine ⟨fun h0 j => by rw [hpow, h0, mul_zero], fun h0 => ?_⟩173  have hn : lam ^ n = 1 := by174    have e : lam ^ n * ψ 1 = ψ 1 := by rw [← hpow, hg.2.1]175    have e2 : (lam ^ n + -1) * ψ 1 = 0 := by rw [Shell.right_distrib, Shell.neg_one_mul, e, add_neg]176    match Prime.mul_eq_zero hq e2 with177    | .inl h => exact Prime.eq_of_sub_eq_zero h178    | .inr h => exact absurd h h0179  obtain ⟨k, hk, e⟩ := roots_of_order hq hg lam hn180  exact ⟨k, hk, e, fun j => by rw [hpow, e, ← pow_mul, Nat.mul_comm, pow_mul, Shell.mul_comm]⟩181182/-! ## Character sums over a core of order `d` -/183184/-- A geometric sum of a root of unity other than `1` vanishes: `x^n = 1`, `x ≠ 1` give `Σ_{l<n} x^l = 0`. -/185theorem geom_sum_zero (hq : FRC.Nat.isPrime q) {x : Shell q} (n : Nat) (hn : x ^ n = 1) (hx : x ≠ 1) :186    sumRange (fun l => x ^ l) n = 0 := by187  have hg := geom_sum_mul x n188  rw [hn, add_neg] at hg189  match mul_eq_zero hq hg with190  | .inl h => exact h191  | .inr h => exact absurd (eq_of_sub_eq_zero h) hx192193/-- The character sum of `ω` of order `d` at the exponent `e`: `Σ_{j<d} ω^{e j} = d` when `d ∣ e`, else `0`. -/194theorem character_sum (hq : FRC.Nat.isPrime q) {ω : Shell q} {d : Nat} (hω : HasOrder ω d) (e : Nat) :195    sumRange (fun j => ω ^ (e * j)) d = if e % d = 0 then ofNat d else 0 := by196  have e1 : ∀ j, ω ^ (e * j) = (ω ^ e) ^ j := fun j => pow_mul ω e j197  rw [sum_congr d (fun j _ => e1 j)]198  match Nat.decEq (e % d) 0 with199  | .isTrue h0 =>200    rw [if_pos h0, (pow_eq_one_iff_mod hq hω e).2 h0]201    have := sum_const (1 : Shell q) d202    rw [mul_one] at this203    rw [← this]; exact sum_congr d (fun j _ => one_pow j)204  | .isFalse h0 =>205    rw [if_neg h0]206    refine geom_sum_zero hq d ?_ ?_207    · rw [← pow_mul, Nat.mul_comm, pow_mul, hω.2.1, one_pow]208    · intro h1; exact h0 ((pow_eq_one_iff_mod hq hω e).1 h1)209210/-- The exponent `r + (d − r')` is a multiple of `d` exactly when `r = r'`, for `r, r' < d`. -/211theorem shift_mod {d r r' : Nat} (hr : r < d) (hr' : r' < d) : (r + (d - r')) % d = 0 ↔ r = r' := by212  have hd : 0 < d := Nat.lt_of_le_of_lt (Nat.zero_le r) hr213  constructor214  · intro h215    match Nat.lt_or_ge r r' with216    | .inl hlt =>217      have hpos : 0 < r + (d - r') := Nat.add_pos_right r (sub_pos hr')218      have hlt' : r + (d - r') < d := by219        have : r + (d - r') < r' + (d - r') := Nat.add_lt_add_right hlt _220        rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt hr')] at this; exact this221      rw [FRC.Nat.mod_eq_of_lt hlt'] at h222      exact absurd h (Nat.ne_of_gt hpos)223    | .inr hge =>224      have e : r + (d - r') = d * 1 + (r - r') := by225        calc r + (d - r') = (r - r' + r') + (d - r') := by rw [FRC.Nat.sub_add_cancel hge]226          _ = (r - r') + (r' + (d - r')) := Nat.add_assoc _ _ _227          _ = (r - r') + d := by rw [FRC.Nat.add_sub_of_le (Nat.le_of_lt hr')]228          _ = d * 1 + (r - r') := by rw [Nat.mul_one, Nat.add_comm]229      rw [e, FRC.Nat.add_mul_mod_self_left _ _ _ hd] at h230      have hlt' : r - r' < d := Nat.lt_of_le_of_lt (Nat.sub_le r r') hr231      rw [FRC.Nat.mod_eq_of_lt hlt'] at h232      exact Nat.le_antisymm (Nat.le_of_sub_eq_zero h) hge233  · intro h; rw [h, FRC.Nat.add_sub_of_le (Nat.le_of_lt hr'), FRC.Nat.mod_self d hd]234235/-- 22:C3, 22:X3 — orthogonality of the forced basis: for a core `C_d` generated by `ω`, the characters `η_r(j) = ω^{rj}`236satisfy `Σ_{j<d} η_r(j) η_{r'}(j)⁻¹ = d δ_{rr'}` (the inverse character is `ω^{(d−r')j}`). -/237theorem orthogonality (hq : FRC.Nat.isPrime q) {ω : Shell q} {d : Nat} (hω : HasOrder ω d) {r r' : Nat} (hr : r < d)238    (hr' : r' < d) :239    sumRange (fun j => ω ^ (r * j) * ω ^ ((d - r') * j)) d = if r = r' then ofNat d else 0 := by240  have e1 : ∀ j, ω ^ (r * j) * ω ^ ((d - r') * j) = ω ^ ((r + (d - r')) * j) := fun j => by241    rw [← pow_add, FRC.Nat.add_mul]242  rw [sum_congr d (fun j _ => e1 j), character_sum hq hω]243  match Nat.decEq r r' with244  | .isTrue h => rw [if_pos h, if_pos ((shift_mod hr hr').2 h)]245  | .isFalse h => rw [if_neg h, if_neg (fun h' => h ((shift_mod hr hr').1 h'))]246247/-- 22:C4, 22:C23, 22:X3, 22:C24, 22:X5 — the selection rule: a pointer channel `r < d` couples to the Object winding `k` over a fibre of the core248exactly when their core phases agree, `k ≡ r (mod d)`: `Σ_{j<d} ω^{kj} ω^{(d−r)j} = d [k ≡ r]`. -/249theorem selection (hq : FRC.Nat.isPrime q) {ω : Shell q} {d : Nat} (hω : HasOrder ω d) (k : Nat) {r : Nat}250    (hr : r < d) :251    sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d = if k % d = r then ofNat d else 0 := by252  have e1 : ∀ j, ω ^ (k * j) * ω ^ ((d - r) * j) = ω ^ ((k % d) * j) * ω ^ ((d - r) * j) := fun j => by253    rw [(pow_eq_pow_iff_mod hq hω (k * j) ((k % d) * j)).2 (FRC.Nat.mul_mod_left' k j d hω.1)]254  rw [sum_congr d (fun j _ => e1 j), orthogonality hq hω (Nat.mod_lt k hω.1) hr]255256/-- 22:C5, 22:X4 — the Lüders projector of the channel `r`, `Π_{jl} = ω^{rj} ω^{(d−r)l}`, is idempotent up to `d`: `Π² = d Π`,257so an immediately repeated registration returns the outcome. -/258theorem lueders {ω : Shell q} {d : Nat} (hω : HasOrder ω d) {r : Nat} (hr : r < d) (j m : Nat) :259    sumRange (fun l => (ω ^ (r * j) * ω ^ ((d - r) * l)) * (ω ^ (r * l) * ω ^ ((d - r) * m))) d =260      ofNat d * (ω ^ (r * j) * ω ^ ((d - r) * m)) := by261  have e1 : ∀ l, (ω ^ (r * j) * ω ^ ((d - r) * l)) * (ω ^ (r * l) * ω ^ ((d - r) * m)) =262      ω ^ (r * j) * ω ^ ((d - r) * m) := fun l => by263    have hl : ω ^ ((d - r) * l) * ω ^ (r * l) = 1 := by264      rw [← pow_add, ← FRC.Nat.add_mul, FRC.Nat.sub_add_cancel (Nat.le_of_lt hr), pow_mul, hω.2.1, one_pow]265    rw [mul_assoc, ← mul_assoc (ω ^ ((d - r) * l)), hl, one_mul]266  rw [sum_congr d (fun l _ => e1 l), sum_const]267268/-- A product of two sums is the double sum of the products. -/269theorem sum_mul_sum (f g : Nat → Shell q) (n m : Nat) :270    sumRange f n * sumRange g m = sumRange (fun j => sumRange (fun l => f j * g l) m) n := by271  rw [← sum_mul_right]272  exact sum_congr n (fun j _ => (sum_mul_left g (f j) m).symm)273274/-- Double sums commute. -/275theorem sum_comm (F : Nat → Nat → Shell q) (n m : Nat) :276    sumRange (fun j => sumRange (fun l => F j l) m) n = sumRange (fun l => sumRange (fun j => F j l) n) m := by277  induction n with278  | zero => rw [sumRange_zero]; exact (sum_zero m (fun l _ => rfl)).symm279  | succ n ih =>280    rw [sumRange_succ, ih, ← sum_add]281    exact sum_congr m (fun l _ => (sumRange_succ _ n).symm)282283/-- 22:C7, 22:X1 — the pair count: the squared amplitude is the double sum of phase agreements,284`(Σ_j ψ_j)(Σ_l ψ̄_l) = Σ_j Σ_l ψ_j ψ̄_l`. -/285theorem pair_count (ψ ψbar : Nat → Shell q) (d : Nat) :286    sumRange ψ d * sumRange ψbar d = sumRange (fun j => sumRange (fun l => ψ j * ψbar l) d) d :=287  sum_mul_sum ψ ψbar d d288289/-- 22:C7, 22:C10, 22:X1 — on a pure winding `k` the weight of the channel `r < d` is `d² [k ≡ r (mod d)]`: the amplitude290`Σ_j ω^{kj} ω^{(d−r)j}` times its conjugate `Σ_l ω^{rl} ω^{(d−k)l}` (the conjugate winding `d − k % d`). -/291theorem pure_winding_weight (hq : FRC.Nat.isPrime q) {ω : Shell q} {d : Nat} (hω : HasOrder ω d) (k : Nat) {r : Nat}292    (hr : r < d) :293    sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d * sumRange (fun l => ω ^ (r * l) * ω ^ ((d - k % d) * l)) d =294      if k % d = r then ofNat (d * d) else 0 := by295  rw [selection hq hω k hr, orthogonality hq hω hr (Nat.mod_lt k hω.1)]296  match Nat.decEq (k % d) r with297  | .isTrue h => rw [if_pos h, if_pos h.symm, if_pos h, ofNat_mul]298  | .isFalse h => rw [if_neg h, zero_mul, if_neg h]299300/-- The cross exponents `r l + (d − r) j` and `l r + (d − j) r` agree modulo `d` for `r, j < d`. -/301theorem cross_mod {d r j : Nat} (hr : r < d) (hj : j < d) (l : Nat) :302    (r * l + (d - r) * j) % d = (l * r + (d - j) * r) % d := by303  have hd : 0 < d := Nat.lt_of_le_of_lt (Nat.zero_le r) hr304  have h1 : r * j + (r * l + (d - r) * j) = d * j + r * l := by305    calc r * j + (r * l + (d - r) * j) = r * l + ((d - r) * j + r * j) := by306          rw [Nat.add_left_comm, Nat.add_comm (r * j)]307      _ = r * l + d * j := by rw [← FRC.Nat.add_mul, FRC.Nat.sub_add_cancel (Nat.le_of_lt hr)]308      _ = d * j + r * l := Nat.add_comm _ _309  have h2 : r * j + (l * r + (d - j) * r) = d * r + l * r := by310    calc r * j + (l * r + (d - j) * r) = l * r + ((d - j) * r + j * r) := by311          rw [Nat.add_left_comm, Nat.add_comm (r * j), Nat.mul_comm r j]312      _ = l * r + d * r := by rw [← FRC.Nat.add_mul, FRC.Nat.sub_add_cancel (Nat.le_of_lt hj)]313      _ = d * r + l * r := Nat.add_comm _ _314  refine mod_add_left_cancel (x := r * j) hd ?_315  rw [h1, h2, FRC.Nat.add_mul_mod_self_left _ _ _ hd, FRC.Nat.add_mul_mod_self_left _ _ _ hd, Nat.mul_comm r l]316317/-- 22:C3, 22:C7 — the bilinear Parseval identity on the core: for any two coefficient vectors `f, g` on the fibre,318`Σ_{r<d} (Σ_j f_j ω^{(d−r)j}) (Σ_l g_l ω^{rl}) = d Σ_j f_j g_j` (with `g = f̄` the resolution of identity and the319norm identity of the forced basis). -/320theorem parseval (hq : FRC.Nat.isPrime q) {ω : Shell q} {d : Nat} (hω : HasOrder ω d) (f g : Nat → Shell q) :321    sumRange (fun r => sumRange (fun j => f j * ω ^ ((d - r) * j)) d * sumRange (fun l => g l * ω ^ (r * l)) d) d =322      ofNat d * sumRange (fun j => f j * g j) d := by323  have e1 : ∀ r, sumRange (fun j => f j * ω ^ ((d - r) * j)) d * sumRange (fun l => g l * ω ^ (r * l)) d =324      sumRange (fun j => sumRange (fun l => (f j * g l) * (ω ^ (r * l) * ω ^ ((d - r) * j))) d) d := fun r => by325    rw [sum_mul_sum]326    refine sum_congr d (fun j _ => sum_congr d (fun l _ => ?_))327    rw [mul_mul_mul_comm, mul_comm (ω ^ ((d - r) * j))]328  rw [sum_congr d (fun r _ => e1 r), sum_comm, ← sum_mul_left]329  refine sum_congr d (fun j hj => ?_)330  rw [sum_comm]331  have e2 : ∀ l, sumRange (fun r => (f j * g l) * (ω ^ (r * l) * ω ^ ((d - r) * j))) d =332      (f j * g l) * sumRange (fun r => ω ^ (r * l) * ω ^ ((d - r) * j)) d := fun l => sum_mul_left _ _ d333  have e3 : ∀ l, l < d → sumRange (fun r => ω ^ (r * l) * ω ^ ((d - r) * j)) d = if l = j then ofNat d else 0 :=334    fun l hl => by335      have e4 : ∀ r, r < d → ω ^ (r * l) * ω ^ ((d - r) * j) = ω ^ (l * r) * ω ^ ((d - j) * r) := fun r hr => by336        rw [← pow_add, ← pow_add]337        exact (pow_eq_pow_iff_mod hq hω _ _).2 (cross_mod hr hj l)338      rw [sum_congr d e4, orthogonality hq hω hl hj]339  rw [sum_congr d (fun l _ => e2 l), sum_congr d (fun l hl => by rw [e3 l hl])]340  rw [sum_eq_single (f := fun l => f j * g l * (if l = j then ofNat d else 0)) hj341    (fun l _ hne => by rw [if_neg hne, mul_zero])]342  rw [if_pos rfl, mul_comm]343344/-! ## 22:C9 — the reduction: the shadow of the group ring is a ring map -/345346/-- `ofNat` is additive. -/347theorem ofNat_add (a b : Nat) : (ofNat a + ofNat b : Shell q) = ofNat (a + b) :=348  Shell.ext (by show (a % q + b % q) % q = (a + b) % q; exact (FRC.Nat.add_mod a b q Pos.pos).symm)349350/-- A sum of naturals. -/351def nsum (f : Nat → Nat) : Nat → Nat352  | 0 => 0353  | n + 1 => nsum f n + f n354355/-- The shadow of a sum of naturals is the sum of the shadows. -/356theorem ofNat_nsum (f : Nat → Nat) : ∀ n, (ofNat (nsum f n) : Shell q) = sumRange (fun e => (ofNat (f e) : Shell q)) n357  | 0 => rfl358  | n + 1 => by359    show (ofNat (nsum f n + f n) : Shell q) = sumRange (fun e => (ofNat (f e) : Shell q)) n + ofNat (f n)360    rw [← ofNat_add, ofNat_nsum f n]361362/-- The shadow of a ledger element `Σ_{e<n} c_e ζ^e` of `ℕ[C_n]` on the shell: `ζ ↦ v`. -/363def shadow (v : Shell q) (c : Nat → Nat) (n : Nat) : Shell q := sumRange (fun e => ofNat (c e) * v ^ e) n364365/-- The product in the group ring `ℕ[C_n]`: `(c ⋆ c')_e = Σ_{a,b<n, a+b ≡ e} c_a c'_b`. -/366def conv (c c' : Nat → Nat) (n e : Nat) : Nat :=367  nsum (fun a => nsum (fun b => if (a + b) % n = e then c a * c' b else 0) n) n368369/-- 22:C9 — the reduction is additive: the shadow of `c + c'` is the sum of the shadows. -/370theorem reduce_add (v : Shell q) (c c' : Nat → Nat) (n : Nat) :371    shadow v (fun e => c e + c' e) n = shadow v c n + shadow v c' n := by372  unfold shadow373  rw [← sum_add]374  exact sum_congr n (fun e _ => by rw [← ofNat_add, right_distrib])375376/-- 22:C9, 22:C17 — the reduction is multiplicative: with `v^n = 1`, the shadow of the convolution `c ⋆ c'` is the product377of the shadows; the Carrier-chart amplitude of a product is the product of the amplitudes, exact as algebra. -/378theorem reduce_mul {v : Shell q} {n : Nat} (hn : 0 < n) (hv : v ^ n = 1) (c c' : Nat → Nat) :379    shadow v (conv c c' n) n = shadow v c n * shadow v c' n := by380  unfold shadow conv381  rw [sum_mul_sum]382  have step1 : ∀ e, ofNat (nsum (fun a => nsum (fun b => if (a + b) % n = e then c a * c' b else 0) n) n) * v ^ e =383      sumRange (fun a => sumRange (fun b => (if (a + b) % n = e then ofNat (c a * c' b) else 0) * v ^ e) n) n := fun e => by384    rw [ofNat_nsum, ← sum_mul_right]385    refine sum_congr n (fun a _ => ?_)386    rw [ofNat_nsum, ← sum_mul_right]387    refine sum_congr n (fun b _ => ?_)388    match Nat.decEq ((a + b) % n) e with389    | .isTrue h => rw [if_pos h, if_pos h]390    | .isFalse h => rw [if_neg h, if_neg h]; rfl391  rw [sum_congr n (fun e _ => step1 e), sum_comm]392  refine sum_congr n (fun a _ => ?_)393  rw [sum_comm]394  refine sum_congr n (fun b _ => ?_)395  have hab : (a + b) % n < n := Nat.mod_lt _ hn396  rw [sum_eq_single (f := fun e => (if (a + b) % n = e then ofNat (c a * c' b) else 0) * v ^ e) hab397    (fun e _ hne => by rw [if_neg (fun h => hne h.symm), zero_mul])]398  rw [if_pos rfl, ← ofNat_mul, mul_mul_mul_comm, ← pow_add]399  congr 1400  match FRC.Nat.mod_spec n hn (a + b) with401  | ⟨k, hk⟩ => conv => rhs; rw [hk, pow_add, pow_mul, hv, one_pow, one_mul]402403/-- 22:C9 — the reduction is silent about magnitude: the count `q` itself reduces to `0`. -/404theorem reduce_wrap : (ofNat q : Shell q) = 0 := ofNat_self405406/-! ## 22:C10, X8, P2 — the window lift and the wrap -/407408/-- 22:C10, 22:X1, 22:X6 — the unique window lift: two tallies below the window `Ω` with one shadow are equal, so a sub-horizon409tally is the unique lift of its residue. -/410theorem window_lift {a b : Nat} (ha : a < q) (hb : b < q) (h : (ofNat a : Shell q) = ofNat b) : a = b := by411  have := val_injective h412  show a = b413  rw [show (ofNat a : Shell q).val = a % q from rfl, show (ofNat b : Shell q).val = b % q from rfl,414    FRC.Nat.mod_eq_of_lt ha, FRC.Nat.mod_eq_of_lt hb] at this415  exact this416417/-- 22:X8, 22:P2 — the wrap is quantised: a tally whose shadow vanishes is a multiple of `Ω`, so a lift of the vanishing418Sorkin sum above the window is `Ω` times an integer, never a small nonzero number. -/419theorem wrap_quantised (a : Nat) : (ofNat a : Shell q) = 0 ↔ ∃ k, a = q * k := by420  constructor421  · intro h422    have hv := val_injective h423    rw [show (ofNat a : Shell q).val = a % q from rfl, val_zero] at hv424    exact eq_mul_of_mod_zero Pos.pos hv425  · intro ⟨k, hk⟩426    rw [hk]; exact Shell.ext (mod_zero_of_eq_mul Pos.pos rfl)427428/-! ## 22:C13 — the forced complex sector -/429430/-- 22:C13, 22:X2 — the shared core of two framed shells: an element of both cycles `C_{4κ}` and `C_{4κ'}` lies in `Q₄` when431the capacities are coprime (`κ a = κ' b + 1` the Bezout witness), and `Q₄` lies in every such cycle. -/432theorem shared_core {κ κ' a b : Nat} (hbez : κ * a = κ' * b + 1) (x : Shell q) (hx : x ^ (4 * κ) = 1)433    (hx' : x ^ (4 * κ') = 1) :434    x ^ 4 = 1 ∧ (∀ y : Shell q, y ^ 4 = 1 → y ^ (4 * κ) = 1 ∧ y ^ (4 * κ') = 1) := by435  constructor436  · have e1 : x ^ (4 * κ * a) = 1 := by rw [pow_mul, hx, one_pow]437    have e2 : 4 * κ * a = 4 * κ' * b + 4 := by rw [FRC.Nat.mul_assoc, hbez, Nat.mul_succ, FRC.Nat.mul_assoc]438    rw [e2, pow_add, pow_mul, hx', one_pow, one_mul] at e1439    exact e1440  · intro y hy441    exact ⟨by rw [pow_mul, hy, one_pow], by rw [pow_mul, hy, one_pow]⟩442443/-- 22:C13, 22:X2 — a shell `p ≡ 3 (mod 4)` has no quarter-turn: no `x` with `x² = −1`, since such an `x` has order `4`,444which divides `p − 1` by Fermat. -/445theorem no_quarter_turn (hq : FRC.Nat.isPrime q) (h3 : q % 4 = 3) : ¬ ∃ x : Shell q, x * x = -1 := by446  intro ⟨x, hx⟩447  have h2 : 2 < q := by448    match q, h3 with449    | 0, h => exact absurd h (by decide)450    | 1, h => exact absurd h (by decide)451    | 2, h => exact absurd h (by decide)452    | k + 3, _ => exact Nat.lt_of_lt_of_le (by decide) (Nat.le_add_left 3 k)453  have hx0 : x ≠ 0 := ne_zero_of_mul_self (neg_one_ne_zero hq) hx454  have h4 : x ^ 4 = 1 := by455    rw [show (4 : Nat) = 2 + 2 from rfl, pow_add, pow_two, hx, neg_mul_neg, mul_one]456  have hord : HasOrder x 4 := by457    refine ⟨by decide, h4, fun l hl hl0 => ?_⟩458    match l with459    | 0 => exact absurd hl0 (Nat.lt_irrefl 0)460    | k + 4 => exact absurd hl (Nat.not_lt_of_le (Nat.le_add_left 4 k))461    | 1 => rw [pow_one]; intro e; rw [e, mul_one] at hx; exact neg_one_ne_one h2 hx.symm462    | 2 => rw [pow_two, hx]; exact neg_one_ne_one h2463    | 3 =>464      rw [show (3 : Nat) = 2 + 1 from rfl, pow_add, pow_two, pow_one, hx, neg_one_mul]465      intro e466      have e' : x = -1 := by rw [← neg_neg x, e]467      rw [e', neg_mul_neg, mul_one] at hx468      exact neg_one_ne_one h2 hx.symm469  obtain ⟨c, hc⟩ := dvd_of_pow_eq_one hord (fermat hq hx0)470  have : (q - 1) % 4 = 0 := mod_zero_of_eq_mul (by decide) hc471  have hq1 : q = (q - 1) + 1 := (FRC.Nat.sub_add_cancel (Nat.le_of_lt (Nat.lt_trans (Nat.lt_succ_self 1) h2))).symm472  rw [hq1, FRC.Nat.add_mod _ _ _ (by decide), this] at h3473  exact absurd h3 (by decide)474475/-! ## 22:C24 — classicality is the index of the core -/476477/-- 22:C24, 22:X5 — with the core `C_d` of index `k` in the Object cycle `C_n = C_{dk}`: the Object is absorbed (classical,478one outcome per channel) exactly when `k = 1`, that is when its cycle is the core, and resolved (quantum) exactly when479`1 < k`, that is when the core is a proper subgroup. -/480theorem classicality_index {d k : Nat} (hd : 0 < d) :481    (k = 1 ↔ d * k = d) ∧ (1 < k ↔ d < d * k) := by482  constructor483  · constructor484    · intro h; exact h ▸ Nat.mul_one d485    · intro h486      exact Nat.eq_of_mul_eq_mul_left hd (h.trans (Nat.mul_one d).symm)487  · constructor488    · intro h489      calc d = d * 1 := (Nat.mul_one d).symm490        _ < d * k := Nat.mul_lt_mul_of_pos_left h hd491    · intro h492      match k with493      | 0 => rw [Nat.mul_zero] at h; exact absurd h (Nat.not_lt_zero d)494      | 1 => rw [Nat.mul_one] at h; exact absurd h (Nat.lt_irrefl d)495      | k + 2 => exact Nat.succ_lt_succ (Nat.zero_lt_succ k)496497/-! ## 22:C27 — the quarter-turn transport trichotomy -/498499/-- The three reductions of `ζ^{3κ}` on a label of order `4m`, read on the exponents (the raw form of 22:C27). -/500theorem transport_trichotomy_raw (hq : FRC.Nat.isPrime q) {ζ : Shell q} {m κ : Nat} (hζ : HasOrder ζ (4 * m)) :501    (ζ ^ (3 * κ) = ζ ^ (3 * m) ↔ (3 * κ) % (4 * m) = (3 * m) % (4 * m)) ∧502    (ζ ^ (3 * κ) = ζ ^ m ↔ (3 * κ) % (4 * m) = m % (4 * m)) ∧503    (ζ ^ (3 * κ) * ζ ^ (3 * κ) = 1 ↔ (3 * κ * 2) % (4 * m) = 0) :=504  ⟨pow_eq_pow_iff_mod hq hζ _ _, pow_eq_pow_iff_mod hq hζ _ _, by505    rw [← pow_add, ← Nat.mul_two]; exact pow_eq_one_iff_mod hq hζ _⟩506507/-- `(m x) % (m y) = m (x % y)` for `0 < m`, `0 < y` (the core's own modular lemma, no `propext`). -/508theorem mul_mod_mul_left' (m x y : Nat) (hm : 0 < m) (hy : 0 < y) : (m * x) % (m * y) = m * (x % y) := by509  match FRC.Nat.mod_spec y hy x with510  | ⟨k, hk⟩ =>511    have hlt : m * (x % y) < m * y := by512      rw [Nat.mul_comm m (x % y), Nat.mul_comm m y]; exact FRC.Nat.mul_lt_mul_of_lt_of_pos (Nat.mod_lt x hy) hm513    exact FRC.Nat.mod_unique hlt (by conv => lhs; rw [hk]; rw [Nat.mul_add, ← FRC.Nat.mul_assoc])514515/-- The three residue readings on the capacity `t = κ/m`, decided by the kernel over the residue `r = t % 4`. -/516theorem transport_residues : ∀ r, r < 4 →517    ((3 * r) % 4 = 3 ↔ r = 1) ∧ ((3 * r) % 4 = 1 ↔ (r + 1) % 4 = 0) ∧ ((6 * r) % 4 = 0 ↔ r % 2 = 0) := by decide518519/-- 22:C27 — the ambient quarter-turn `g^{−κ} = g^{3κ}` of a shell of capacity `κ` reduces onto an embedded label520`C_n`, `n = 4m` dividing `4κ` (`κ = m t`), generated by `ζ`, as `ζ^{3κ}`: it is the label's own quarter-turn `ζ^{3m}`521(faithful) exactly when `κ ≡ m (mod n)`, its conjugate `ζ^m` exactly when `κ + m ≡ 0 (mod n)`, and a sign (broken, no522quarter-turn: its square is `1`) exactly when `κ ≡ 0 (mod n/2)`, the complement of the two quarter-turn cases; for523`n = 4` the three cases are `κ ≡ 1`, `κ ≡ 3` and `κ` even, the residue mod `4`; on `C_{40}` the broken case is524`κ ≡ 0 (mod 20)`, the `𝔽_{641}` case (`κ = 160`). Off the embedding (`m ∤ κ`) the element `ζ^{3κ}` is not the525reduction of the ambient quarter-turn and the criterion does not apply. -/526theorem transport_trichotomy (hq : FRC.Nat.isPrime q) {ζ : Shell q} {m κ t : Nat} (hζ : HasOrder ζ (4 * m))527    (ht : κ = m * t) :528    (ζ ^ (3 * κ) = ζ ^ (3 * m) ↔ κ % (4 * m) = m) ∧529    (ζ ^ (3 * κ) = ζ ^ m ↔ (κ + m) % (4 * m) = 0) ∧530    (ζ ^ (3 * κ) * ζ ^ (3 * κ) = 1 ↔ κ % (2 * m) = 0) := by531  have hm : 0 < m := by532    match m, hζ.1 with533    | m + 1, _ => exact Nat.zero_lt_succ m534  have h4 : 0 < 4 := by decide535  have h2 : 0 < 2 := by decide536  have hr := transport_residues (t % 4) (Nat.mod_lt t h4)537  -- the residues of the three multiples of `κ = m t`, each `m` times a residue of `t`538  have e1 : (3 * κ) % (4 * m) = m * ((3 * t) % 4) := by539    rw [ht, Nat.mul_comm 4 m, ← FRC.Nat.mul_assoc, Nat.mul_comm 3 m, FRC.Nat.mul_assoc,540      mul_mod_mul_left' m (3 * t) 4 hm h4]541  have e2 : (3 * m) % (4 * m) = m * 3 := by542    rw [Nat.mul_comm 4 m, Nat.mul_comm 3 m, mul_mod_mul_left' m 3 4 hm h4]543  have e3 : κ % (4 * m) = m * (t % 4) := by rw [ht, Nat.mul_comm 4 m, mul_mod_mul_left' m t 4 hm h4]544  have e4 : (κ + m) % (4 * m) = m * ((t + 1) % 4) := by545    rw [ht, Nat.mul_comm 4 m, ← Nat.mul_succ, mul_mod_mul_left' m (t + 1) 4 hm h4]546  have e5 : (3 * κ * 2) % (4 * m) = m * ((6 * t) % 4) := by547    have e : 3 * (m * t) * 2 = m * (6 * t) := by548      rw [FRC.Nat.mul_left_comm 3 m t, FRC.Nat.mul_assoc, FRC.Nat.mul_assoc 3 t 2, Nat.mul_comm t 2,549        ← FRC.Nat.mul_assoc 3 2 t]550    rw [ht, e, Nat.mul_comm 4 m, mul_mod_mul_left' m (6 * t) 4 hm h4]551  have e6 : κ % (2 * m) = m * (t % 2) := by rw [ht, Nat.mul_comm 2 m, mul_mod_mul_left' m t 2 hm h2]552  have em : m % (4 * m) = m := by553    have := mul_mod_mul_left' m 1 4 hm h4554    rw [Nat.mul_one, Nat.mul_comm m 4] at this555    rw [this]556  have mod3 : (3 * t) % 4 = (3 * (t % 4)) % 4 := (FRC.Nat.mul_mod_mod 3 t 4 h4).symm557  have mod6 : (6 * t) % 4 = (6 * (t % 4)) % 4 := (FRC.Nat.mul_mod_mod 6 t 4 h4).symm558  have mod1 : (t + 1) % 4 = (t % 4 + 1) % 4 := (FRC.Nat.mod_add_mod t 1 4 h4).symm559  have mod2 : t % 2 = (t % 4) % 2 := by560    match FRC.Nat.mod_spec 4 h4 t with561    | ⟨k, hk⟩ =>562      conv => lhs; rw [hk]563      rw [show 4 * k + t % 4 = 2 * (2 * k) + t % 4 by rw [← FRC.Nat.mul_assoc], FRC.Nat.add_mul_mod_self_left _ _ _ h2]564  have cancel : ∀ a b : Nat, m * a = m * b ↔ a = b := fun a b =>565    ⟨fun e => Nat.eq_of_mul_eq_mul_left hm e, fun e => by rw [e]⟩566  have c1 : ∀ a : Nat, m * a = m ↔ a = 1 := fun a => by have := cancel a 1; rw [Nat.mul_one] at this; exact this567  have c0 : ∀ a : Nat, m * a = 0 ↔ a = 0 := fun a => by have := cancel a 0; rw [Nat.mul_zero] at this; exact this568  have t3 := transport_trichotomy_raw hq hζ (κ := κ)569  refine ⟨Iff.trans t3.1 ?_, Iff.trans t3.2.1 ?_, Iff.trans t3.2.2 ?_⟩570  · rw [e1, e2, e3]571    refine Iff.trans (cancel _ _) (Iff.trans ?_ (c1 _).symm)572    rw [mod3]; exact hr.1573  · rw [e1, e4, em]574    refine Iff.trans (c1 _) (Iff.trans ?_ (c0 _).symm)575    rw [mod3, mod1]; exact hr.2.1576  · rw [e5, e6]577    refine Iff.trans (c0 _) (Iff.trans ?_ (c0 _).symm)578    rw [mod6, mod2]; exact hr.2.2579580/-- 22:C27 — the three cases read on the capacity, decided by the kernel on the worked labels `C_{40}`, `Q₄` and581`C_{12}`: `3κ ≡ 3m`, `3κ ≡ m` and `6κ ≡ 0 (mod 4m)` are `κ ≡ m`, `κ + m ≡ 0` and `κ ≡ 0 (mod 2m)`, and on `C_{12}`582(`m = 3`, the embedded capacities `κ = 3t`) the faithful case is `κ ≡ 3 (mod 12)`. -/583theorem transport_cases :584    (∀ κ, κ < 40 → ((3 * κ) % 40 = (3 * 10) % 40 ↔ κ % 40 = 10 % 40) ∧ ((3 * κ) % 40 = 10 % 40 ↔ (κ + 10) % 40 = 0) ∧585      ((3 * κ * 2) % 40 = 0 ↔ κ % 20 = 0)) ∧586    (∀ κ, κ < 4 → ((3 * κ) % 4 = 3 % 4 ↔ κ % 4 = 1) ∧ ((3 * κ) % 4 = 1 % 4 ↔ κ % 4 = 3) ∧587      ((3 * κ * 2) % 4 = 0 ↔ κ % 2 = 0)) ∧588    (∀ t, t < 4 → ((3 * (3 * t)) % 12 = 9 % 12 ↔ (3 * t) % 12 = 3)) := by decide +kernel589590/-! ## 22:C6 — conjugation is inversion -/591592/-- 22:C6 — exponent negation inverts the phase cycle: `ζ^{n−k}` is the inverse of `ζ^k` on a cycle of order `n`. -/593theorem exponent_negation {ζ : Shell q} {n : Nat} (hζ : ζ ^ n = 1) {k : Nat} (hk : k ≤ n) :594    ζ ^ k * ζ ^ (n - k) = 1 := by rw [← pow_add, FRC.Nat.add_sub_of_le hk, hζ]595596section extension597open FRC.Extension FRC.Extension.Ext598599variable {ν : Shell q}600601/-- The inverse of a nonzero residue, `a^{p−2}`. -/602theorem inv_spec (hq : FRC.Nat.isPrime q) {a : Shell q} (ha : a ≠ 0) : a * a ^ (q - 2) = 1 := by603  have e : q - 2 + 1 = q - 1 := by604    match q, hq.1 with605    | k + 2, _ => rfl606  rw [Shell.mul_comm, ← pow_succ, e, fermat hq ha]607608/-- With `ν` a nonsquare, a zero norm forces zero: `a² = ν b²` has only the trivial solution. -/609theorem eq_zero_of_norm_eq_zero (hq : FRC.Nat.isPrime q) (hν : ¬ ∃ y : Shell q, y * y = ν) {z : Ext q ν}610    (h : norm z = 0) : z = 0 := by611  have hsq : z.re * z.re = ν * (z.im * z.im) := eq_of_sub_eq_zero h612  match Nat.decEq z.im.val 0 with613  | .isTrue him =>614    have him' : z.im = 0 := Shell.ext him615    rw [him', mul_zero, mul_zero] at hsq616    have hre : z.re = 0 := match mul_eq_zero hq hsq with | .inl a => a | .inr a => a617    exact Ext.ext hre him'618  | .isFalse him =>619    have him' : z.im ≠ 0 := fun e => him (by rw [e]; rfl)620    have hi := inv_spec hq him'621    exact absurd ⟨z.re * z.im ^ (q - 2), by622      calc (z.re * z.im ^ (q - 2)) * (z.re * z.im ^ (q - 2)) = (z.re * z.re) * (z.im ^ (q - 2) * z.im ^ (q - 2)) :=623            Shell.mul_mul_mul_comm _ _ _ _624        _ = ν * ((z.im * z.im ^ (q - 2)) * (z.im * z.im ^ (q - 2))) := by625            rw [hsq, Shell.mul_assoc, Shell.mul_mul_mul_comm]626        _ = ν := by rw [hi, Shell.mul_one, Shell.mul_one]⟩ hν627628/-- `𝔽_{p²}` has no zero divisors for `ν` a nonsquare. -/629theorem ext_mul_eq_zero (hq : FRC.Nat.isPrime q) (hν : ¬ ∃ y : Shell q, y * y = ν) {z z' : Ext q ν}630    (h : z * z' = 0) : z = 0 ∨ z' = 0 := by631  have hn : norm z * norm z' = 0 := by632    rw [← norm_mul, h]633    show norm (ofShell (0 : Shell q) : Ext q ν) = 0634    rw [norm_ofShell, Shell.mul_zero]635  match mul_eq_zero hq hn with636  | .inl e => exact .inl (eq_zero_of_norm_eq_zero hq hν e)637  | .inr e => exact .inr (eq_zero_of_norm_eq_zero hq hν e)638639theorem ext_add_neg (z : Ext q ν) : z + -z = 0 := Ext.ext (Shell.add_neg z.re) (Shell.add_neg z.im)640641theorem ext_sq_eq_sq (hq : FRC.Nat.isPrime q) (hν : ¬ ∃ y : Shell q, y * y = ν) {x y : Ext q ν}642    (h : x * x = y * y) : x = y ∨ x = -y := by643  have e : (x + -y) * (x + y) = 0 := by644    have e1 : (x + -y) * (x + y) = x * x + -(y * y) := Ext.ext645      (by show (x.re + -y.re) * (x.re + y.re) + ν * ((x.im + -y.im) * (x.im + y.im)) = (x.re * x.re + ν * (x.im * x.im)) + -(y.re * y.re + ν * (y.im * y.im))646          exact Shell.Frame.RE.sound (Shell.Frame.look [ν, x.re, x.im, y.re, y.im])647            (.add (.mul (.add (.var 1) (.neg (.var 3))) (.add (.var 1) (.var 3))) (.mul (.var 0) (.mul (.add (.var 2) (.neg (.var 4))) (.add (.var 2) (.var 4)))))648            (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.neg (.add (.mul (.var 3) (.var 3)) (.mul (.var 0) (.mul (.var 4) (.var 4))))))649            (by decide +kernel))650      (by show (x.re + -y.re) * (x.im + y.im) + (x.im + -y.im) * (x.re + y.re) = (x.re * x.im + x.im * x.re) + -(y.re * y.im + y.im * y.re)651          exact Shell.Frame.RE.sound (Shell.Frame.look [ν, x.re, x.im, y.re, y.im])652            (.add (.mul (.add (.var 1) (.neg (.var 3))) (.add (.var 2) (.var 4))) (.mul (.add (.var 2) (.neg (.var 4))) (.add (.var 1) (.var 3))))653            (.add (.add (.mul (.var 1) (.var 2)) (.mul (.var 2) (.var 1))) (.neg (.add (.mul (.var 3) (.var 4)) (.mul (.var 4) (.var 3)))))654            (by decide +kernel))655    rw [e1, h]; exact ext_add_neg _656  match ext_mul_eq_zero hq hν e with657  | .inl e' => exact .inl (calc x = (x + -y) + y := by rw [add_assoc', ext_neg_add, ext_add_zero]658      _ = 0 + y := by rw [e']659      _ = y := ext_zero_add y)660  | .inr e' => exact .inr (calc x = (x + y) + -y := by rw [add_assoc', ext_add_neg, ext_add_zero]661      _ = 0 + -y := by rw [e']662      _ = -y := ext_zero_add (-y))663where664  add_assoc' (a b c : Ext q ν) : a + b + c = a + (b + c) := Ext.ext (Shell.add_assoc _ _ _) (Shell.add_assoc _ _ _)665  ext_neg_add (z : Ext q ν) : -z + z = 0 := Ext.ext (Shell.neg_add z.re) (Shell.neg_add z.im)666  ext_add_zero (z : Ext q ν) : z + 0 = z := Ext.ext (Shell.add_zero z.re) (Shell.add_zero z.im)667  ext_zero_add (z : Ext q ν) : 0 + z = z := Ext.ext (Shell.zero_add z.re) (Shell.zero_add z.im)668669/-- Every element is `a + b w`. -/670theorem ext_decompose (z : Ext q ν) : z = ofShell z.re + ofShell z.im * w :=671  Ext.ext (by show z.re = z.re + (z.im * 0 + ν * (0 * 1)); rw [Shell.mul_zero, Shell.zero_mul, Shell.mul_zero, Shell.add_zero, Shell.add_zero])672    (by show z.im = 0 + (z.im * 1 + 0 * 0); rw [Shell.mul_one, Shell.zero_mul, Shell.add_zero, Shell.zero_add])673674/-- 22:C6 — the Frobenius is forced: a ring map `σ` of `𝔽_{p²}` fixing the shell (`σ(c) = c`, additive, multiplicative)675is the identity or the conjugation `w ↦ −w`, since `σ(w)² = ν` leaves `σ(w) = ±w`. -/676theorem frobenius_unique (hq : FRC.Nat.isPrime q) (hν : ¬ ∃ y : Shell q, y * y = ν) (σ : Ext q ν → Ext q ν)677    (hfix : ∀ c : Shell q, σ (ofShell c) = ofShell c) (hadd : ∀ z z', σ (z + z') = σ z + σ z')678    (hmul : ∀ z z', σ (z * z') = σ z * σ z') : (∀ z, σ z = z) ∨ (∀ z, σ z = conj z) := by679  have hw : σ w * σ w = w * w := by rw [← hmul, w_sq, hfix]680  match ext_sq_eq_sq hq hν hw with681  | .inl e => exact .inl (fun z => by682      conv => lhs; rw [ext_decompose z]683      rw [hadd, hmul, hfix, hfix, e, ← ext_decompose])684  | .inr e => exact .inr (fun z => by685      conv => lhs; rw [ext_decompose z]686      rw [hadd, hmul, hfix, hfix, e]687      exact Ext.ext688        (by show z.re + (z.im * -0 + ν * (0 * -1)) = z.re689            rw [Shell.neg_zero, Shell.mul_zero, Shell.zero_mul, Shell.mul_zero, Shell.add_zero, Shell.add_zero])690        (by show 0 + (z.im * -1 + 0 * -0) = -z.im691            rw [← Shell.mul_neg, Shell.mul_one, Shell.zero_mul, Shell.add_zero, Shell.zero_add]))692693/-- 22:C6, 22:A2, 22:P4 — on the norm-one torus the conjugation is the inversion: `z · conj z = 1`. -/694theorem torus_conj_inv (z : Ext q ν) (hz : norm z = 1) : z * conj z = 1 := conj_inv_of_norm_one z hz695696end extension697698end FRC.Observation699