Theme/Causal.lean — FrcCore

1import FrcCore.Parity2import FrcCore.Theme.Extension3import FrcCore.Theme.Gravity45/-!6# FrcCore.Theme.Causal — the counts of the Lorentzian form on every shell (3-causality, 7 November 2026)78The gravity theme's counting (`count`, `nsum`, their invariance under a bijection of the residues, and the plane conic9`y² + z² = c` with `p − 1` points for `c ≠ 0` and `2p − 1` for `c = 0`) applied to the diagonal form10`Q_ν = −ν t² + x² + y² + z²` of 3-causality, on every frame `(τ; 0, 1, g)` with `p = 4κ + 1`:1112* the plane form `x² − ν t²` takes the value `0` once when `ν` is a nonsquare (`plane_zero_aniso`) and `2p − 1` times13  when `ν = w²` (`plane_zero_split`); over all values it takes `p²` points (`plane_total`);14* the count of `Q_ν = a` is `p²(p − 1) + p` times the plane's count at `a` (`form_count`), so the null cone has15  `p³ − p² + p` points for a nonsquare `ν` and `p³ + p² − p` for a square (`null_elliptic`, `null_hyperbolic`);16* for the drive `ν = g` the plane takes every nonzero value equally often, by the scaling `(t, x) ↦ (wt, wx)` and the17  swap `(t, x) ↦ (x, gt)`, which multiplies the form by `−g`: hence `p + 1` times (`plane_nonzero`), the norm-one18  cycle has `p + 1` elements, and every nonzero value of `Q_g` — the time sphere `Q_g = −g` among them — is taken19  `p³ + p` times (`sphere_drive`).2021The counts are natural numbers and no numeral is formed. No axioms.22-/2324namespace FRC.Causal2526open FRC.Shell FRC.Shell.Frame FRC.Grav2728variable {p : Nat} [Pos p]2930/-! ## Sums over the residues -/3132/-- A sum over the residues is invariant under a bijection of the residues. -/33theorem nsum_bij (F : Shell p → Nat) (f h : Shell p → Shell p) (hhf : ∀ x, h (f x) = x) :34    nsum (fun t => F (f (ofNat t))) p = nsum (fun t => F (ofNat t)) p := by35  have e : ∀ t, t < p → (fun t => F (f (ofNat t))) t = (fun y => F (ofNat y)) ((f (ofNat t)).val) := fun t _ => by36    show F (f (ofNat t)) = F (ofNat (f (ofNat t)).val)37    rw [ofNat_val]38  rw [nsum_congr p e]39  exact nsum_perm (fun y => F (ofNat y)) (fun t => (f (ofNat t)).val) p (fun t _ => (f (ofNat t)).lt)40    (fun i j hi hj hij => ofNat_inj hi hj (by rw [← hhf (ofNat i), ← hhf (ofNat j), ext hij]))4142/-- An indicator summed over the residues is a count. -/43theorem nsum_ind (P : Shell p → Prop) [DecidablePred P] :44    nsum (fun x => if P (ofNat x) then 1 else 0) p = count P :=45  (natCount_eq_nsum (fun x => P (ofNat x)) p).symm4647/-- A sum over the residues splits into the term at `0` and the terms at the nonzero residues. -/48theorem nsum_split (F : Shell p → Nat) :49    nsum (fun t => F (ofNat t)) p = F 0 + nsum (fun l => F (ofNat (l + 1))) (p - 1) := by50  have hp : (p - 1) + 1 = p := FRC.Nat.sub_add_cancel Pos.pos51  calc nsum (fun t => F (ofNat t)) p = nsum (fun t => F (ofNat t)) ((p - 1) + 1) := by rw [hp]52    _ = F (ofNat 0) + nsum (fun l => F (ofNat (l + 1))) (p - 1) := nsum_succ' _ _53    _ = F 0 + nsum (fun l => F (ofNat (l + 1))) (p - 1) := rfl5455/-- The nonzero residues `l + 1`, `l < p − 1`, are nonzero. -/56theorem succ_ne_zero' {l : Nat} (hl : l < p - 1) : (ofNat (l + 1) : Shell p) ≠ 0 := fun h => by57  have hlt : l + 1 < p := by58    have h1 : l + 1 < (p - 1) + 1 := Nat.succ_lt_succ hl59    rw [FRC.Nat.sub_add_cancel Pos.pos] at h160    exact h161  exact Nat.succ_ne_zero l (ofNat_inj hlt Pos.pos h)6263/-! ## The plane form `x² − ν t²` -/6465/-- `#{(t, x) : x² − ν t² = c}`. -/66def planeCount (ν c : Shell p) : Nat :=67  nsum (fun t => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = c then 1 else 0) p) p6869/-- The plane takes `p²` points over all its values. -/70theorem plane_total (ν : Shell p) : nsum (fun c => planeCount ν (ofNat c)) p = p * p := by71  have h1 : ∀ t, t < p →72      nsum (fun c => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = (ofNat c : Shell p) then 1 else 0) p) p = p := by73    intro t _74    have h2 : ∀ x, x < p →75        nsum (fun c => if Q2 ν (ofNat t) (ofNat x) = (ofNat c : Shell p) then 1 else 0) p = 1 := by76      intro x _77      exact (nsum_congr p (fun c _ => ite_iff ⟨Eq.symm, Eq.symm⟩ 1 0)).trans78        ((nsum_ind (fun c => c = Q2 ν (ofNat t) (ofNat x))).trans (count_eq _))79    calc nsum (fun c => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = (ofNat c : Shell p) then 1 else 0) p) p80        = nsum (fun x => nsum (fun c => if Q2 ν (ofNat t) (ofNat x) = (ofNat c : Shell p) then 1 else 0) p) p :=81          nsum_comm (fun c x => if Q2 ν (ofNat t) (ofNat x) = (ofNat c : Shell p) then 1 else 0) p p82      _ = nsum (fun _ => 1) p := nsum_congr p h283      _ = p := by rw [nsum_const, Nat.mul_one]84  calc nsum (fun c => planeCount ν (ofNat c)) p85      = nsum (fun t => nsum (fun c => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = (ofNat c : Shell p) then 1 else 0) p) p) p :=86        nsum_comm (fun c t => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = (ofNat c : Shell p) then 1 else 0) p) p p87    _ = nsum (fun _ => p) p := nsum_congr p h188    _ = p * p := nsum_const p p8990section frame91variable {κ : Nat} {g : Shell p}9293/-- `x² = 0` only at `x = 0`. -/94theorem sq_eq_zero (F : Frame p κ g) {x : Shell p} : x * x = 0 ↔ x = 0 :=95  ⟨fun h => match F.mul_eq_zero h with | .inl h' => h' | .inr h' => h', fun h => by rw [h, mul_zero]⟩9697/-- The row `t = 0` of the plane at `0`: one point, `x = 0`. -/98theorem row_zero (F : Frame p κ g) (ν : Shell p) :99    nsum (fun x => if Q2 ν 0 (ofNat x) = 0 then 1 else 0) p = 1 := by100  have e : ∀ x : Shell p, Q2 ν 0 x = 0 ↔ x = 0 := fun x => by101    unfold Q2102    rw [mul_zero, mul_zero, neg_zero, add_zero]103    exact sq_eq_zero F104  exact (nsum_congr p (fun x _ => ite_iff (e (ofNat x)) 1 0)).trans105    ((nsum_ind (fun x : Shell p => x = 0)).trans (count_eq _))106107/-- 3:B4 — for a nonsquare `ν` the plane `x² − ν t²` vanishes only at the origin: one point. -/108theorem plane_zero_aniso (F : Frame p κ g) {ν : Shell p} (hν : ¬IsSquare ν) : planeCount ν 0 = 1 := by109  unfold planeCount110  rw [nsum_split (fun t => nsum (fun x => if Q2 ν t (ofNat x) = 0 then 1 else 0) p)]111  have hrow : ∀ l, l < p - 1 → nsum (fun x => if Q2 ν (ofNat (l + 1)) (ofNat x) = 0 then 1 else 0) p = 0 := by112    intro l hl113    have e : ∀ x, x < p → (if Q2 ν (ofNat (l + 1)) (ofNat x) = (0 : Shell p) then 1 else 0) = 0 := fun x _ =>114      ite_eq_right (fun h => by115        have h' : (ofNat x : Shell p) * ofNat x = ν * (ofNat (l + 1) * ofNat (l + 1)) := by116          unfold Q2 at h117          calc (ofNat x : Shell p) * ofNat x118              = ofNat x * ofNat x + -(ν * (ofNat (l + 1) * ofNat (l + 1))) + ν * (ofNat (l + 1) * ofNat (l + 1)) := by119                rw [add_assoc, neg_add, add_zero]120            _ = ν * (ofNat (l + 1) * ofNat (l + 1)) := by rw [h, zero_add]121        exact succ_ne_zero' hl (aniso_tx F hν h').1)122    rw [nsum_congr p e, nsum_zero]123  show nsum (fun x => if Q2 ν 0 (ofNat x) = 0 then 1 else 0) p + _ = 1124  rw [row_zero F ν, nsum_congr (p - 1) hrow, nsum_zero]125126/-- 3:B4 — for a square `ν = w²`, `w ≠ 0`, the plane `x² − w² t²` vanishes on `2p − 1` points: the two lines127`x = ±wt`. -/128theorem plane_zero_split (F : Frame p κ g) {w : Shell p} (hw : w ≠ 0) : planeCount (w * w) 0 + 1 = 2 * p := by129  unfold planeCount130  rw [nsum_split (fun t => nsum (fun x => if Q2 (w * w) t (ofNat x) = 0 then 1 else 0) p)]131  have hrow : ∀ l, l < p - 1 → nsum (fun x => if Q2 (w * w) (ofNat (l + 1)) (ofNat x) = 0 then 1 else 0) p = 2 := by132    intro l hl133    have hb : w * ofNat (l + 1) ≠ 0 := F.mul_ne_zero hw (succ_ne_zero' hl)134    have e : ∀ x : Shell p, Q2 (w * w) (ofNat (l + 1)) x = 0 ↔ x * x = (w * ofNat (l + 1)) * (w * ofNat (l + 1)) :=135      fun x => by136        unfold Q2137        rw [sq_mul w (ofNat (l + 1)), mul_assoc]138        exact ⟨fun h => by139            calc x * x = x * x + -(w * (w * (ofNat (l + 1) * ofNat (l + 1)))) + w * (w * (ofNat (l + 1) * ofNat (l + 1))) := by140                  rw [add_assoc, neg_add, add_zero]141              _ = w * (w * (ofNat (l + 1) * ofNat (l + 1))) := by rw [h, zero_add],142          fun h => by rw [h, add_neg]⟩143    exact (nsum_congr p (fun x _ => ite_iff (e (ofNat x)) 1 0)).trans144      ((nsum_ind (fun x : Shell p => x * x = (w * ofNat (l + 1)) * (w * ofNat (l + 1)))).trans (count_sq F hb))145  show nsum (fun x => if Q2 (w * w) 0 (ofNat x) = 0 then 1 else 0) p + _ + 1 = 2 * p146  rw [row_zero F (w * w), nsum_congr (p - 1) hrow, nsum_const]147  have hp : (p - 1) + 1 = p := FRC.Nat.sub_add_cancel Pos.pos148  calc 1 + (p - 1) * 2 + 1 = ((p - 1) + 1) * 2 := by rw [Nat.succ_mul, Nat.add_comm 1, Nat.add_assoc]149    _ = 2 * p := by rw [hp, Nat.mul_comm]150151/-! ## The four-dimensional form -/152153/-- `#{(t, x, y, z) : x² − ν t² + y² + z² = a}`. -/154def formCount (ν a : Shell p) : Nat :=155  nsum (fun t => nsum (fun x => nsum (fun y => count (fun z =>156    ofNat y * ofNat y + z * z = a + -(Q2 ν (ofNat t) (ofNat x)))) p) p) p157158/-- The count of `Q_ν = a` is `p²(p − 1) + p` times the plane's count at `a`. -/159theorem form_count (F : Frame p κ g) (ν a : Shell p) : formCount ν a = p * p * (p - 1) + p * planeCount ν a := by160  unfold formCount planeCount161  have hx : ∀ t x, nsum (fun y => count (fun z => ofNat y * ofNat y + z * z = a + -(Q2 ν (ofNat t) (ofNat x)))) p162      = (p - 1) + p * (if Q2 ν (ofNat t) (ofNat x) = a then 1 else 0) := fun t x => by163    rw [conic_count F]164    congr 1165    have hiff : a + -(Q2 ν (ofNat t) (ofNat x)) = 0 ↔ Q2 ν (ofNat t) (ofNat x) = a := ⟨fun h => by166        calc Q2 ν (ofNat t) (ofNat x) = Q2 ν (ofNat t) (ofNat x) + (a + -(Q2 ν (ofNat t) (ofNat x))) := by rw [h, add_zero]167          _ = a := by rw [add_left_comm, add_neg, add_zero],168      fun h => by rw [h, add_neg]⟩169    match (inferInstance : Decidable (Q2 ν (ofNat t) (ofNat x) = a)) with170    | isTrue h => rw [ite_eq_left (hiff.2 h), ite_eq_left h, Nat.mul_one]171    | isFalse h => rw [ite_eq_right (fun h' => h (hiff.1 h')), ite_eq_right h, Nat.mul_zero]172  have ht : ∀ t, t < p → nsum (fun x => nsum (fun y => count (fun z =>173      ofNat y * ofNat y + z * z = a + -(Q2 ν (ofNat t) (ofNat x)))) p) p174      = p * (p - 1) + p * nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = a then 1 else 0) p := fun t _ => by175    rw [nsum_congr p (fun x _ => hx t x), nsum_add, nsum_const, nsum_mul_left]176  rw [nsum_congr p ht, nsum_add, nsum_const, nsum_mul_left, Nat.mul_assoc]177178/-- 3:B4, 3:B7 — the null cone of `Q_ν` for a nonsquare `ν`: `p³ − p² + p` points, the elliptic count (written179`N + p² = p³ + p`). -/180theorem null_elliptic (F : Frame p κ g) {ν : Shell p} (hν : ¬IsSquare ν) : formCount ν 0 + p * p = p * p * p + p := by181  rw [form_count F, plane_zero_aniso F hν, Nat.mul_one, Nat.add_right_comm, ← Nat.mul_succ]182  show p * p * ((p - 1) + 1) + p = p * p * p + p183  rw [FRC.Nat.sub_add_cancel Pos.pos]184185/-- 3:B4, 3:B2 — the null cone of `Q_ν` for a square `ν = w²`, `w ≠ 0`: `p³ + p² − p` points, the hyperbolic count186(written `N + p = p³ + p²`). -/187theorem null_hyperbolic (F : Frame p κ g) {w : Shell p} (hw : w ≠ 0) :188    formCount (w * w) 0 + p = p * p * p + p * p := by189  rw [form_count F]190  have h := plane_zero_split F hw191  have hp : (p - 1) + 1 = p := FRC.Nat.sub_add_cancel Pos.pos192  calc p * p * (p - 1) + p * planeCount (w * w) 0 + p = p * p * (p - 1) + p * (planeCount (w * w) 0 + 1) := by193        rw [Nat.mul_add, Nat.mul_one, Nat.add_assoc]194    _ = p * p * (p - 1) + p * p + p * p := by rw [h, Nat.mul_comm 2 p, ← Nat.mul_assoc, Nat.mul_two, Nat.add_assoc]195    _ = p * p * ((p - 1) + 1) + p * p := by rw [← Nat.mul_succ]196    _ = p * p * p + p * p := by rw [hp]197198end frame199200/-! ## The plane takes every nonzero value equally often (the drive) -/201202/-- The plane form under the scaling `(t, x) ↦ (wt, wx)`: `Q₂(wt, wx) = w² Q₂(t, x)`. -/203theorem q2_scale (ν w t x : Shell p) : Q2 ν (w * t) (w * x) = w * w * Q2 ν t x := by204  unfold Q2205  exact Shell.Frame.RE.sound (Shell.Frame.look [w, x, ν, t])206    (.add (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (.neg (.mul (.var 2) (.mul (.mul (.var 0) (.var 3)) (.mul (.var 0) (.var 3))))))207    (.mul (.mul (.var 0) (.var 0)) (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 2) (.mul (.var 3) (.var 3))))))208    (by decide +kernel)209210/-- The plane form under the swap `(t, x) ↦ (x, νt)`: `Q₂(x, νt) = −ν Q₂(t, x)`. -/211theorem q2_swap (ν t x : Shell p) : Q2 ν x (ν * t) = -(ν * Q2 ν t x) := by212  unfold Q2213  exact Shell.Frame.RE.sound (Shell.Frame.look [ν, t, x])214    (.add (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2)))))215    (.neg (.mul (.var 0) (.add (.mul (.var 2) (.var 2)) (.neg (.mul (.var 0) (.mul (.var 1) (.var 1)))))))216    (by decide +kernel)217218/-- Cancelling a positive factor in the naturals. -/219theorem nat_mul_left_cancel {a b c : Nat} (ha : 0 < a) (h : a * b = a * c) : b = c :=220  match Nat.lt_or_ge b c with221  | .inl hlt => absurd h (fun e => Nat.lt_irrefl (a * c) (by222      have := FRC.Nat.mul_lt_mul_of_lt_of_pos hlt ha223      rw [Nat.mul_comm b a, Nat.mul_comm c a, e] at this224      exact this))225  | .inr hge => match Nat.lt_or_ge c b with226    | .inl hlt => absurd h (fun e => Nat.lt_irrefl (a * b) (by227        have := FRC.Nat.mul_lt_mul_of_lt_of_pos hlt ha228        rw [Nat.mul_comm c a, Nat.mul_comm b a, ← e] at this229        exact this))230    | .inr hle => Nat.le_antisymm hle hge231232section frame233variable {κ : Nat} {g : Shell p}234235/-- `a·u = a·v` iff `u = v` for `a ≠ 0`. -/236theorem mul_cancel_iff (F : Frame p κ g) {a : Shell p} (ha : a ≠ 0) (u v : Shell p) : a * u = a * v ↔ u = v :=237  ⟨F.mul_left_cancel ha, fun h => by rw [h]⟩238239/-- The scaling: the plane takes `w² c` as often as `c`, for `w ≠ 0`. -/240theorem plane_scale (F : Frame p κ g) {w : Shell p} (hw : w ≠ 0) (ν c : Shell p) :241    planeCount ν (w * w * c) = planeCount ν c := by242  obtain ⟨u, hu⟩ := F.exists_inv hw243  have hinv : ∀ y : Shell p, u * (w * y) = y := fun y => by rw [← mul_assoc, mul_comm u w, hu, one_mul]244  have hww : w * w ≠ 0 := F.mul_ne_zero hw hw245  unfold planeCount246  have step1 : ∀ t, t < p → nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = c then 1 else 0) p247      = nsum (fun x => if Q2 ν (w * ofNat t) (w * ofNat x) = w * w * c then 1 else 0) p := fun t _ =>248    nsum_congr p (fun x _ => by249      rw [q2_scale]250      exact (ite_iff (mul_cancel_iff F hww _ _) 1 0).symm)251  have step2 : ∀ t, t < p → nsum (fun x => if Q2 ν (w * ofNat t) (w * ofNat x) = w * w * c then 1 else 0) p252      = nsum (fun x => if Q2 ν (w * ofNat t) (ofNat x) = w * w * c then 1 else 0) p := fun t _ =>253    nsum_bij (fun y => if Q2 ν (w * ofNat t) y = w * w * c then 1 else 0) (fun y => w * y) (fun y => u * y) hinv254  calc nsum (fun t => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = w * w * c then 1 else 0) p) p255      = nsum (fun t => (fun s : Shell p => nsum (fun x => if Q2 ν s (ofNat x) = w * w * c then 1 else 0) p) ((fun y => w * y) (ofNat t))) p :=256        (nsum_bij (fun s : Shell p => nsum (fun x => if Q2 ν s (ofNat x) = w * w * c then 1 else 0) p) (fun y => w * y) (fun y => u * y) hinv).symm257    _ = nsum (fun t => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = c then 1 else 0) p) p :=258        nsum_congr p (fun t ht => ((step1 t ht).trans (step2 t ht)).symm)259260/-- The swap: the plane takes `−ν c` as often as `c`, for `ν ≠ 0`. -/261theorem plane_swap (F : Frame p κ g) {ν : Shell p} (hν : ν ≠ 0) (c : Shell p) :262    planeCount ν (-(ν * c)) = planeCount ν c := by263  obtain ⟨u, hu⟩ := F.exists_inv hν264  have hinv : ∀ y : Shell p, u * (ν * y) = y := fun y => by rw [← mul_assoc, mul_comm u ν, hu, one_mul]265  have hneg : -ν ≠ 0 := fun h => hν (by rw [← neg_neg ν, h, neg_zero])266  have hiff : ∀ q : Shell p, -(ν * q) = -(ν * c) ↔ q = c := fun q => by267    rw [neg_mul, neg_mul]; exact mul_cancel_iff F hneg q c268  unfold planeCount269  have step1 : ∀ t, t < p → nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = c then 1 else 0) p270      = nsum (fun x => if Q2 ν (ofNat x) (ν * ofNat t) = -(ν * c) then 1 else 0) p := fun t _ =>271    nsum_congr p (fun x _ => by rw [q2_swap]; exact (ite_iff (hiff _) 1 0).symm)272  have step2 : ∀ x, x < p → nsum (fun t => if Q2 ν (ofNat x) (ν * ofNat t) = -(ν * c) then 1 else 0) p273      = nsum (fun t => if Q2 ν (ofNat x) (ofNat t) = -(ν * c) then 1 else 0) p := fun x _ =>274    nsum_bij (fun y => if Q2 ν (ofNat x) y = -(ν * c) then 1 else 0) (fun y => ν * y) (fun y => u * y) hinv275  calc nsum (fun t => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = -(ν * c) then 1 else 0) p) p276      = nsum (fun x => nsum (fun t => if Q2 ν (ofNat x) (ν * ofNat t) = -(ν * c) then 1 else 0) p) p :=277        (nsum_congr p step2).symm278    _ = nsum (fun t => nsum (fun x => if Q2 ν (ofNat x) (ν * ofNat t) = -(ν * c) then 1 else 0) p) p :=279        nsum_comm (fun x t => if Q2 ν (ofNat x) (ν * ofNat t) = -(ν * c) then 1 else 0) p p280    _ = nsum (fun t => nsum (fun x => if Q2 ν (ofNat t) (ofNat x) = c then 1 else 0) p) p :=281        nsum_congr p (fun t ht => (step1 t ht).symm)282283/-- For the drive `g`, the plane takes every nonzero value as often as `1`. -/284theorem plane_const (F : Frame p κ g) {c : Shell p} (hc : c ≠ 0) : planeCount g c = planeCount g 1 := by285  have hg : g ≠ 0 := by have := F.pow_ne_zero 1; rw [Shell.pow_one] at this; exact this286  have hi : quarterTurn g κ ≠ 0 := fun h => F.one_ne_zero (by287    have := F.quarter_turn_sq288    rw [h, mul_zero] at this289    rw [← neg_neg (1 : Shell p), ← this, neg_zero])290  obtain ⟨k, _, hk⟩ := F.eq_pow_of_ne_zero hc291  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec 2 (Nat.zero_lt_succ 1) k292  have hsq : ∀ j, g ^ (2 * j) = g ^ j * g ^ j := fun j => by rw [Nat.mul_comm, Shell.pow_mul, Shell.pow_two]293  have hwq : g ^ q ≠ 0 := F.pow_ne_zero q294  have h1 : planeCount g (-1) = planeCount g 1 := by295    rw [← F.quarter_turn_sq, ← mul_one (quarterTurn g κ * quarterTurn g κ)]296    exact plane_scale F hi g 1297  match mod_two_cases k with298  | .inl h0 =>299    rw [h0, Nat.add_zero] at hq300    rw [← hk, hq, hsq, ← mul_one (g ^ q * g ^ q)]301    exact plane_scale F hwq g 1302  | .inr h1' =>303    rw [h1'] at hq304    have e : c = g ^ q * g ^ q * g := by rw [← hk, hq, Shell.pow_add, hsq, Shell.pow_one]305    have eg : -(g * -1) = g := by rw [← mul_neg, neg_neg, mul_one]306    rw [e, plane_scale F hwq g g]307    calc planeCount g g = planeCount g (-(g * -1)) := by rw [eg]308      _ = planeCount g (-1) := plane_swap F hg (-1)309      _ = planeCount g 1 := h1310311/-- 3:C2, 3:B6 — for the drive `g` the plane `x² − g t²` takes every nonzero value `p + 1` times: the norm-one cycle of312`𝔽_p(√g)` (the boosts, `γ² − g b² = 1`) has `p + 1` elements. -/313theorem plane_nonzero (F : Frame p κ g) {c : Shell p} (hc : c ≠ 0) : planeCount g c = p + 1 := by314  rw [plane_const F hc]315  have hgns : ¬IsSquare g := drive_nonsquare F316  have htot := plane_total g317  rw [nsum_split (fun c => planeCount g c), plane_zero_aniso F hgns,318    nsum_congr (p - 1) (fun l hl => plane_const F (succ_ne_zero' hl)), nsum_const] at htot319  have hp : (p - 1) + 1 = p := FRC.Nat.sub_add_cancel Pos.pos320  have e : 1 + (p - 1) * (p - 1 + 1 + 1) = p * p := by321    calc 1 + (p - 1) * (p - 1 + 1 + 1) = (p - 1) * (p - 1) + (p - 1) + ((p - 1) + 1) := by322          rw [Nat.mul_succ, Nat.mul_succ, Nat.add_comm 1, Nat.add_assoc ((p - 1) * (p - 1) + (p - 1))]323      _ = ((p - 1) + 1) * ((p - 1) + 1) := by rw [Nat.succ_mul, Nat.mul_succ]324      _ = p * p := by rw [hp]325  have h2 : (p - 1) * planeCount g 1 = (p - 1) * (p - 1 + 1 + 1) :=326    FRC.Nat.add_left_cancel (htot.trans e.symm)327  rw [nat_mul_left_cancel F.n_pos h2, hp]328329/-- 3:B6 — for the drive `g` every nonzero value of `Q_g = −g t² + x² + y² + z²` is taken `p³ + p` times; at `a = −g`330this is the time sphere, whose `p³ + p` points times `|O(3, 𝔽_p)| = 2p(p² − 1)` give `|O₄⁻(p)| = 2p²(p⁴ − 1)`. -/331theorem sphere_drive (F : Frame p κ g) {a : Shell p} (ha : a ≠ 0) : formCount g a = p * p * p + p := by332  rw [form_count F, plane_nonzero F ha, Nat.mul_succ, ← Nat.add_assoc, ← Nat.mul_succ]333  show p * p * ((p - 1) + 1) + p = p * p * p + p334  rw [FRC.Nat.sub_add_cancel Pos.pos]335336end frame337338/-! ## The causal classes, the pair algebra, the boost in dimension `1 + 3` -/339340section frame341variable {κ : Nat} {g : Shell p}342343/-- 3:B7 — the similitude `(t, x, y, z) ↦ (cz, ax − by, bx + ay, cνt)` with `a² + b² = ν` and `c² = −1` multiplies344`Q_ν = −ν t² + x² + y² + z²` by `ν`. -/345theorem similitude (ν a b c t x y z : Shell p) (hab : a * a + b * b = ν) (hc : c * c = -1) :346    -(ν * ((c * z) * (c * z))) + (a * x + -(b * y)) * (a * x + -(b * y)) + (b * x + a * y) * (b * x + a * y)347      + (c * (ν * t)) * (c * (ν * t))348      = ν * (-(ν * (t * t)) + x * x + y * y + z * z) := by349  have e : -(ν * ((c * z) * (c * z))) + (a * x + -(b * y)) * (a * x + -(b * y)) + (b * x + a * y) * (b * x + a * y)350      + (c * (ν * t)) * (c * (ν * t))351      = ν * (-(ν * (t * t)) + x * x + y * y + z * z) + (c * c + 1) * (ν * ν * (t * t) + -(ν * (z * z)))352        + (a * a + b * b + -ν) * (x * x + y * y) :=353    Shell.Frame.RE.sound (Shell.Frame.look [ν, a, b, c, t, x, y, z])354      (.add (.add (.add (.neg (.mul (.var 0) (.mul (.mul (.var 3) (.var 7)) (.mul (.var 3) (.var 7)))))355        (.mul (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 6)))) (.add (.mul (.var 1) (.var 5)) (.neg (.mul (.var 2) (.var 6))))))356        (.mul (.add (.mul (.var 2) (.var 5)) (.mul (.var 1) (.var 6))) (.add (.mul (.var 2) (.var 5)) (.mul (.var 1) (.var 6)))))357        (.mul (.mul (.var 3) (.mul (.var 0) (.var 4))) (.mul (.var 3) (.mul (.var 0) (.var 4)))))358      (.add (.add (.mul (.var 0) (.add (.add (.add (.neg (.mul (.var 0) (.mul (.var 4) (.var 4)))) (.mul (.var 5) (.var 5))) (.mul (.var 6) (.var 6))) (.mul (.var 7) (.var 7))))359        (.mul (.add (.mul (.var 3) (.var 3)) .one) (.add (.mul (.mul (.var 0) (.var 0)) (.mul (.var 4) (.var 4))) (.neg (.mul (.var 0) (.mul (.var 7) (.var 7)))))))360        (.mul (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 2) (.var 2))) (.neg (.var 0))) (.add (.mul (.var 5) (.var 5)) (.mul (.var 6) (.var 6)))))361      (by decide +kernel)362  have h1 : c * c + 1 = 0 := by rw [hc, neg_add]363  have h2 : a * a + b * b + -ν = 0 := by rw [hab, add_neg]364  rw [e, h1, h2, zero_mul, zero_mul, add_zero, add_zero]365366/-- 3:B7 — multiplication by the drive exchanges the two square classes of the nonzero residues. -/367theorem class_flip (F : Frame p κ g) {s : Shell p} (hs : s ≠ 0) : IsSquare s ↔ ¬IsSquare (g * s) := by368  obtain ⟨k, _, hk⟩ := F.eq_pow_of_ne_zero hs369  have hgs : g * s = g ^ (k + 1) := by rw [← hk, Shell.pow_succ, mul_comm]370  constructor371  · intro hsq hgsq372    have h0 : k % 2 = 0 := (parity_iff F k).1 (match hsq with | ⟨y, hy⟩ => ⟨y, hy.trans hk.symm⟩)373    have h1 : (k + 1) % 2 = 0 := (parity_iff F (k + 1)).1 (match hgsq with | ⟨y, hy⟩ => ⟨y, hy.trans hgs⟩)374    have h2 := (succ_mod_two_eq_zero_iff k).1 h1375    rw [h0] at h2376    exact Nat.noConfusion h2377  · intro hn378    match mod_two_cases k with379    | .inl h0 => exact match (parity_iff F k).2 h0 with | ⟨y, hy⟩ => ⟨y, hy.trans hk⟩380    | .inr h1 => exact absurd (match (parity_iff F (k + 1)).2 ((succ_mod_two_eq_zero_iff k).2 h1) with381        | ⟨y, hy⟩ => ⟨y, hy.trans hgs.symm⟩) hn382383/-- 3:B8 — the drive cycle `𝔽_p^×` meets the norm-one cycle of `𝔽_p(√ν)` in `±1`: `γ² − ν·0² = 1` forces `γ = ±1`. -/384theorem drive_meets_norm_one (F : Frame p κ g) {ν γ : Shell p} (h : γ * γ + -(ν * (0 * 0)) = 1) : γ = 1 ∨ γ = -1 := by385  rw [mul_zero, mul_zero, neg_zero, add_zero] at h386  exact ((root_pair F 1 1 (mul_one 1) F.one_ne_zero).1 γ).1 h387388/-- 3:C4 — the `x`-boost `Λ ⊕ I₂` lies in `O(Q_ν, 𝔽_p)` on every shell: it preserves `x² − ν t² + y² + z²`. -/389theorem xboost_preserves {ν γ b : Shell p} (h : γ * γ + -(ν * (b * b)) = 1) (t x y z : Shell p) :390    Q2 ν (boostT ν γ b t x) (boostX ν γ b t x) + (y * y + z * z) = Q2 ν t x + (y * y + z * z) := by391  rw [boost_preserves h]392393end frame394395/-! ## The generation of the Lorentz group of the shell: the reduction to a spatial vector -/396397section frame398variable {κ : Nat} {g : Shell p}399400/-- 3:C4 — the square shift: for `t ≠ 0` the residue `x = (1 + g t²)/2` makes `x² − g t²` the nonzero square `y²`,401`y = (g t² − 1)/2`; `y ≠ 0` since `g t² = 1` would make the drive a square. -/402theorem square_shift (F : Frame p κ g) {t : Shell p} (ht : t ≠ 0) :403    ∃ x y : Shell p, y ≠ 0 ∧ x * x + -(g * (t * t)) = y * y := by404  obtain ⟨h, hh⟩ := F.exists_inv F.two_ne_zero405  have h2 : h + h = 1 := by rw [← two_mul', hh]406  let u := g * (t * t)407  have e : ((1 + u) * h) * ((1 + u) * h) + -u = ((u + -1) * h) * ((u + -1) * h) + u * ((h + h) * (h + h) + -1) :=408    Shell.Frame.RE.sound (Shell.Frame.look [u, h])409      (.add (.mul (.mul (.add .one (.var 0)) (.var 1)) (.mul (.add .one (.var 0)) (.var 1))) (.neg (.var 0)))410      (.add (.mul (.mul (.add (.var 0) (.neg .one)) (.var 1)) (.mul (.add (.var 0) (.neg .one)) (.var 1)))411        (.mul (.var 0) (.add (.mul (.add (.var 1) (.var 1)) (.add (.var 1) (.var 1))) (.neg .one))))412      (by decide +kernel)413  refine ⟨(1 + u) * h, (u + -1) * h, fun hy => ?_, ?_⟩414  · have hh0 : h ≠ 0 := fun h0 => F.one_ne_zero (by rw [← hh, h0, mul_zero])415    have hu : u + -1 = 0 := match F.mul_eq_zero hy with416      | .inl e1 => e1417      | .inr e2 => absurd e2 hh0418    have hu1 : g * (t * t) = 1 := by419      calc g * (t * t) = u + -1 + 1 := by rw [add_assoc, neg_add, add_zero]420        _ = 1 := by rw [hu, zero_add]421    obtain ⟨s, hs⟩ := F.exists_inv ht422    exact drive_nonsquare F ⟨s, by423      calc s * s = g * (t * t) * (s * s) := by rw [hu1, one_mul]424        _ = g * ((t * s) * (t * s)) := by rw [mul_assoc, sq_mul t s]425        _ = g := by rw [hs, mul_one, mul_one]⟩426  · rw [e, h2, mul_one, add_neg, mul_zero, add_zero]427428/-- 3:C4 — the boosts act transitively on each level set of the plane `x² − g t² = m`, `m ≠ 0`: the boost429`γ = (x₂x₁ − g t₂t₁)/m`, `b = (t₂x₁ − x₂t₁)/m` (the quotient of the two points in `𝔽_p(√g)`) carries `(t₁, x₁)` to430`(t₂, x₂)`. -/431theorem boost_transitive (F : Frame p κ g) {t₁ x₁ t₂ x₂ : Shell p}432    (hm : Q2 g t₁ x₁ ≠ 0) (h12 : Q2 g t₁ x₁ = Q2 g t₂ x₂) :433    ∃ γ b : Shell p, γ * γ + -(g * (b * b)) = 1 ∧ boostT g γ b t₁ x₁ = t₂ ∧ boostX g γ b t₁ x₁ = x₂ := by434  obtain ⟨n, hn⟩ := F.exists_inv hm435  let m := Q2 g t₁ x₁436  have hm1 : m = x₁ * x₁ + -(g * (t₁ * t₁)) := rfl437  have hm2 : m = x₂ * x₂ + -(g * (t₂ * t₂)) := h12438  refine ⟨(x₂ * x₁ + -(g * (t₂ * t₁))) * n, (t₂ * x₁ + -(x₂ * t₁)) * n, ?_, ?_, ?_⟩439  · -- Brahmagupta: (x₂x₁ − g t₂t₁)² − g (t₂x₁ − x₂t₁)² = (x₂² − g t₂²)(x₁² − g t₁²)440    have e : ((x₂ * x₁ + -(g * (t₂ * t₁))) * n) * ((x₂ * x₁ + -(g * (t₂ * t₁))) * n)441        + -(g * (((t₂ * x₁ + -(x₂ * t₁)) * n) * ((t₂ * x₁ + -(x₂ * t₁)) * n)))442        = ((x₂ * x₂ + -(g * (t₂ * t₂))) * n) * ((x₁ * x₁ + -(g * (t₁ * t₁))) * n) :=443      Shell.Frame.RE.sound (Shell.Frame.look [x₁, t₁, x₂, t₂, g, n])444        (.add (.mul (.mul (.add (.mul (.var 2) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 3) (.var 1))))) (.var 5))445                    (.mul (.add (.mul (.var 2) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 3) (.var 1))))) (.var 5)))446              (.neg (.mul (.var 4) (.mul (.mul (.add (.mul (.var 3) (.var 0)) (.neg (.mul (.var 2) (.var 1)))) (.var 5))447                    (.mul (.add (.mul (.var 3) (.var 0)) (.neg (.mul (.var 2) (.var 1)))) (.var 5))))))448        (.mul (.mul (.add (.mul (.var 2) (.var 2)) (.neg (.mul (.var 4) (.mul (.var 3) (.var 3))))) (.var 5))449              (.mul (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 1) (.var 1))))) (.var 5)))450        (by decide +kernel)451    rw [e, ← hm2, ← hm1]452    show Q2 g t₁ x₁ * n * (Q2 g t₁ x₁ * n) = 1453    rw [hn, mul_one]454  · -- γ t₁ + b x₁ = t₂ (x₁² − g t₁²) / m455    unfold boostT456    have e : ((x₂ * x₁ + -(g * (t₂ * t₁))) * n) * t₁ + ((t₂ * x₁ + -(x₂ * t₁)) * n) * x₁457        = t₂ * ((x₁ * x₁ + -(g * (t₁ * t₁))) * n) :=458      Shell.Frame.RE.sound (Shell.Frame.look [x₁, t₁, x₂, t₂, g, n])459        (.add (.mul (.mul (.add (.mul (.var 2) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 3) (.var 1))))) (.var 5)) (.var 1))460              (.mul (.mul (.add (.mul (.var 3) (.var 0)) (.neg (.mul (.var 2) (.var 1)))) (.var 5)) (.var 0)))461        (.mul (.var 3) (.mul (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 1) (.var 1))))) (.var 5)))462        (by decide +kernel)463    rw [e, ← hm1]464    show _ * (Q2 g t₁ x₁ * n) = _465    rw [hn, mul_one]466  · -- γ x₁ + g b t₁ = x₂ (x₁² − g t₁²) / m467    unfold boostX468    have e : ((x₂ * x₁ + -(g * (t₂ * t₁))) * n) * x₁ + g * (((t₂ * x₁ + -(x₂ * t₁)) * n) * t₁)469        = x₂ * ((x₁ * x₁ + -(g * (t₁ * t₁))) * n) :=470      Shell.Frame.RE.sound (Shell.Frame.look [x₁, t₁, x₂, t₂, g, n])471        (.add (.mul (.mul (.add (.mul (.var 2) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 3) (.var 1))))) (.var 5)) (.var 0))472              (.mul (.var 4) (.mul (.mul (.add (.mul (.var 3) (.var 0)) (.neg (.mul (.var 2) (.var 1)))) (.var 5)) (.var 1))))473        (.mul (.var 2) (.mul (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 1) (.var 1))))) (.var 5)))474        (by decide +kernel)475    rw [e, ← hm1]476    show _ * (Q2 g t₁ x₁ * n) = _477    rw [hn, mul_one]478479/-- 3:C4 — time to space: for `t ≠ 0` there are a residue `x` and a boost carrying `(t, x)` to `(0, y)` with `y ≠ 0`.480With the spatial rotations, which give the spatial part any `x`-component (Witt), every non-null vector of `Q_g` is481carried to a spatial one; the conjugates of the spatial reflections are then all the reflections, which generate482`O(Q_g, 𝔽_p)` (Cartan–Dieudonné). -/483theorem time_to_space (F : Frame p κ g) {t : Shell p} (ht : t ≠ 0) :484    ∃ x y γ b : Shell p, y ≠ 0 ∧ γ * γ + -(g * (b * b)) = 1 ∧ boostT g γ b t x = 0 ∧ boostX g γ b t x = y := by485  obtain ⟨x, y, hy, hxy⟩ := square_shift F ht486  have hq : Q2 g t x = Q2 g 0 y := by487    show x * x + -(g * (t * t)) = y * y + -(g * (0 * 0))488    rw [hxy, mul_zero, mul_zero, neg_zero, add_zero]489  have hm : Q2 g t x ≠ 0 := by490    rw [hq]; show y * y + -(g * (0 * 0)) ≠ 0491    rw [mul_zero, mul_zero, neg_zero, add_zero]492    exact fun h => hy ((sq_eq_zero F).1 h)493  obtain ⟨γ, b, hγ, h1, h2⟩ := boost_transitive F hm hq494  exact ⟨x, y, γ, b, hy, hγ, h1, h2⟩495496end frame497498/-! ## The worked shells -/499500/-- The frame of the laboratory Subject `𝔽₁₇₃`, drive `2`. -/501theorem frame173 : Frame 173 43 (2 : Shell 173) := ⟨rfl, Nat.zero_lt_succ 42, by decide +kernel⟩502503/-- 3:D1 [value] — `𝔽₁₃`: `14` boosts, decided by the kernel. -/504theorem normOne13 : normOneCount 13 2 = 14 := by decide +kernel505506/-- 3:D1 [value] — `𝔽₁₇₃`, drive `2`: the null cone of `Q_2` has `173³ − 173² + 173 = 5 147 961` points and the507boosts number `174`, from the general counts on the frame `(τ; 0, 1, 2)`. -/508theorem shell173 : formCount (2 : Shell 173) 0 + 173 * 173 = 173 * 173 * 173 + 173 ∧ planeCount (2 : Shell 173) 1 = 174 :=509  ⟨null_elliptic frame173 (drive_nonsquare frame173), plane_nonzero frame173 (by decide)⟩510511end FRC.Causal512