Theme/Subject.lean — FrcCore

1import FrcCore.Theme.Field2import FrcCore.FrameCore3import FrcCore.Parity4import FrcCore.Theme.Quadratic56/-!7# FrcCore.Theme.Subject — the Subject: the frame, the signature, the square class, the chirality (the subject theme)89Master block C, task LM24, on the Subject's frame `(τ; 0, 1, g)` (`FrameCore.lean`, `Parity.lean`) and on the prime10shell without a generator (`Theme/Field.lean`, `Theme/Quadratic.lean`):1112* **C1** the frame's web: `2π ≡ −1`, `g^π = −1`, `−π = 2⁻¹`, `i² = −1`, `g` the one nonsquare datum (`frame_web`);13* **C3** the signature: the norm form `x² − ν t²` is isotropic iff `ν` is a square, `ν = 2⁻¹ · 2g`, the classes of14  `2⁻¹` and `2g` fixed by the parity of `κ` (`signature`);15* **C8** the square class is chronon parity (`square_class`);16* **C13** its part 10:G2, the exponent-window ladder on every capacity, the threshold `κ ≥ 17` exact (`exponent_ladder`);17* **C14** the quarter-turn is the odd member of the `±√−1` pair, the conjugate chart toggles it, and the parity names18  the chirality class of the generator (`quarter_turn_odd`);19* **C16** the spinor dichotomy: `κ` odd iff `v₂(p − 1) = 2` iff the fold `(r, s) ↦ iʳ g^{4s}` is a bijection20  `C₄ × C_κ → 𝔽_p^×` iff `3κr + 4s ≡ 1 (mod 4κ)` is solvable; the shared 2-part and the cover degree (`spinor`);21* **C20** the mass–energy channel: `C_{p−1}` meets `C_{p+1}` in `±1` and `C_{2(p+1)}` in `Q₄`, `N(i) = −1` (`channel`);22* **C25** the horizon is the origin's antipode on the boost torus: the torsor map `P¹ → C_{p+1}`, `P ↦ u_P/ū_P`, is an23  equivariant bijection sending the origin to `1` and the horizon to `−1`, exchanged by the torus's one involution24  `q ↦ ν/q`; the additive antipode is no residue (`horizon_antipode`). No axioms.25-/2627namespace FRC.Subject2829open FRC.Shell3031variable {p : Nat} [Pos p]3233/-! ## Two helpers: a frame's shell is prime, and the inverse on a prime shell -/3435/-- A frame's shell is prime: it has no zero divisors, and completeness is primality. -/36theorem frame_isPrime {κ : Nat} {g : Shell p} (F : Frame p κ g) : FRC.Nat.isPrime p :=37  Prime.isPrime_of_no_zero_divisors (Nat.le_of_lt F.two_lt_p) (fun h => F.mul_eq_zero h)3839/-- The inverse on a prime shell, `a⁻¹ = a^{p−2}` (Fermat). -/40def inv (a : Shell p) : Shell p := a ^ (p - 2)4142theorem mul_inv (hp : FRC.Nat.isPrime p) {a : Shell p} (ha : a ≠ 0) : a * inv a = 1 := by43  have e : p - 1 = p - 2 + 1 := by44    match p, hp.1 with45    | k + 2, _ => rfl46  rw [mul_comm, inv, ← pow_succ, ← e, Prime.fermat hp ha]4748theorem inv_ne_zero (hp : FRC.Nat.isPrime p) {a : Shell p} (ha : a ≠ 0) : inv a ≠ 0 := fun h => by49  have := mul_inv hp ha; rw [h, mul_zero] at this; exact Prime.one_ne_zero hp this.symm5051theorem even_add {a b : Nat} (h : (a + b) % 2 = 0) : a % 2 = 0 ↔ b % 2 = 0 := by52  rw [FRC.Nat.add_mod _ _ _ (Nat.zero_lt_succ 1)] at h53  constructor54  · intro ha; rw [ha, Nat.zero_add, FRC.Nat.mod_mod _ _ (Nat.zero_lt_succ 1)] at h; exact h55  · intro hb; rw [hb, Nat.add_zero, FRC.Nat.mod_mod _ _ (Nat.zero_lt_succ 1)] at h; exact h5657/-! ## C1: the frame's web -/5859/-- **C1 (p00021), the frame's web.** On every frame, `π = 2κ` and `i = −g^κ`: `2π ≡ −1`, `g^π = −1`, `−π = 2⁻¹`,60`i² = −1`; `0` and `1` are squares and the drive is not, the one nonsquare frame datum. -/61theorem frame_web {κ : Nat} {g : Shell p} (F : Frame p κ g) :62    (ofNat (2 * Frame.halfPeriod κ) : Shell p) = -1 ∧ g ^ Frame.halfPeriod κ = -1 ∧63    -(ofNat (Frame.halfPeriod κ) : Shell p) * 2 = 1 ∧ Frame.quarterTurn g κ * Frame.quarterTurn g κ = -1 ∧64    (∃ y : Shell p, y * y = 0) ∧ (∃ y : Shell p, y * y = 1) ∧ ¬ ∃ y : Shell p, y * y = g := by65  refine ⟨F.two_pi, F.half_period, ?_, F.quarter_turn_sq, ⟨0, mul_zero 0⟩, ⟨1, mul_one 1⟩, F.drive_nonsquare⟩66  have e : (ofNat (Frame.halfPeriod κ) : Shell p) * 2 = -1 := by67    rw [show (2 : Shell p) = ofNat 2 from rfl, Prime.ofNat_mul, Nat.mul_comm]; exact F.two_pi68  rw [← neg_mul, e, neg_neg]6970/-! ## C3: the signature -/7172/-- **C3 (p00150), the Euclidean–Lorentzian dichotomy.** On every frame the temporal coefficient `ν = g` is a73nonsquare; the norm form `x² − ν t²` has a zero with `t ≠ 0` iff `ν` is a square (split torus) and none otherwise74(non-split); `ν = 2⁻¹ · (2g)`, and the classes of `2⁻¹` and `2g` are fixed by the parity of `κ`. -/75theorem signature {κ : Nat} {g : Shell p} (F : Frame p κ g) :76    (¬ ∃ y : Shell p, y * y = g) ∧77    (∀ ν : Shell p, (∃ t x : Shell p, t ≠ 0 ∧ x * x = ν * (t * t)) ↔ ∃ w : Shell p, w * w = ν) ∧78    (∀ h : Shell p, 2 * h = 1 → h * (2 * g) = g ∧ ((∃ r : Shell p, r * r = h) ↔ κ % 2 = 0) ∧79      ((∃ r : Shell p, r * r = 2 * g) ↔ κ % 2 = 1)) := by80  have hp := frame_isPrime F81  refine ⟨F.drive_nonsquare, fun ν => ⟨fun ⟨t, x, ht, e⟩ => ?_, fun ⟨w, hw⟩ => ⟨1, w, F.one_ne_zero, by rw [mul_one, mul_one, hw]⟩⟩,82    fun h h2 => ?_⟩83  · obtain ⟨s, hs⟩ := F.exists_inv ht84    exact ⟨x * s, by rw [mul_mul_mul_comm, e, mul_assoc, ← mul_mul_mul_comm, hs, mul_one, mul_one]⟩85  · have hh0 : h ≠ 0 := fun e => by rw [e, mul_zero] at h2; exact F.one_ne_zero h2.symm86    have hh : h = ofNat (2 * κ + 1) :=87      Prime.mul_left_cancel hp F.two_ne_zero (h2.trans (Prime.two_mul_chart_half F.cap).symm)88    have hsq : (∃ r : Shell p, r * r = h) ↔ κ % 2 = 0 := by rw [hh]; exact Prime.half_square_iff hp F.cap89    refine ⟨by rw [← mul_assoc, mul_comm h 2, h2, one_mul], hsq, ?_⟩90    obtain ⟨a, _, ha⟩ := F.eq_pow_of_ne_zero hh091    obtain ⟨b, _, hb⟩ := F.eq_pow_of_ne_zero F.two_ne_zero92    have hab : (a + b) % 2 = 0 := by93      have h1 : g ^ (a + b) = 1 := by rw [pow_add, ha, hb, mul_comm]; exact h294      obtain ⟨q, hq⟩ := FRC.Nat.mod_spec (p - 1) F.n_pos (a + b)95      rw [F.mod_eq_zero_of_pow_eq_one h1, Nat.add_zero, F.n_eq, FRC.Nat.mul_assoc] at hq96      rw [hq, show 4 = 2 * 2 from rfl, FRC.Nat.mul_assoc]; exact Frame.two_mul_mod _97    have h2g : 2 * g = g ^ (b + 1) := by rw [pow_succ, hb]98    rw [h2g]99    refine (F.parity_iff (b + 1)).trans ((Frame.succ_mod_two_eq_zero_iff b).trans ?_)100    have hA : a % 2 = 0 ↔ κ % 2 = 0 := (F.parity_iff a).symm.trans (by rw [ha]; exact hsq)101    constructor102    · intro hb1103      match Frame.mod_two_cases κ with104      | .inr e => exact e105      | .inl e => rw [(even_add hab).1 (hA.2 e)] at hb1; exact absurd hb1 (by decide)106    · intro hk107      match Frame.mod_two_cases b with108      | .inr e => exact e109      | .inl e => rw [hA.1 ((even_add hab).2 e)] at hk; exact absurd hk (by decide)110111/-! ## C8: the square class is chronon parity -/112113/-- **C8 (p00028), the square class is chronon parity.** On every frame `g^m` is a square iff `m` is even: the114registered (two-way) transport `g²` is even, the one-way multiplier `g` and its inverse odd. -/115theorem square_class {κ : Nat} {g : Shell p} (F : Frame p κ g) :116    (∀ m : Nat, (∃ y : Shell p, y * y = g ^ m) ↔ m % 2 = 0) ∧ (¬ ∃ y : Shell p, y * y = g) ∧117    (∀ y : Shell p, g * y = 1 → ¬ ∃ r : Shell p, r * r = y) ∧ (∃ y : Shell p, y * y = g * g) :=118  ⟨F.parity_iff, F.drive_nonsquare, fun _ hy => F.inv_drive_nonsquare hy, ⟨g, rfl⟩⟩119120/-- The Carrier's class `[c²] = [2⁻¹]` (C3, C8): on a prime `p = 4S + 1`, the half `h` (`2h = 1`) is a square iff `S`121is even; the half is `2S + 1` (`Prime.half_square_iff`). -/122theorem half_class (hp : FRC.Nat.isPrime p) {S : Nat} (hS : p = 4 * S + 1) :123    ∀ h : Shell p, 2 * h = 1 → ((∃ c : Shell p, c * c = h) ↔ S % 2 = 0) := fun h h2 => by124  have hh : h = ofNat (2 * S + 1) :=125    calc h = h * (2 * ofNat (2 * S + 1)) := by rw [Prime.two_mul_chart_half hS, mul_one]126      _ = 2 * h * ofNat (2 * S + 1) := by rw [← mul_assoc, mul_comm h 2]127      _ = ofNat (2 * S + 1) := by rw [h2, one_mul]128  rw [hh]; exact Prime.half_square_iff hp hS129130/-! ## C20: the mass–energy channel -/131132/-- 38:A3, 22:A2, 22:P4 — **C20 (p00040), the mass–energy channel**, generator-free on a prime `p` with a quarter-turn `h² = −1`: inside133`𝔽_{p²}^×`, `C_{p−1} = 𝔽_p^×` meets the boost torus `C_{p+1} = {z^{p+1} = 1}` in the sign `±1` alone, and the spinor134cover `C_{2(p+1)}` in exactly `Q₄ = {±1, ±h}`; the quarter is spinorial, `N(h) = h^{p+1} = h² = −1`. -/135theorem channel (hp : FRC.Nat.isPrime p) {h : Shell p} (hh : h * h = -1) :136    (∀ x : Shell p, x ≠ 0 → (x ^ (p + 1) = 1 ↔ x = 1 ∨ x = -1)) ∧137    (∀ x : Shell p, x ≠ 0 → (x ^ (2 * (p + 1)) = 1 ↔ x = 1 ∨ x = -1 ∨ x = h ∨ x = -h)) ∧ h ^ (p + 1) = -1 := by138  have e : p + 1 = p - 1 + 2 := by139    match p, hp.1 with140    | k + 2, _ => rfl141  have hN : ∀ x : Shell p, x ≠ 0 → x ^ (p + 1) = x * x := fun x hx => by142    rw [e, pow_add, Prime.fermat hp hx, one_mul, pow_two]143  have h0 : h ≠ 0 := Prime.ne_zero_of_mul_self (Prime.neg_one_ne_zero hp) hh144  have hsq1 : ∀ x : Shell p, x * x = 1 ↔ x = 1 ∨ x = -1 := fun x =>145    ⟨Prime.sq_eq_one hp, fun hx => match hx with146      | .inl e => by rw [e, mul_one]147      | .inr e => by rw [e, neg_mul_neg, mul_one]⟩148  refine ⟨fun x hx => by rw [hN x hx]; exact hsq1 x, fun x hx => ?_, by rw [hN h h0, hh]⟩149  rw [show 2 * (p + 1) = (p + 1) * 2 from Nat.mul_comm 2 (p + 1), pow_mul, hN x hx, pow_two]150  refine (hsq1 (x * x)).trans ?_151  constructor152  · intro hx2153    match hx2 with154    | .inl e1 => exact match (hsq1 x).1 e1 with155      | .inl a => .inl a156      | .inr a => .inr (.inl a)157    | .inr e1 => exact match Prime.sq_eq_sq hp (e1.trans hh.symm) with158      | .inl a => .inr (.inr (.inl a))159      | .inr a => .inr (.inr (.inr a))160  · intro hx161    match hx with162    | .inl a => exact .inl ((hsq1 x).2 (.inl a))163    | .inr (.inl a) => exact .inl ((hsq1 x).2 (.inr a))164    | .inr (.inr (.inl a)) => exact .inr (by rw [a, hh])165    | .inr (.inr (.inr a)) => exact .inr (by rw [a, neg_mul_neg, hh])166167/-- 38:A4 — C20's Carrier instance: on `Ω = 233`, `78^58 = 89 = ħ`, a root of `−1`. -/168theorem channel_233 : (78 : Shell 233) ^ 58 = 89 ∧ (89 : Shell 233) * 89 = -1 := by decide169170/-! ## C13's part 10:G2: the exponent-window ladder on every capacity -/171172/-- **10:G2 (p10038), the exponent-window ladder, on every capacity** (C13's first part; the key is paper 10's): coherence173`2√κ` lies below recovery `κ/2` iff `16κ < κ²` iff `κ ≥ 17`, so the threshold is exact and the toy `κ = 3` fails;174recovery `κ/2` below flag inaccessibility `κ`, and the flag below covariance `2κ`, both `κ < 2κ`; and the coherence175identity `(2√κ)² = 4κ = p − 1` on `p = 4κ + 1`. -/176theorem exponent_ladder :177    (∀ κ : Nat, 16 * κ < κ * κ ↔ 17 ≤ κ) ∧ (∀ κ : Nat, 0 < κ → κ < 2 * κ) ∧ (∀ κ : Nat, 2 * 2 * κ = 4 * κ + 1 - 1) := by178  refine ⟨fun κ => ⟨fun h => ?_, fun h => FRC.Nat.mul_lt_mul_of_lt_of_pos h (Nat.lt_of_lt_of_le (by decide) h)⟩,179    fun κ hκ => ?_, fun κ => rfl⟩180  · match Nat.lt_or_ge κ 17 with181    | .inr h' => exact h'182    | .inl h' => exact absurd (Nat.lt_of_lt_of_le h (Nat.mul_le_mul_right κ (Nat.le_of_lt_succ h'))) (Nat.lt_irrefl _)183  · have := FRC.Nat.mul_lt_mul_of_lt_of_pos (by decide : 1 < 2) hκ184    rwa [Nat.one_mul] at this185186/-! ## C14: the quarter-turn is the odd member of the `±√−1` pair -/187188theorem parity_ne {a b : Nat} (h : a % 2 = 0 ↔ ¬ b % 2 = 0) : a % 2 ≠ b % 2 := fun e =>189  match Frame.mod_two_cases a with190  | .inl ha => h.1 ha (e ▸ ha)191  | .inr ha => (show a % 2 ≠ 0 by rw [ha]; decide) (h.2 (by rw [← e, ha]; decide))192193/-- **C14 (p00034), the quarter-turn is the odd member of the `±√−1` pair.** On every frame: the Euler identity194`e^{iπ} := (g^i)^{i·2κ} = (−1)^i` for every lift `i`; the two roots of `−1` have representatives of opposite parity,195so `e^{iπ} = −1` holds exactly on the odd one; the conjugate chart (the inverse drive) is a frame and toggles the196quarter-turn; and every frame is `g^u` with `u` odd, its quarter-turn the same as `g`'s when `u ≡ 1 (mod 4)` and the197negative when `u ≡ 3`, so the parity of the quarter-turn names the chirality class. -/198theorem quarter_turn_odd {κ : Nat} {g : Shell p} (F : Frame p κ g) :199    (∀ i : Nat, (g ^ i) ^ (i * (2 * κ)) = if i % 2 = 0 then 1 else -1) ∧200    (∀ h : Shell p, h * h = -1 → (h.val % 2 = 0 ↔ ¬ (-h).val % 2 = 0)) ∧201    (∀ h : Shell p, h * h = -1 → ((g ^ h.val) ^ (h.val * (2 * κ)) = -1 ↔ h.val % 2 = 1)) ∧202    (∀ y : Shell p, g * y = 1 → Frame p κ y ∧ Frame.quarterTurn y κ = -Frame.quarterTurn g κ) ∧203    (∀ g' : Shell p, Frame p κ g' → ∃ u : Nat, u < p - 1 ∧ g ^ u = g' ∧ (u % 4 = 1 ∨ u % 4 = 3) ∧204      (u % 4 = 1 → Frame.quarterTurn g' κ = Frame.quarterTurn g κ) ∧205      (u % 4 = 3 → Frame.quarterTurn g' κ = -Frame.quarterTurn g κ) ∧206      ((Frame.quarterTurn g' κ).val % 2 = (Frame.quarterTurn g κ).val % 2 ↔ u % 4 = 1)) := by207  have hp := frame_isPrime F208  have hroot : ∀ h : Shell p, h * h = -1 → h ≠ 0 := fun h hh => Prime.ne_zero_of_mul_self (Prime.neg_one_ne_zero hp) hh209  have hflip : ∀ x : Shell p, x ≠ 0 → (x.val % 2 = 0 ↔ ¬ (-x).val % 2 = 0) := fun x hx => Prime.parity_flips F.cap hx210  refine ⟨F.euler_identity, fun h hh => hflip h (hroot h hh), fun h _ => ?_, fun y hy => ?_, fun g' F' => ?_⟩211  · rw [F.euler_identity]212    match Frame.mod_two_cases h.val with213    | .inl e => rw [ite_eq_left e, e]214                exact ⟨fun e1 => absurd e1.symm (Prime.neg_one_ne_one F.two_lt_p), fun e1 => absurd e1 (by decide)⟩215    | .inr e => rw [ite_eq_right (by rw [e]; decide), e]; exact ⟨fun _ => rfl, fun _ => rfl⟩216  · have hpow : ∀ l, g ^ l * y ^ l = 1 := fun l => by rw [← mul_pow, hy, one_pow]217    have Fy : Frame p κ y := ⟨F.cap, F.cap_pos,218      ⟨by have := hpow (p - 1); rwa [F.pow_n, one_mul] at this,219       fun l hl hl0 e => F.prim.2 l hl hl0 (by have := hpow l; rwa [e, mul_one] at this)⟩⟩220    refine ⟨Fy, ?_⟩221    have e1 : g ^ κ * y ^ κ = g ^ κ * -(g ^ κ) := by222      rw [hpow κ, ← mul_neg, ← pow_add, ← Nat.two_mul, F.half_period, neg_neg]223    show -(y ^ κ) = -(-(g ^ κ))224    rw [Prime.mul_left_cancel hp (F.pow_ne_zero κ) e1]225  · obtain ⟨u, hu, hgu⟩ := F.eq_pow_of_ne_zero F'.g_ne_zero226    have hodd : u % 2 = 1 := match Frame.mod_two_cases u with227      | .inr e => e228      | .inl e => absurd (hgu ▸ (F.parity_iff u).2 e) F'.drive_nonsquare229    have h4 : u % 4 = 1 ∨ u % 4 = 3 := by230      obtain ⟨q, hq⟩ := FRC.Nat.mod_spec 4 (by decide) u231      have hm : (u % 4) % 2 = 1 := by rw [← Frame.mod_two_of_mod_four_mul (u % 4) q, ← hq]; exact hodd232      have hlt := Nat.mod_lt u (by decide : 0 < 4)233      generalize u % 4 = r at hm hlt ⊢234      match r, hm, hlt with235      | 1, _, _ => exact .inl rfl236      | 3, _, _ => exact .inr rfl237      | 0, hm, _ => exact absurd hm (by decide)238      | 2, hm, _ => exact absurd hm (by decide)239      | k + 4, _, hlt => exact absurd hlt (Nat.not_lt_of_le (Nat.le_add_left 4 k))240    have hq1 : u % 4 = 1 → Frame.quarterTurn g' κ = Frame.quarterTurn g κ := fun e => by241      rw [← hgu]; exact (F.orientation_class u).1 e242    have hq3 : u % 4 = 3 → Frame.quarterTurn g' κ = -Frame.quarterTurn g κ := fun e => by243      rw [← hgu]; exact (F.orientation_class u).2 e244    refine ⟨u, hu, hgu, h4, hq1, hq3, fun hpar => ?_, fun e => by rw [hq1 e]⟩245    match h4 with246    | .inl e => exact e247    | .inr e =>248      rw [hq3 e] at hpar249      exact absurd hpar.symm (parity_ne (hflip _ (hroot _ F.quarter_turn_sq)))250251/-! ## C16: the spinor dichotomy -/252253/-- `n = 4q + r`, `r < 4`, by counting: no division. -/254def qr4 : Nat → Nat × Nat255  | 0 => (0, 0)256  | n + 1 => if (qr4 n).2 = 3 then ((qr4 n).1 + 1, 0) else ((qr4 n).1, (qr4 n).2 + 1)257258theorem qr4_spec : ∀ n, n = 4 * (qr4 n).1 + (qr4 n).2 ∧ (qr4 n).2 < 4259  | 0 => ⟨rfl, by decide⟩260  | n + 1 => by261    have ih := qr4_spec n262    show n + 1 = 4 * (if (qr4 n).2 = 3 then ((qr4 n).1 + 1, 0) else ((qr4 n).1, (qr4 n).2 + 1)).1 +263      (if (qr4 n).2 = 3 then ((qr4 n).1 + 1, 0) else ((qr4 n).1, (qr4 n).2 + 1)).2 ∧264      (if (qr4 n).2 = 3 then ((qr4 n).1 + 1, 0) else ((qr4 n).1, (qr4 n).2 + 1)).2 < 4265    generalize qr4 n = x at ih ⊢266    obtain ⟨q, r⟩ := x267    obtain ⟨e, hr⟩ := ih268    change n = 4 * q + r at e269    change r < 4 at hr270    show n + 1 = 4 * (if r = 3 then (q + 1, 0) else (q, r + 1)).1 + (if r = 3 then (q + 1, 0) else (q, r + 1)).2 ∧271      (if r = 3 then (q + 1, 0) else (q, r + 1)).2 < 4272    match Nat.decEq r 3 with273    | .isTrue h3 =>274      rw [ite_eq_left h3, e, h3]275      exact ⟨by show 4 * q + 3 + 1 = 4 * (q + 1) + 0; rw [Nat.left_distrib], by show 0 < 4; decide⟩276    | .isFalse h3 =>277      rw [ite_eq_right h3, e]278      exact ⟨Nat.add_assoc _ _ _, Nat.succ_lt_succ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hr) h3)⟩279280/-- The fold `iʳ (g⁴)ˢ = g^{3κr + 4s}` (`i = −g^κ = g^{3κ}`). -/281theorem fold_eq {κ : Nat} {g : Shell p} (F : Frame p κ g) (r s : Nat) :282    Frame.quarterTurn g κ ^ r * (g ^ 4) ^ s = g ^ (3 * κ * r + 4 * s) := by283  have hi : Frame.quarterTurn g κ = g ^ (3 * κ) := by284    show -(g ^ κ) = g ^ (3 * κ)285    rw [show 3 * κ = 2 * κ + κ by rw [Nat.succ_mul, Nat.add_comm], pow_add, F.half_period, neg_one_mul]286  rw [hi, ← pow_mul, ← pow_mul, ← pow_add]287288theorem pow_ne_zero (hp : FRC.Nat.isPrime p) {x : Shell p} (hx : x ≠ 0) : ∀ k : Nat, x ^ k ≠ 0289  | 0 => Prime.one_ne_zero hp290  | k + 1 => Prime.mul_ne_zero hp (pow_ne_zero hp hx k) hx291292/-- An element with `j² = −1` tells `0, 1, 2, 3` apart: `jʳ = jʳ'` with `r, r' < 4` gives `r = r'`. -/293theorem quarter_pow_inj (hp : FRC.Nat.isPrime p) (h2 : 2 < p) {j : Shell p} (hj : j * j = -1) :294    ∀ {r r' : Nat}, r < 4 → r' < 4 → j ^ r = j ^ r' → r = r' := by295  have hne : (-1 : Shell p) ≠ 1 := Prime.neg_one_ne_one h2296  have hj0 : j ≠ 0 := Prime.ne_zero_of_mul_self (Prime.neg_one_ne_zero hp) hj297  have one : ∀ d, d < 4 → j ^ d = 1 → d = 0 := fun d hd e => by298    match d, hd, e with299    | 0, _, _ => rfl300    | 1, _, e => rw [pow_one] at e; rw [e, mul_one] at hj; exact absurd hj.symm hne301    | 2, _, e => rw [pow_two, hj] at e; exact absurd e hne302    | 3, _, e =>303      rw [show (3 : Nat) = 2 + 1 from rfl, pow_succ, pow_two, hj, neg_one_mul] at e304      rw [← neg_neg j, e, neg_mul_neg, mul_one] at hj; exact absurd hj.symm hne305    | k + 4, hd, _ => exact absurd hd (Nat.not_lt_of_le (Nat.le_add_left 4 k))306  have key : ∀ {r r' : Nat}, r' ≤ r → r < 4 → j ^ r = j ^ r' → r = r' := fun {r r'} hle hr e => by307    have e1 : j ^ r' * j ^ (r - r') = j ^ r' * 1 := by rw [← pow_add, FRC.Nat.add_sub_of_le hle, mul_one, e]308    have h0 := one (r - r') (Nat.lt_of_le_of_lt (Nat.sub_le r r') hr)309      (Prime.mul_left_cancel hp (pow_ne_zero hp hj0 r') e1)310    rw [← FRC.Nat.add_sub_of_le hle, h0, Nat.add_zero]311  intro r r' hr hr' e312  match Nat.lt_or_ge r r' with313  | .inl hlt => exact (key (Nat.le_of_lt hlt) hr' e.symm).symm314  | .inr hge => exact key hge hr e315316/-- 38:A2 — **C16 (p00151), the spinor dichotomy**, on every frame (`p − 1 = 4κ`, `i = −g^κ`): `κ` is odd iff317`v₂(p − 1) = 2` (`8 ∤ p − 1`) iff the fold `(r, s) ↦ iʳ (g⁴)ˢ` is injective on `C₄ × C_κ`, and then onto `𝔽_p^×`, so318`C_{p−1} ≅ C₄ × C_κ`; and iff `3κr + 4s ≡ 1 (mod 4κ)` is solvable. -/319theorem spinor {κ : Nat} {g : Shell p} (F : Frame p κ g) :320    (κ % 2 = 1 ↔ (p - 1) % 8 ≠ 0) ∧321    (κ % 2 = 1 ↔ ∀ r s r' s' : Nat, r < 4 → s < κ → r' < 4 → s' < κ →322        Frame.quarterTurn g κ ^ r * (g ^ 4) ^ s = Frame.quarterTurn g κ ^ r' * (g ^ 4) ^ s' → r = r' ∧ s = s') ∧323    (κ % 2 = 1 → ∀ x : Shell p, x ≠ 0 → ∃ r s : Nat, r < 4 ∧ s < κ ∧ Frame.quarterTurn g κ ^ r * (g ^ 4) ^ s = x) ∧324    (κ % 2 = 1 ↔ ∃ r s : Nat, r < 4 ∧ s < κ ∧ (3 * κ * r + 4 * s) % (4 * κ) = 1) := by325  have hp := frame_isPrime F326  have h2 := F.two_lt_p327  have hn := F.n_eq328  have hq := F.quarter_turn_sq329  have hi0 : Frame.quarterTurn g κ ≠ 0 := Prime.ne_zero_of_mul_self (Prime.neg_one_ne_zero hp) hq330  have h4κ : 0 < 4 * κ := Nat.mul_pos (by decide) F.cap_pos331  -- injectivity on an odd capacity332  have inj : κ % 2 = 1 → ∀ r s r' s' : Nat, r < 4 → s < κ → r' < 4 → s' < κ →333      Frame.quarterTurn g κ ^ r * (g ^ 4) ^ s = Frame.quarterTurn g κ ^ r' * (g ^ 4) ^ s' → r = r' ∧ s = s' := by334    intro hk r s r' s' hr hs hr' hs' e335    have kill : ∀ t : Nat, ((g ^ 4) ^ t) ^ κ = 1 := fun t => by336      rw [← pow_mul, ← pow_mul, show 4 * (t * κ) = 4 * κ * t by rw [Nat.mul_comm t κ, FRC.Nat.mul_assoc],337        pow_mul, ← hn, F.pow_n, one_pow]338    have ej : (Frame.quarterTurn g κ ^ κ) ^ r = (Frame.quarterTurn g κ ^ κ) ^ r' := by339      have this : (Frame.quarterTurn g κ ^ r * (g ^ 4) ^ s) ^ κ = (Frame.quarterTurn g κ ^ r' * (g ^ 4) ^ s') ^ κ := by340        rw [e]341      rw [mul_pow, mul_pow, kill, kill, mul_one, mul_one, pow_mul_comm, pow_mul_comm (Frame.quarterTurn g κ) r'] at this342      exact this343    have hjj : Frame.quarterTurn g κ ^ κ * Frame.quarterTurn g κ ^ κ = -1 := by344      rw [← pow_add, ← Nat.two_mul, pow_mul, pow_two, hq, neg_one_pow, ite_eq_right (by rw [hk]; decide)]345    have hrr := quarter_pow_inj hp h2 hjj hr hr' ej346    subst hrr347    have e2 := Prime.mul_left_cancel hp (pow_ne_zero hp hi0 r) e348    rw [← pow_mul, ← pow_mul] at e2349    have h4s : ∀ t, t < κ → 4 * t < p - 1 := fun t ht => by350      rw [hn, Nat.mul_comm 4 t, Nat.mul_comm 4 κ]; exact FRC.Nat.mul_lt_mul_of_lt_of_pos ht (by decide : 0 < 4)351    exact ⟨rfl, Nat.eq_of_mul_eq_mul_left (by decide : 0 < 4) (F.pow_inj (h4s s hs) (h4s s' hs') e2)⟩352  have notinj : κ % 2 = 0 → ¬ ∀ r s r' s' : Nat, r < 4 → s < κ → r' < 4 → s' < κ →353      Frame.quarterTurn g κ ^ r * (g ^ 4) ^ s = Frame.quarterTurn g κ ^ r' * (g ^ 4) ^ s' → r = r' ∧ s = s' := by354    intro he hall355    obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 (by decide) κ356    rw [he, Nat.add_zero] at hm357    have hm0 : 0 < m := by358      match m, hm with359      | 0, hm => have := F.cap_pos; rw [hm] at this; exact absurd this (Nat.lt_irrefl 0)360      | k + 1, _ => exact Nat.zero_lt_succ k361    have hmκ : m < κ := by rw [hm, Nat.two_mul]; exact Nat.lt_add_of_pos_right hm0362    have h4m : 4 * m = 2 * κ := by rw [hm, ← FRC.Nat.mul_assoc]363    have e : Frame.quarterTurn g κ ^ 2 * (g ^ 4) ^ 0 = Frame.quarterTurn g κ ^ 0 * (g ^ 4) ^ m := by364      rw [pow_two, hq, pow_zero, mul_one, pow_zero, one_mul, ← pow_mul, h4m, F.half_period]365    exact absurd (hall 2 0 0 m (by decide) F.cap_pos (by decide) hmκ e).1 (by decide)366  have hp' : p = p - 1 + 1 := (FRC.Nat.sub_add_cancel Pos.pos).symm367  have surj : κ % 2 = 1 → ∀ x : Shell p, x ≠ 0 →368      ∃ r s : Nat, r < 4 ∧ s < κ ∧ Frame.quarterTurn g κ ^ r * (g ^ 4) ^ s = x := by369    intro hk x hx370    have hy : ∀ n, Frame.quarterTurn g κ ^ (qr4 n).2 * (g ^ 4) ^ (qr4 n).1 ≠ 0 := fun n =>371      Prime.mul_ne_zero hp (pow_ne_zero hp hi0 _) (pow_ne_zero hp (pow_ne_zero hp F.g_ne_zero 4) _)372    have hq4 : ∀ n, n < p - 1 → (qr4 n).1 < κ := fun n hn' => by373      have h1 : 4 * (qr4 n).1 ≤ n :=374        calc 4 * (qr4 n).1 ≤ 4 * (qr4 n).1 + (qr4 n).2 := Nat.le_add_right _ _375          _ = n := (qr4_spec n).1.symm376      rw [hn] at hn'377      match Nat.lt_or_ge (qr4 n).1 κ with378      | .inl h => exact h379      | .inr h => exact absurd (Nat.lt_of_le_of_lt (Nat.le_trans (Nat.mul_le_mul_left 4 h) h1) hn') (Nat.lt_irrefl _)380    have hinj : ∀ i j, i < p - 1 → j < p - 1 →381        (fun n => (Frame.quarterTurn g κ ^ (qr4 n).2 * (g ^ 4) ^ (qr4 n).1).val) i =382        (fun n => (Frame.quarterTurn g κ ^ (qr4 n).2 * (g ^ 4) ^ (qr4 n).1).val) j → i = j := fun i j hi hj e => by383      obtain ⟨er, es⟩ := inj hk _ _ _ _ (qr4_spec i).2 (hq4 i hi) (qr4_spec j).2 (hq4 j hj) (ext e)384      calc i = 4 * (qr4 i).1 + (qr4 i).2 := (qr4_spec i).1385        _ = 4 * (qr4 j).1 + (qr4 j).2 := by rw [er, es]386        _ = j := (qr4_spec j).1.symm387    have hb : ∀ e, Pigeonhole.mem e (imageList (fun n => (Frame.quarterTurn g κ ^ (qr4 n).2 * (g ^ 4) ^ (qr4 n).1).val) (p - 1)) →388        1 ≤ e ∧ e ≤ p - 1 := fun e he =>389      match mem_imageList he with390      | ⟨n, _, hσ⟩ => ⟨by rw [← hσ]; exact Prime.val_pos (hy n),391          by rw [← hσ]; exact Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (Shell.lt _) (Nat.le_of_eq hp'))⟩392    obtain ⟨n, hn', hσ⟩ := mem_imageList (Pigeonhole.mem_of_nodup_of_length (p - 1) _ (imageList_nodup hinj (Nat.le_refl _))393      hb (imageList_length _ _) x.val (Prime.val_pos hx) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le x.lt (Nat.le_of_eq hp'))))394    exact ⟨(qr4 n).2, (qr4 n).1, (qr4_spec n).2, hq4 n hn', ext hσ⟩395  have solv1 : κ % 2 = 1 → ∃ r s : Nat, r < 4 ∧ s < κ ∧ (3 * κ * r + 4 * s) % (4 * κ) = 1 := fun hk => by396    obtain ⟨r, s, hr, hs, e⟩ := surj hk g F.g_ne_zero397    rw [fold_eq F] at e398    refine ⟨r, s, hr, hs, ?_⟩399    have e2 : g ^ ((3 * κ * r + 4 * s) % (p - 1)) = g ^ 1 := by rw [← F.pow_mod, pow_one]; exact e400    have h1 : 1 < p - 1 := by401      rw [hn]; exact Nat.lt_of_lt_of_le (by decide : 1 < 4 * 1) (Nat.mul_le_mul_left 4 F.cap_pos)402    rw [← hn]; exact F.pow_inj (Nat.mod_lt _ F.n_pos) h1 e2403  have solv2 : (∃ r s : Nat, r < 4 ∧ s < κ ∧ (3 * κ * r + 4 * s) % (4 * κ) = 1) → κ % 2 = 1 := fun ⟨r, s, _, _, e⟩ => by404    match Frame.mod_two_cases κ with405    | .inr h => exact h406    | .inl h =>407      obtain ⟨m, hm⟩ := FRC.Nat.mod_spec 2 (by decide) κ408      rw [h, Nat.add_zero] at hm409      obtain ⟨t, ht⟩ := FRC.Nat.mod_spec (4 * κ) h4κ (3 * κ * r + 4 * s)410      rw [e] at ht411      have hl : 3 * κ * r + 4 * s = 2 * (3 * m * r + 2 * s) := by412        rw [hm, FRC.Nat.mul_left_comm 3 2 m, FRC.Nat.mul_assoc 2, show 4 * s = 2 * (2 * s) by rw [← FRC.Nat.mul_assoc],413          ← Nat.left_distrib]414      have hr' : 4 * κ * t + 1 = 2 * (2 * κ * t) + 1 := by rw [← FRC.Nat.mul_assoc, ← FRC.Nat.mul_assoc]415      have this : (2 * (3 * m * r + 2 * s)) % 2 = (2 * (2 * κ * t) + 1) % 2 := by rw [← hl, ht, hr']416      rw [Frame.two_mul_mod, FRC.Nat.add_mul_mod_self_left _ _ _ (by decide)] at this417      exact absurd this (by decide)418  have hv : κ % 2 = 1 ↔ (p - 1) % 8 ≠ 0 := by419    rw [hn]420    obtain ⟨q, hq'⟩ := FRC.Nat.mod_spec 2 (by decide) κ421    have e8 : 4 * κ = 8 * q + 4 * (κ % 2) :=422      calc 4 * κ = 4 * (2 * q + κ % 2) := by rw [← hq']423        _ = 8 * q + 4 * (κ % 2) := by rw [Nat.left_distrib, ← FRC.Nat.mul_assoc]424    rw [e8, FRC.Nat.add_mul_mod_self_left _ _ _ (by decide)]425    match Frame.mod_two_cases κ with426    | .inl h => rw [h]; exact ⟨fun e => absurd e (by decide), fun e => absurd rfl e⟩427    | .inr h => rw [h]; exact ⟨fun _ => by decide, fun _ => rfl⟩428  exact ⟨hv, ⟨inj, fun hall => match Frame.mod_two_cases κ with429    | .inr h => h430    | .inl h => absurd hall (notinj h)⟩, surj, ⟨solv1, solv2⟩⟩431432/-- 00:C16, the converse — for `κ` even no isomorphism `C_{p−1} ≅ C₄ × C_κ` exists: a map `φ` from the nonzero residues433to the pairs `(r mod 4, s mod κ)` that turns products into sums is never injective, since `2κ` kills `C₄ × C_κ`434(`4 ∣ 2κ`) while `g^{2κ} = −1 ≠ 1`. -/435theorem no_iso {κ : Nat} {g : Shell p} (F : Frame p κ g) (hκ : κ % 2 = 0) (φ : Shell p → Nat × Nat)436    (hφ : ∀ x y : Shell p, x ≠ 0 → y ≠ 0 → φ (x * y) = (((φ x).1 + (φ y).1) % 4, ((φ x).2 + (φ y).2) % κ)) :437    ¬ ∀ x y : Shell p, x ≠ 0 → y ≠ 0 → φ x = φ y → x = y := fun hinj => by438  have hg0 : g ≠ 0 := by have := F.pow_ne_zero 1; rwa [pow_one] at this439  have hpow : ∀ n, φ (g ^ (n + 2)) = (((n + 2) * (φ g).1) % 4, ((n + 2) * (φ g).2) % κ) := fun n => by440    induction n with441    | zero => show φ (g ^ 1 * g) = (((0 + 2) * (φ g).1) % 4, ((0 + 2) * (φ g).2) % κ); rw [pow_one, hφ g g hg0 hg0, Nat.zero_add, Nat.two_mul, Nat.two_mul]442    | succ n ih =>443      show φ (g ^ (n + 2) * g) = (((n + 1 + 2) * (φ g).1) % 4, ((n + 1 + 2) * (φ g).2) % κ)444      rw [hφ _ g (F.pow_ne_zero _) hg0, ih, FRC.Nat.mod_add_mod _ _ _ (Nat.zero_lt_succ 3),445        FRC.Nat.mod_add_mod _ _ _ F.cap_pos, Nat.succ_mul (n + 2) (φ g).1, Nat.succ_mul (n + 2) (φ g).2]446  obtain ⟨t, ht⟩ := FRC.Nat.mod_spec 2 (Nat.zero_lt_succ 1) κ; rw [hκ, Nat.add_zero] at ht447  have c1 : ((2 * κ + 2) * (φ g).1) % 4 = ((0 + 2) * (φ g).1) % 4 := by448    rw [FRC.Nat.add_mul, ht, ← FRC.Nat.mul_assoc 2 2 t, FRC.Nat.mul_assoc (2 * 2) t, Nat.zero_add]449    exact FRC.Nat.add_mul_mod_self_left _ (t * (φ g).1) 4 (Nat.zero_lt_succ 3)450  have c2 : ((2 * κ + 2) * (φ g).2) % κ = ((0 + 2) * (φ g).2) % κ := by451    rw [FRC.Nat.add_mul, Nat.mul_comm 2 κ, FRC.Nat.mul_assoc κ 2, Nat.zero_add]452    exact FRC.Nat.add_mul_mod_self_left _ _ _ F.cap_pos453  have he : φ (g ^ (2 * κ + 2)) = φ (g ^ (0 + 2)) := by rw [hpow, hpow, c1, c2]454  have hg := hinj _ _ (F.pow_ne_zero _) (F.pow_ne_zero _) he; rw [pow_add, Nat.zero_add, F.half_period] at hg455  have hc : g ^ 2 * -1 = g ^ 2 * 1 := by rw [mul_comm, hg, mul_one]456  exact Prime.neg_one_ne_one F.two_lt_p (F.mul_left_cancel (F.pow_ne_zero 2) hc)457458/-- `2^k ∣ 2^a u` with `u` odd forces `k ≤ a`. -/459theorem pow_dvd_odd {a k u : Nat} (hu : u % 2 = 1) : 2 ^ k ∣ 2 ^ a * u → k ≤ a460  | ⟨c, hc⟩ => by461    match Nat.lt_or_ge a k with462    | .inr h => exact h463    | .inl h =>464      obtain ⟨d, hd⟩ : ∃ d, k = a + 1 + d := ⟨k - (a + 1), (FRC.Nat.add_sub_of_le (Nat.succ_le_of_lt h)).symm⟩465      have e : 2 ^ a * u = 2 ^ a * (2 * (2 ^ d * c)) := by466        rw [hc, hd, FRC.Nat.pow_add, Nat.pow_succ, FRC.Nat.mul_assoc (2 ^ a) 2, FRC.Nat.mul_assoc (2 ^ a),467          FRC.Nat.mul_assoc 2]468      rw [Nat.eq_of_mul_eq_mul_left (FRC.Nat.pos_pow_of_pos a (by decide : 0 < 2)) e, Frame.two_mul_mod] at hu469      exact absurd hu (by decide)470471/-- 38:A2 — C16's 2-parts. With `p − 1 = 2^a u` and `Ω − 1 = 2^b w`, `u, w` odd, and `m = min(a, b)`: `2^m` divides both and472`2^{m+1}` not both (the shared 2-part `C_{2^m}`), and `2^m · 2^{b−m} = 2^b` (the shared order times the cover degree is473the Carrier's 2-part); for `Ω − 1 = 4S` the Carrier's 2-part is `8` iff `S ≡ 2 (mod 4)`. -/474theorem two_part :475    (∀ a b u w m : Nat, u % 2 = 1 → w % 2 = 1 → m ≤ a → m ≤ b → (m = a ∨ m = b) →476      2 ^ m ∣ 2 ^ a * u ∧ 2 ^ m ∣ 2 ^ b * w ∧ ¬ (2 ^ (m + 1) ∣ 2 ^ a * u ∧ 2 ^ (m + 1) ∣ 2 ^ b * w) ∧477      2 ^ m * 2 ^ (b - m) = 2 ^ b) ∧478    (∀ S b w : Nat, w % 2 = 1 → 4 * S = 2 ^ b * w → (2 ^ b = 8 ↔ S % 4 = 2)) := by479  have dv : ∀ m a u, m ≤ a → 2 ^ m ∣ 2 ^ a * u := fun m a u h =>480    ⟨2 ^ (a - m) * u, by rw [← FRC.Nat.mul_assoc, ← FRC.Nat.pow_add, FRC.Nat.add_sub_of_le h]⟩481  refine ⟨fun a b u w m hu hw ha hb hm => ⟨dv m a u ha, dv m b w hb, fun ⟨h1, h2⟩ => ?_,482    by rw [← FRC.Nat.pow_add, FRC.Nat.add_sub_of_le hb]⟩, fun S b w hw e => ⟨fun h8 => ?_, fun h2 => ?_⟩⟩483  · match hm with484    | .inl e => rw [e] at h1; exact Nat.not_succ_le_self a (pow_dvd_odd hu h1)485    | .inr e => rw [e] at h2; exact Nat.not_succ_le_self b (pow_dvd_odd hw h2)486  · rw [h8] at e487    have hS : S = 2 * w := Nat.eq_of_mul_eq_mul_left (by decide : 0 < 4) (by rw [e, ← FRC.Nat.mul_assoc])488    obtain ⟨t, ht⟩ := FRC.Nat.mod_spec 2 (by decide) w489    rw [hw] at ht490    rw [hS, ht, Nat.left_distrib, ← FRC.Nat.mul_assoc, FRC.Nat.add_mul_mod_self_left _ _ _ (by decide)]491  · obtain ⟨t, ht⟩ := FRC.Nat.mod_spec 4 (by decide) S492    rw [h2] at ht493    have e' : 2 ^ b * w = 2 ^ 3 * (2 * t + 1) := by494      rw [← e, ht]495      show 4 * (4 * t + 2) = 8 * (2 * t + 1)496      rw [Nat.left_distrib, Nat.left_distrib, ← FRC.Nat.mul_assoc, ← FRC.Nat.mul_assoc]497    have hodd : (2 * t + 1) % 2 = 1 := FRC.Nat.add_mul_mod_self_left 1 t 2 (by decide)498    have hb : b = 3 := Nat.le_antisymm (pow_dvd_odd hodd ⟨w, e'.symm⟩) (pow_dvd_odd hw ⟨2 * t + 1, e'⟩)499    rw [hb]500501/-! ## C25: the horizon is the origin's antipode on the boost torus -/502503section torus504variable {ν : Shell p}505506/-- The boost carrying the origin `[0 : 1]` to the direction `[x : y]` (`q = x/y`): `u = yν + xw`. -/507def dir (ν : Shell p) (x y : Shell p) : Extension.Ext p ν := ⟨ν * y, x⟩508509/-- The torsor map `u ↦ u/ū = u²/N(u)` onto the boost torus `C_{p+1} = {N = 1}`. -/510def ratio (u : Extension.Ext p ν) : Extension.Ext p ν := Extension.Ext.ofShell (inv u.norm) * (u * u)511512theorem ext_mul4 (a b c d : Extension.Ext p ν) : a * b * (c * d) = a * c * (b * d) := by513  rw [Extension.Ext.mul_assoc, ← Extension.Ext.mul_assoc b, Extension.Ext.mul_comm b c, Extension.Ext.mul_assoc c,514    ← Extension.Ext.mul_assoc]515516theorem ratio_ofShell (hp : FRC.Nat.isPrime p) {a : Shell p} (ha : a ≠ 0) :517    ratio (Extension.Ext.ofShell a : Extension.Ext p ν) = 1 := by518  rw [ratio, Extension.Ext.norm_ofShell, Extension.Ext.ofShell_mul, Extension.Ext.ofShell_mul, mul_comm,519    mul_inv hp (Prime.mul_ne_zero hp ha ha)]; rfl520521theorem ratio_mul (u v : Extension.Ext p ν) : ratio (v * u) = ratio v * ratio u := by522  rw [ratio, ratio, ratio, Extension.Ext.norm_mul, inv, inv, inv, mul_pow, ← Extension.Ext.ofShell_mul,523    ext_mul4 v u v u, ext_mul4]524525theorem ratio_scale (hp : FRC.Nat.isPrime p) {c : Shell p} (hc : c ≠ 0) (u : Extension.Ext p ν) :526    ratio (Extension.Ext.ofShell c * u) = ratio u := by527  rw [ratio_mul, ratio_ofShell hp hc, Extension.Ext.one_mul]528529theorem norm_ratio (hp : FRC.Nat.isPrime p) {u : Extension.Ext p ν} (hu : u.norm ≠ 0) : (ratio u).norm = 1 := by530  rw [ratio, Extension.Ext.norm_scale, Extension.Ext.norm_mul, mul_mul_mul_comm, mul_comm (inv _), mul_inv hp hu, one_mul]531532theorem nonsquare_ne_zero {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) : ν ≠ 0 :=533  fun e => hν ⟨0, by rw [e, mul_zero]⟩534535/-- **C25 (p00139), the horizon is the origin's antipode on the boost torus.** On a prime `p = 4κ + 1` with `ν` a536nonsquare and `𝔽_{p²} = 𝔽_p[w]/(w² − ν)`: a direction `[x : y] ≠ 0` has the boost `u = yν + xw` of nonzero norm, and537`v = a + bw` moves it by `q ↦ (aq + νb)/(bq + a)`; the torsor map `u ↦ u/ū` lands on `C_{p+1}`, is constant on the538classes `𝔽_p^× u` and equivariant, and is a bijection from the directions onto `C_{p+1}`; it sends the origin `[0 : 1]`539to `1` and the horizon `[1 : 0]` to `−1`, the one element of order two, and `𝔽_p^× ∩ C_{p+1} = {±1}`; the one boost540of order two is the class of `w`, `q ↦ ν/q`, which swaps the origin and the horizon; and `2s = 0` forces `s = 0`, the541seam `2κ + (2κ + 1) = 0`: `2⁻¹ = 2κ + 1 = −2κ`. -/542theorem horizon_antipode (hp : FRC.Nat.isPrime p) {κ : Nat} (hκ : p = 4 * κ + 1) (hν : ¬ ∃ y : Shell p, y * y = ν) :543    (∀ x y : Shell p, (x ≠ 0 ∨ y ≠ 0) → (dir ν x y).norm ≠ 0) ∧544    (∀ (v : Extension.Ext p ν) (x y : Shell p), v * dir ν x y = dir ν (v.re * x + ν * (v.im * y)) (v.re * y + v.im * x)) ∧545    (∀ u : Extension.Ext p ν, u.norm ≠ 0 → (ratio u).norm = 1) ∧546    (∀ (c : Shell p) (u : Extension.Ext p ν), c ≠ 0 → ratio (Extension.Ext.ofShell c * u) = ratio u) ∧547    (∀ u v : Extension.Ext p ν, ratio (v * u) = ratio v * ratio u) ∧548    (∀ x y x' y' : Shell p, (x ≠ 0 ∨ y ≠ 0) → (x' ≠ 0 ∨ y' ≠ 0) →549      (ratio (dir ν x y) = ratio (dir ν x' y') ↔ x * y' = x' * y)) ∧550    (∀ z : Extension.Ext p ν, z.norm = 1 → ∃ x y : Shell p, (x ≠ 0 ∨ y ≠ 0) ∧ ratio (dir ν x y) = z) ∧551    ratio (dir ν 0 1) = 1 ∧ ratio (dir ν 1 0) = -1 ∧552    (∀ z : Extension.Ext p ν, z.norm = 1 → z * z = 1 → z = 1 ∨ z = -1) ∧553    (∀ z : Extension.Ext p ν, z.im = 0 → (z.norm = 1 ↔ z = 1 ∨ z = -1)) ∧554    (∀ v : Extension.Ext p ν, (v * v).im = 0 → v.im ≠ 0 → v.re = 0) ∧555    (∀ x y : Shell p, Extension.Ext.w * dir ν x y = dir ν (ν * y) x) ∧556    (∀ s : Shell p, 2 * s = 0 → s = 0) ∧ (2 : Shell p) * ofNat (2 * κ + 1) = 1 ∧557      ofNat (2 * κ) + ofNat (2 * κ + 1) = (0 : Shell p) := by558  have hν0 := nonsquare_ne_zero hν559  have h2 : (2 : Shell p) ≠ 0 := fun e => by560    have := Prime.two_mul_chart_half hκ; rw [e, zero_mul] at this; exact Prime.one_ne_zero hp this.symm561  have hsq1 : ∀ c : Shell p, c * c = 1 ↔ c = 1 ∨ c = -1 := fun c =>562    ⟨Prime.sq_eq_one hp, fun h => match h with563      | .inl e => by rw [e, mul_one]564      | .inr e => by rw [e, neg_mul_neg, mul_one]⟩565  -- the norm of a direction's boost, `ν (ν y² − x²)`566  have hnd : ∀ x y : Shell p, (dir ν x y).norm = ν * (ν * (y * y) + -(x * x)) := fun x y =>567    Shell.Frame.RE.sound (Shell.Frame.look [ν, x, y])568      (.add (.mul (.mul (.var 0) (.var 2)) (.mul (.var 0) (.var 2))) (.neg (.mul (.var 0) (.mul (.var 1) (.var 1)))))569      (.mul (.var 0) (.add (.mul (.var 0) (.mul (.var 2) (.var 2))) (.neg (.mul (.var 1) (.var 1))))) (by decide +kernel)570  have hne : ∀ x y : Shell p, (x ≠ 0 ∨ y ≠ 0) → (dir ν x y).norm ≠ 0 := fun x y hxy h0 => by571    rw [hnd] at h0572    have e := Prime.eq_of_sub_eq_zero ((Prime.mul_eq_zero hp h0).resolve_left hν0)573    match Shell.instDecidableEq y 0 with574    | .isFalse hy =>575      exact hν ⟨x * inv y, by rw [mul_mul_mul_comm, ← e, mul_assoc, ← mul_mul_mul_comm, mul_inv hp hy, mul_one, mul_one]⟩576    | .isTrue hy =>577      rw [hy, mul_zero, mul_zero] at e578      have hx : x = 0 := match Prime.mul_eq_zero hp e.symm with | .inl a => a | .inr a => a579      exact match hxy with | .inl a => a hx | .inr a => a hy580  have hact : ∀ (v : Extension.Ext p ν) (x y : Shell p),581      v * dir ν x y = dir ν (v.re * x + ν * (v.im * y)) (v.re * y + v.im * x) := fun v x y =>582    Extension.Ext.ext583      (Shell.Frame.RE.sound (Shell.Frame.look [ν, v.re, v.im, x, y])584        (.add (.mul (.var 1) (.mul (.var 0) (.var 4))) (.mul (.var 0) (.mul (.var 2) (.var 3))))585        (.mul (.var 0) (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3)))) (by decide +kernel))586      (Shell.Frame.RE.sound (Shell.Frame.look [ν, v.re, v.im, x, y])587        (.add (.mul (.var 1) (.var 3)) (.mul (.var 2) (.mul (.var 0) (.var 4))))588        (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4)))) (by decide +kernel))589  -- the horizon's boost is `w`, of norm `−ν`590  have hw : dir ν 1 0 = Extension.Ext.w := Extension.Ext.ext (mul_zero ν) rfl591  have hm1 : ratio (dir ν 1 0) = -1 := by592    rw [hw, ratio, Extension.Ext.w_sq, Extension.Ext.ofShell_mul]593    have hn : (Extension.Ext.w : Extension.Ext p ν).norm = -ν := by594      show 0 * 0 + -(ν * (1 * 1)) = -ν; rw [zero_mul, zero_add, mul_one, mul_one]595    rw [hn]596    have hn0 : -ν ≠ 0 := fun h => hν0 (by rw [← neg_neg ν, h, neg_zero])597    have e : inv (-ν) * ν = -1 :=598      calc inv (-ν) * ν = -(inv (-ν) * -ν) := by rw [← mul_neg, neg_neg]599        _ = -1 := by rw [mul_comm, mul_inv hp hn0]600    rw [e]; exact Extension.Ext.ext rfl (neg_zero).symm601  -- `a² + νb² = a² − νb²` forces `b = 0`602  have hb0 : ∀ a b : Shell p, a * a + ν * (b * b) = a * a + -(ν * (b * b)) → b = 0 := fun a b e => by603    have key : a * a + ν * (b * b) + -(a * a + -(ν * (b * b))) = (1 + 1) * (ν * (b * b)) :=604      Shell.Frame.RE.sound (Shell.Frame.look [ν, a, b])605        (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.neg (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2)))))))606        (.mul (.add .one .one) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (by decide +kernel)607    rw [e, add_neg] at key608    have e3 := (Prime.mul_eq_zero hp key.symm).resolve_left (by rw [← Prime.two_eq]; exact h2)609    have e4 := (Prime.mul_eq_zero hp e3).resolve_left hν0610    exact match Prime.mul_eq_zero hp e4 with | .inl a => a | .inr a => a611  -- a norm-one element of order two is `±1`612  have hord2 : ∀ z : Extension.Ext p ν, z.norm = 1 → z * z = 1 → z = 1 ∨ z = -1 := fun z hz hzz => by613    have hre : z.re * z.re + ν * (z.im * z.im) = 1 := Extension.Ext.re_congr hzz614    have hb := hb0 z.re z.im (hre.trans hz.symm)615    have ha : z.re * z.re = 1 := by rw [hb, mul_zero, mul_zero, add_zero] at hre; exact hre616    exact match (hsq1 z.re).1 ha with617      | .inl a => .inl (Extension.Ext.ext a hb)618      | .inr a => .inr (Extension.Ext.ext a (by rw [hb]; exact (neg_zero).symm))619  -- the torsor map is injective on directions620  have hinj : ∀ x y x' y' : Shell p, (x ≠ 0 ∨ y ≠ 0) → (x' ≠ 0 ∨ y' ≠ 0) →621      (ratio (dir ν x y) = ratio (dir ν x' y') ↔ x * y' = x' * y) := fun x y x' y' hxy hxy' => by622    constructor623    · intro e624      have hu' := hne x' y' hxy'625      have hnc : (Extension.Ext.conj (dir ν x' y')).norm = (dir ν x' y').norm := by626        show (ν * y') * (ν * y') + -(ν * (-x' * -x')) = (ν * y') * (ν * y') + -(ν * (x' * x')); rw [neg_mul_neg]627      have hc : ratio (Extension.Ext.conj (dir ν x' y')) * ratio (dir ν x' y') = 1 := by628        rw [← ratio_mul, Extension.Ext.mul_comm, Extension.Ext.mul_conj]; exact ratio_ofShell hp hu'629      have ht : ratio (dir ν x y * Extension.Ext.conj (dir ν x' y')) = 1 := by630        rw [ratio_mul, e, Extension.Ext.mul_comm]; exact hc631      have hnt : (dir ν x y * Extension.Ext.conj (dir ν x' y')).norm ≠ 0 := by632        rw [Extension.Ext.norm_mul, hnc]; exact Prime.mul_ne_zero hp (hne x y hxy) hu'633      generalize hT : dir ν x y * Extension.Ext.conj (dir ν x' y') = T at ht hnt634      have h1 : inv T.norm * (T * T).re = 1 := by635        have := Extension.Ext.re_congr ht; rw [ratio, Extension.Ext.ofShell_mul_eq] at this; exact this636      have h2' : (T * T).re = T.norm := by637        rw [← one_mul (T * T).re, ← mul_inv hp hnt, mul_assoc, h1, mul_one]638      have hTi : T.im = 0 := hb0 T.re T.im h2'639      have hTi' : T.im = ν * (x * y' + -(x' * y)) := by640        rw [← hT]641        exact Shell.Frame.RE.sound (Shell.Frame.look [ν, x, y, x', y'])642          (.add (.mul (.mul (.var 0) (.var 2)) (.neg (.var 3))) (.mul (.var 1) (.mul (.var 0) (.var 4))))643          (.mul (.var 0) (.add (.mul (.var 1) (.var 4)) (.neg (.mul (.var 3) (.var 2))))) (by decide +kernel)644      rw [hTi'] at hTi645      exact Prime.eq_of_sub_eq_zero ((Prime.mul_eq_zero hp hTi).resolve_left hν0)646    · intro e647      match Shell.instDecidableEq y 0 with648      | .isFalse hy =>649        have hy' : y' ≠ 0 := fun h0 => by650          rw [h0, mul_zero] at e651          exact match hxy' with652            | .inl a => a ((Prime.mul_eq_zero hp e.symm).resolve_right hy)653            | .inr a => a h0654        have hd : dir ν x' y' = Extension.Ext.ofShell (y' * inv y) * dir ν x y := by655          rw [Extension.Ext.ofShell_mul_eq]656          refine Extension.Ext.ext ?_ ?_657          · show ν * y' = y' * inv y * (ν * y)658            rw [mul_assoc, mul_left_comm (inv y), mul_comm (inv y), mul_inv hp hy, mul_one, mul_comm]659          · show x' = y' * inv y * x660            calc x' = x' * (y * inv y) := by rw [mul_inv hp hy, mul_one]661              _ = x * y' * inv y := by rw [e, mul_assoc]662              _ = y' * inv y * x := by rw [mul_comm x y', mul_assoc, mul_comm x (inv y), ← mul_assoc]663        rw [hd, ratio_scale hp (Prime.mul_ne_zero hp hy' (inv_ne_zero hp hy))]664      | .isTrue hy =>665        subst hy666        have hx : x ≠ 0 := match hxy with | .inl a => a | .inr a => absurd rfl a667        have hy' : y' = 0 := by668          rw [mul_zero] at e; exact (Prime.mul_eq_zero hp e).resolve_left hx669        subst hy'670        have hx' : x' ≠ 0 := match hxy' with | .inl a => a | .inr a => absurd rfl a671        have hd : dir ν x' 0 = Extension.Ext.ofShell (x' * inv x) * dir ν x 0 := by672          rw [Extension.Ext.ofShell_mul_eq]673          refine Extension.Ext.ext ?_ ?_674          · show ν * 0 = x' * inv x * (ν * 0); rw [mul_zero, mul_zero]675          · show x' = x' * inv x * x; rw [mul_assoc, mul_comm (inv x), mul_inv hp hx, mul_one]676        rw [hd, ratio_scale hp (Prime.mul_ne_zero hp hx' (inv_ne_zero hp hx))]677  -- and onto `C_{p+1}` (Hilbert 90: `z = (1 + z)/(1 + z̄)` for `z ≠ −1`)678  have hsurj : ∀ z : Extension.Ext p ν, z.norm = 1 → ∃ x y : Shell p, (x ≠ 0 ∨ y ≠ 0) ∧ ratio (dir ν x y) = z :=679    fun z hz => by680    have hzn : z.re * z.re + -(ν * (z.im * z.im)) = 1 := hz681    match Shell.instDecidableEq (1 + z.re) 0 with682    | .isTrue h1 =>683      refine ⟨1, 0, .inl (Prime.one_ne_zero hp), ?_⟩684      have hre : z.re = -1 := (neg_eq_of_add_eq_zero h1).symm685      rw [hre, neg_mul_neg, mul_one] at hzn686      have h0 : -(ν * (z.im * z.im)) = 0 :=687        add_right_cancel (by rw [add_comm, hzn, zero_add] : -(ν * (z.im * z.im)) + 1 = 0 + 1)688      have hn0 : ν * (z.im * z.im) = 0 := by rw [← neg_neg (ν * (z.im * z.im)), h0, neg_zero]689      have him : z.im = 0 :=690        match Prime.mul_eq_zero hp ((Prime.mul_eq_zero hp hn0).resolve_left hν0) with | .inl a => a | .inr a => a691      rw [hm1]692      exact Extension.Ext.ext hre.symm (by show -(0 : Shell p) = z.im; rw [him, neg_zero])693    | .isFalse h1 =>694      refine ⟨ν * z.im, 1 + z.re, .inr h1, ?_⟩695      have hd : dir ν (ν * z.im) (1 + z.re) = Extension.Ext.ofShell ν * (⟨1 + z.re, z.im⟩ : Extension.Ext p ν) := by696        rw [Extension.Ext.ofShell_mul_eq]; rfl697      rw [hd, ratio_scale hp hν0]698      have hbb : ν * (z.im * z.im) = z.re * z.re + -1 := by699        have e : ν * (z.im * z.im) = z.re * z.re + -(z.re * z.re + -(ν * (z.im * z.im))) :=700          Shell.Frame.RE.sound (Shell.Frame.look [z.re, ν * (z.im * z.im)]) (.var 1)701            (.add (.mul (.var 0) (.var 0)) (.neg (.add (.mul (.var 0) (.var 0)) (.neg (.var 1))))) (by decide +kernel)702        rw [e, hzn]703      have hM : (⟨1 + z.re, z.im⟩ : Extension.Ext p ν).norm = (1 + 1) * (1 + z.re) := by704        show (1 + z.re) * (1 + z.re) + -(ν * (z.im * z.im)) = (1 + 1) * (1 + z.re)705        rw [hbb]706        exact Shell.Frame.RE.sound (Shell.Frame.look [z.re])707          (.add (.mul (.add .one (.var 0)) (.add .one (.var 0))) (.neg (.add (.mul (.var 0) (.var 0)) (.neg .one))))708          (.mul (.add .one .one) (.add .one (.var 0))) (by decide +kernel)709      have hsq : (⟨1 + z.re, z.im⟩ : Extension.Ext p ν) * ⟨1 + z.re, z.im⟩ =710          Extension.Ext.ofShell ((1 + 1) * (1 + z.re)) * z := by711        rw [Extension.Ext.ofShell_mul_eq]712        refine Extension.Ext.ext ?_ ?_713        · show (1 + z.re) * (1 + z.re) + ν * (z.im * z.im) = (1 + 1) * (1 + z.re) * z.re714          rw [hbb]715          exact Shell.Frame.RE.sound (Shell.Frame.look [z.re])716            (.add (.mul (.add .one (.var 0)) (.add .one (.var 0))) (.add (.mul (.var 0) (.var 0)) (.neg .one)))717            (.mul (.mul (.add .one .one) (.add .one (.var 0))) (.var 0)) (by decide +kernel)718        · exact Shell.Frame.RE.sound (Shell.Frame.look [z.re, z.im])719            (.add (.mul (.add .one (.var 0)) (.var 1)) (.mul (.var 1) (.add .one (.var 0))))720            (.mul (.mul (.add .one .one) (.add .one (.var 0))) (.var 1)) (by decide +kernel)721      have hM0 : (1 + 1) * (1 + z.re) ≠ 0 := Prime.mul_ne_zero hp (by rw [← Prime.two_eq]; exact h2) h1722      rw [ratio, hM, hsq, ← Extension.Ext.mul_assoc, Extension.Ext.ofShell_mul, mul_comm, mul_inv hp hM0]723      exact Extension.Ext.one_mul z724  have h01 : ratio (dir ν 0 1) = 1 := by725    have : dir ν 0 1 = Extension.Ext.ofShell (ν * 1) := rfl726    rw [this]; exact ratio_ofShell hp (by rw [mul_one]; exact hν0)727  have hinv : ∀ v : Extension.Ext p ν, (v * v).im = 0 → v.im ≠ 0 → v.re = 0 := fun v e hv => by728    have key : (v * v).im = (1 + 1) * (v.re * v.im) :=729      Shell.Frame.RE.sound (Shell.Frame.look [v.re, v.im])730        (.add (.mul (.var 0) (.var 1)) (.mul (.var 1) (.var 0))) (.mul (.add .one .one) (.mul (.var 0) (.var 1)))731        (by decide +kernel)732    rw [key] at e733    exact (Prime.mul_eq_zero hp ((Prime.mul_eq_zero hp e).resolve_left (by rw [← Prime.two_eq]; exact h2))).resolve_right hv734  have hwact : ∀ x y : Shell p, Extension.Ext.w * dir ν x y = dir ν (ν * y) x := fun x y => by735    rw [hact]736    show dir ν (0 * x + ν * (1 * y)) (0 * y + 1 * x) = dir ν (ν * y) x737    rw [zero_mul, zero_add, one_mul, zero_mul, zero_add, one_mul]738  have hrat : ∀ z : Extension.Ext p ν, z.im = 0 → (z.norm = 1 ↔ z = 1 ∨ z = -1) := fun z hz => by739    have hn : z.norm = z.re * z.re := by740      show z.re * z.re + -(ν * (z.im * z.im)) = z.re * z.re741      rw [hz, zero_mul, mul_zero, neg_zero, add_zero]742    rw [hn]743    constructor744    · intro h745      match (hsq1 z.re).1 h with746      | .inl e => exact .inl (Extension.Ext.ext e hz)747      | .inr e => exact .inr (Extension.Ext.ext e (by show z.im = -(0 : Shell p); rw [hz, neg_zero]))748    · intro h749      match h with750      | .inl e => rw [e]; exact mul_one (1 : Shell p)751      | .inr e => rw [e]; show (-1 : Shell p) * -1 = 1; rw [neg_mul_neg, mul_one]752  have hseam : (ofNat (2 * κ) : Shell p) + ofNat (2 * κ + 1) = 0 := by753    rw [show (ofNat (2 * κ) + ofNat (2 * κ + 1) : Shell p) = ofNat (2 * κ + (2 * κ + 1)) from754      ext (FRC.Nat.add_mod _ _ _ Pos.pos).symm, show 2 * κ + (2 * κ + 1) = p by755      rw [hκ, ← Nat.add_assoc, ← Nat.two_mul, ← FRC.Nat.mul_assoc]]756    exact Prime.ofNat_self757  exact ⟨hne, hact, fun u hu => norm_ratio hp hu, fun c u hc => ratio_scale hp hc u, fun u v => ratio_mul u v, hinj,758    hsurj, h01, hm1, hord2, hrat, hinv, hwact,759    fun s hs => (Prime.mul_eq_zero hp hs).resolve_left h2, Prime.two_mul_chart_half hκ, hseam⟩760761/-- 00:C25, 22:A2, 22:P4 — the horizon is `ζ^{(p+1)/2}` for every generator `ζ` of the torus: a norm-one `ζ` of order exactly `p + 1`762has `ζ^{2κ+1} = −1`, the torus's one element of order two. -/763theorem horizon_generator (hp : FRC.Nat.isPrime p) {κ : Nat} (hκ : p = 4 * κ + 1) (hν : ¬ ∃ y : Shell p, y * y = ν)764    (ζ : Extension.Ext p ν) (hn : ζ.norm = 1) (hζ : ζ ^ (p + 1) = 1)765    (hmin : ∀ l, 0 < l → l < p + 1 → ζ ^ l ≠ 1) : ζ ^ (2 * κ + 1) = -1 := by766  have hh : (2 * κ + 1) + (2 * κ + 1) = p + 1 := by767    rw [hκ, show 4 * κ = 2 * κ + 2 * κ from FRC.Nat.add_mul 2 2 κ]; exact congrArg Nat.succ (Nat.succ_add _ _)768  have hsq : ζ ^ (2 * κ + 1) * ζ ^ (2 * κ + 1) = 1 := by rw [← Extension.Ext.pow_add, hh, hζ]769  have hnorm : (ζ ^ (2 * κ + 1)).norm = 1 := by rw [Extension.Ext.norm_pow, hn, one_pow]770  have hlt : 2 * κ + 1 < p + 1 := by rw [← hh]; exact Nat.lt_add_of_pos_right (Nat.zero_lt_succ _)771  match (horizon_antipode hp hκ hν).2.2.2.2.2.2.2.2.2.1 _ hnorm hsq with772  | .inl e => exact absurd e (hmin _ (Nat.zero_lt_succ _) hlt)773  | .inr e => exact e774775/-- 00:C25 — `u_P` is the unique boost carrying the origin to `P`: a boost `v` with `v · dir(0, 1) = c · dir(x, y)` is776`(c/ν) · dir(x, y)`, so it is `dir(x, y)` up to a scalar, which acts trivially on `ℙ¹` and leaves the ratio unchanged. -/777theorem boost_unique (hp : FRC.Nat.isPrime p) (hν : ¬ ∃ y : Shell p, y * y = ν) (v : Extension.Ext p ν) (c x y : Shell p)778    (h : v * dir ν 0 1 = Extension.Ext.ofShell c * dir ν x y) :779    v = Extension.Ext.ofShell (c * inv ν) * dir ν x y := by780  have h0 : dir ν 0 1 = Extension.Ext.ofShell ν := Extension.Ext.ext (mul_one ν) rfl781  have hi : (Extension.Ext.ofShell (inv ν) : Extension.Ext p ν) * Extension.Ext.ofShell ν = 1 := by782    rw [Extension.Ext.ofShell_mul, mul_comm, mul_inv hp (nonsquare_ne_zero hν)]; rfl783  calc v = Extension.Ext.ofShell (inv ν) * Extension.Ext.ofShell ν * v := by rw [hi, Extension.Ext.one_mul]784    _ = Extension.Ext.ofShell (inv ν) * (v * dir ν 0 1) := by rw [h0, Extension.Ext.mul_assoc, Extension.Ext.mul_comm _ v]785    _ = Extension.Ext.ofShell (c * inv ν) * dir ν x y := by rw [h, ← Extension.Ext.mul_assoc, Extension.Ext.ofShell_mul, mul_comm (inv ν) c]786787end torus788789end FRC.Subject790