Theme/Projective.lean — FrcCore

1import FrcCore.Ring2import FrcCore.Frame34/-!5# FrcCore.Theme.Projective — the affine group of the shell (the projective theme, ledger migration task LM17)67The affine maps `x ↦ a + b·x`, `b ≠ 0`: the Borel subgroup of `PGL₂` acting on the shell's affine line. They form a8group under composition and act simply transitively on the frames `(a, b)`; there are `p·(p − 1)` of them9(1:C2, 4:C5). Moved from 1-algebra with their names unchanged. No axioms.10-/1112namespace FRC13namespace Shell14namespace Frame1516variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}1718/-- An affine map of the shell, `x ↦ a + b·x` with `b ≠ 0`. -/19structure Affine (p : Nat) [Pos p] where20  a : Shell p21  b : Shell p22  hb : b ≠ 02324namespace Affine2526def apply (φ : Affine p) (x : Shell p) : Shell p := φ.a + φ.b * x2728theorem ext' {φ ψ : Affine p} (ha : φ.a = ψ.a) (hb : φ.b = ψ.b) : φ = ψ := by29  cases φ; cases ψ; cases ha; cases hb; rfl3031/-- The identity `x ↦ 0 + 1·x`. -/32def one (F : Frame p κ g) : Affine p := ⟨0, 1, F.one_ne_zero⟩3334/-- Composition: `(a, b) ∘ (c, d) = (a + b·c, b·d)`. -/35def comp (F : Frame p κ g) (φ ψ : Affine p) : Affine p := ⟨φ.a + φ.b * ψ.a, φ.b * ψ.b, F.mul_ne_zero φ.hb ψ.hb⟩3637theorem comp_apply (F : Frame p κ g) (φ ψ : Affine p) (x : Shell p) :38    (comp F φ ψ).apply x = φ.apply (ψ.apply x) := by39  unfold comp apply40  show φ.a + φ.b * ψ.a + φ.b * ψ.b * x = φ.a + φ.b * (ψ.a + ψ.b * x)41  rw [left_distrib, add_assoc, mul_assoc]4243theorem one_apply (F : Frame p κ g) (x : Shell p) : (one F).apply x = x := by44  unfold one apply; show 0 + 1 * x = x; rw [one_mul, zero_add]4546theorem comp_assoc (F : Frame p κ g) (φ ψ χ : Affine p) : comp F (comp F φ ψ) χ = comp F φ (comp F ψ χ) :=47  ext' (by show φ.a + φ.b * ψ.a + φ.b * ψ.b * χ.a = φ.a + φ.b * (ψ.a + ψ.b * χ.a); rw [left_distrib, add_assoc, mul_assoc])48    (by show φ.b * ψ.b * χ.b = φ.b * (ψ.b * χ.b); exact mul_assoc _ _ _)4950/-- The inverse of `(a, b)`: `(−a·b⁻¹, b⁻¹)`, with `y` the inverse of `b`. -/51def inv (F : Frame p κ g) (φ : Affine p) (y : Shell p) (hy : φ.b * y = 1) : Affine p :=52  ⟨-(φ.a * y), y, fun h => F.one_ne_zero (by rw [← hy, h, mul_zero])⟩5354theorem comp_inv (F : Frame p κ g) (φ : Affine p) (y : Shell p) (hy : φ.b * y = 1) :55    comp F φ (inv F φ y hy) = one F :=56  ext' (by57      show φ.a + φ.b * -(φ.a * y) = 058      calc φ.a + φ.b * -(φ.a * y) = φ.a + -(φ.b * (φ.a * y)) := by rw [← mul_neg]59        _ = φ.a + -(φ.a * (φ.b * y)) := by rw [mul_left_comm]60        _ = φ.a + -φ.a := by rw [hy, mul_one]61        _ = 0 := add_neg _)62    (by show φ.b * y = 1; exact hy)6364/-- 1:C2, 4:C5 (the frame group), simple transitivity — for frames `(a, b)` and `(c, d)` (`b, d ≠ 0`) there65is exactly one affine map carrying the first to the second: `φ (a, b) := (φ.apply a, φ.b · b)`. -/66theorem simply_transitive (F : Frame p κ g) (a b c d : Shell p) (hb : b ≠ 0) (hd : d ≠ 0) :67    (∃ φ : Affine p, φ.apply a = c ∧ φ.b * b = d) ∧68    (∀ φ ψ : Affine p, φ.apply a = c → φ.b * b = d → ψ.apply a = c → ψ.b * b = d → φ = ψ) := by69  match F.exists_inv hb with70  | ⟨y, hy⟩ =>71    constructor72    · refine ⟨⟨c + -(d * y * a), d * y, ?_⟩, ?_, ?_⟩73      · exact F.mul_ne_zero hd (fun h => F.one_ne_zero (by rw [← hy, h, mul_zero]))74      · show c + -(d * y * a) + d * y * a = c75        rw [add_assoc, neg_add, add_zero]76      · show d * y * b = d77        rw [mul_assoc, mul_comm y b, hy, mul_one]78    · intro φ ψ h1 h2 h3 h479      have eb : φ.b = ψ.b := by80        calc φ.b = φ.b * (b * y) := by rw [hy, mul_one]81          _ = (φ.b * b) * y := (mul_assoc _ _ _).symm82          _ = (ψ.b * b) * y := by rw [h2, h4]83          _ = ψ.b := by rw [mul_assoc, hy, mul_one]84      have ea : φ.a = ψ.a := by85        have e1 : φ.a + φ.b * a = c := h186        have e2 : ψ.a + ψ.b * a = c := h387        rw [← eb] at e288        exact add_right_cancel (e1.trans e2.symm)89      exact ext' ea eb9091end Affine9293/-- 1:C2, 4:C5, the order — the frames `(a, b)`, `b ≠ 0`, number `p·(p − 1)`: `p` choices of the origin, `p − 1`94of the unit. -/95theorem frame_count :96    natCount (fun _ => True) p * natCount (fun b => b ≠ 0) p = p * (p - 1) := by97  have h1 : ∀ n, natCount (fun _ => True) n = n := fun n => by98    induction n with99    | zero => rfl100    | succ n ih => show natCount (fun _ => True) n + (if True then 1 else 0) = n + 1; rw [ih, ite_eq_left trivial]101  have hp : p = (p - 1) + 1 := (FRC.Nat.sub_add_cancel Pos.pos).symm102  rw [h1]103  have h2 : natCount (fun b => b ≠ 0) p = p - 1 := by104    have := natCount_ne_zero (p - 1)105    rw [← hp] at this; exact this106  rw [h2]107108109/-! ## C19: the Hopf section of `PGL₂` (task LM25)110111`PGL₂(𝔽_p)` by elements: a matrix `[[a, b], [c, d]]` acts on the projective line by `[x : y] ↦ [a x + b y : c x + d y]`112and is read up to a nonzero scalar. The non-split torus is the boosts `[[α, νβ], [β, α]]` (`ν` a nonsquare), the Borel113subgroup the upper-triangular matrices, the stabiliser of the horizon `[1 : 0]`: the cone chart `x ↦ a x + b`. -/114115/-- A 2 × 2 matrix over the shell. -/116structure M2 (p : Nat) [Pos p] where117  a : Shell p118  b : Shell p119  c : Shell p120  d : Shell p121122namespace M2123124theorem ext' {M N : M2 p} (ha : M.a = N.a) (hb : M.b = N.b) (hc : M.c = N.c) (hd : M.d = N.d) : M = N := by125  cases M; cases N; cases ha; cases hb; cases hc; cases hd; rfl126127/-- The product. -/128theorem ext'_a {M N : M2 p} (h : M = N) : M.a = N.a := by cases h; rfl129theorem ext'_b {M N : M2 p} (h : M = N) : M.b = N.b := by cases h; rfl130theorem ext'_c {M N : M2 p} (h : M = N) : M.c = N.c := by cases h; rfl131theorem ext'_d {M N : M2 p} (h : M = N) : M.d = N.d := by cases h; rfl132133def mul (M N : M2 p) : M2 p :=134  ⟨M.a * N.a + M.b * N.c, M.a * N.b + M.b * N.d, M.c * N.a + M.d * N.c, M.c * N.b + M.d * N.d⟩135136/-- A scalar multiple. -/137def smul (l : Shell p) (M : M2 p) : M2 p := ⟨l * M.a, l * M.b, l * M.c, l * M.d⟩138139/-- The determinant. -/140def det (M : M2 p) : Shell p := M.a * M.d + -(M.b * M.c)141142/-- The action on the projective line, `[x : y] ↦ [a x + b y : c x + d y]`. -/143def act (M : M2 p) (x y : Shell p) : Shell p × Shell p := (M.a * x + M.b * y, M.c * x + M.d * y)144145end M2146147/-- The boost `α + β w` as a matrix, `[[α, ν β], [β, α]]`: the non-split torus `C_{p+1}`. -/148def boost (ν α β : Shell p) : M2 p := ⟨α, ν * β, β, α⟩149150/-- An upper-triangular matrix `[[a, b], [0, e]]`: the Borel subgroup, the cone chart `x ↦ (a x + b)/e`. -/151def borel (a b e : Shell p) : M2 p := ⟨a, b, 0, e⟩152153/-- Two points `(x, y)`, `(x', y')` of the projective line are equal, `x y' = x' y`. -/154def PEq (u v : Shell p × Shell p) : Prop := u.1 * v.2 = v.1 * u.2155156theorem eq_of_add_neg_eq_zero {x y : Shell p} (h : x + -y = 0) : x = y := by157  rw [← add_zero x, ← neg_add y, ← add_assoc, h, zero_add]158159/-- The field laws of a shell, as the Hopf section and the frame triple use them; a frame gives them (`Frame.fld`), so160does primality (`Prime.fld`, `Theme/Hopf.lean`): the theorems below hold on every prime shell (38:A9). -/161structure Fld (p : Nat) [Pos p] : Prop where162  one_ne_zero : (1 : Shell p) ≠ 0163  exists_inv : ∀ {x : Shell p}, x ≠ 0 → ∃ y, x * y = 1164  mul_eq_zero : ∀ {a b : Shell p}, a * b = 0 → a = 0 ∨ b = 0165  mul_ne_zero : ∀ {a b : Shell p}, a ≠ 0 → b ≠ 0 → a * b ≠ 0166  mul_left_cancel : ∀ {a b c : Shell p}, a ≠ 0 → a * b = a * c → b = c167  sq_eq_one : ∀ {x : Shell p}, x * x = 1 → x = 1 ∨ x = -1168169/-- A frame has the field laws. -/170theorem fld (F : Frame p κ g) : Fld p :=171  ⟨F.one_ne_zero, fun hx => F.exists_inv hx, fun h => F.mul_eq_zero h, fun ha hb => F.mul_ne_zero ha hb,172   fun ha h => F.mul_left_cancel ha h, fun h => F.sq_eq_one h⟩173174/-- 38:A9, 00:C19 — on a field-law shell, `x² − ν y² ≠ 0` for `(x, y) ≠ 0` when `ν` is a nonsquare. -/175theorem Fld.norm_ne_zero (K : Fld p) {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) {x y : Shell p}176    (hxy : x ≠ 0 ∨ y ≠ 0) : x * x + -(ν * (y * y)) ≠ 0 := fun h => by177  have e := eq_of_add_neg_eq_zero h178  match Shell.instDecidableEq y 0 with179  | .isTrue hy =>180    rw [hy, mul_zero, mul_zero] at e181    exact hxy.elim (fun hx => hx (match K.mul_eq_zero e with | .inl h => h | .inr h => h)) (fun h => h hy)182  | .isFalse hy =>183    obtain ⟨s, hs⟩ := K.exists_inv hy184    exact hν ⟨x * s, by rw [mul_mul_mul_comm, e, mul_assoc, ← mul_mul_mul_comm, hs, mul_one, mul_one]⟩185186/-- 38:A7, 38:A9 — **C19 (p00039), the Hopf section.** In `PGL₂(𝔽_p)` on a frame, `ν` a nonsquare:187(1) a boost that is not scalar fixes no point of `ℙ¹`; (2) a boost in the Borel subgroup is scalar: `T ∩ B = 1`;188(3) every invertible matrix factors as (cone chart) × (boost) up to a scalar, (4) uniquely up to scalars — the cone189chart is a global section of `G → G/T`; (5) the boost classes are the points of `ℙ¹` (`p + 1` per fibre) and (6) the190cone charts number `p (p − 1)`; (7) on the spin cover `SL₂` the sign `−I` is both a boost and a chart, `B ∩ T = {±I}`191there, and `b t = (−b)(−t)`: the section obstructs at `−1`. -/192theorem Fld.hopf_section (K : Fld p) {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) :193    (∀ α β x y : Shell p, β ≠ 0 → (x ≠ 0 ∨ y ≠ 0) → ¬ PEq ((boost ν α β).act x y) (x, y)) ∧194    (∀ α β a b e l : Shell p, boost ν α β = M2.smul l (borel a b e) → β = 0) ∧195    (∀ M : M2 p, M.det ≠ 0 → ∃ N a b e α β : Shell p, N ≠ 0 ∧ a * e ≠ 0 ∧ (α ≠ 0 ∨ β ≠ 0) ∧196      M2.smul N M = (borel a b e).mul (boost ν α β)) ∧197    (∀ l a1 b1 e1 α1 β1 a2 b2 e2 α2 β2 : Shell p, l ≠ 0 → e2 ≠ 0 → (α1 ≠ 0 ∨ β1 ≠ 0) →198      M2.smul l ((borel a1 b1 e1).mul (boost ν α1 β1)) = (borel a2 b2 e2).mul (boost ν α2 β2) →199      α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) ∧200    (∀ α β α' β' : Shell p, (α ≠ 0 ∨ β ≠ 0) → (α' ≠ 0 ∨ β' ≠ 0) →201      ((∃ μ : Shell p, μ ≠ 0 ∧ boost ν α' β' = M2.smul μ (boost ν α β)) ↔ α * β' = α' * β)) ∧202    natCount (fun _ => True) p * natCount (fun b => b ≠ 0) p = p * (p - 1) ∧203    (boost ν (-1) 0 = borel (-1) 0 (-1) ∧ (-1 : Shell p) * -1 + -(ν * (0 * 0)) = 1 ∧ (-1 : Shell p) * -1 = 1 ∧204      (∀ α β a b e : Shell p, boost ν α β = borel a b e → α * α + -(ν * (β * β)) = 1 → β = 0 ∧ (α = 1 ∨ α = -1)) ∧205      ∀ M N : M2 p, (M2.smul (-1) M).mul (M2.smul (-1) N) = M.mul N) := by206  have hN : ∀ {x y : Shell p}, (x ≠ 0 ∨ y ≠ 0) → x * x + -(ν * (y * y)) ≠ 0 := fun hxy => K.norm_ne_zero hν hxy207  refine ⟨fun α β x y hβ hxy hP => ?_, fun α β a b e l h => ?_, fun M hM => ?_,208    fun l a1 b1 e1 α1 β1 a2 b2 e2 α2 β2 hl he2 hαβ h => ?_, fun α β α' β' h1 h2 => ?_, frame_count, ?_⟩209  · -- (1) a fixed point forces `β (ν y² − x²) = 0`210    have e : (α * x + ν * β * y) * y + -(x * (β * x + α * y)) = β * (ν * (y * y) + -(x * x)) :=211      Shell.Frame.RE.sound (Shell.Frame.look [α, β, ν, x, y])212        (.add (.mul (.add (.mul (.var 0) (.var 3)) (.mul (.mul (.var 2) (.var 1)) (.var 4))) (.var 4)) (.neg (.mul (.var 3) (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.var 4))))))213        (.mul (.var 1) (.add (.mul (.var 2) (.mul (.var 4) (.var 4))) (.neg (.mul (.var 3) (.var 3))))) (by decide +kernel)214    have hP' : (α * x + ν * β * y) * y = x * (β * x + α * y) := hP215    rw [hP', add_neg] at e216    match K.mul_eq_zero e.symm with217    | .inl h => exact hβ h218    | .inr h =>219      have h' : x * x + -(ν * (y * y)) = 0 := by220        rw [← neg_neg (x * x + -(ν * (y * y))), neg_add_rev, neg_neg, add_comm, h, neg_zero]221      exact hN hxy h'222  · -- (2) the `c`-entry223    have := congrArg M2.c h224    show β = 0225    exact this.trans (mul_zero l)226  · -- (3) `N M = [[det, b d − ν a c], [0, N]] · boost (d, c)`, `N = d² − ν c²`227    have hcd : M.d ≠ 0 ∨ M.c ≠ 0 := by228      match Shell.instDecidableEq M.d 0, Shell.instDecidableEq M.c 0 with229      | .isTrue hd, .isTrue hc =>230        exact absurd (show M.det = 0 by231          show M.a * M.d + -(M.b * M.c) = 0; rw [hd, hc, mul_zero, mul_zero, neg_zero, add_zero]) hM232      | .isFalse hd, _ => exact .inl hd233      | _, .isFalse hc => exact .inr hc234    refine ⟨M.d * M.d + -(ν * (M.c * M.c)), M.det, M.b * M.d + -(ν * (M.a * M.c)), M.d * M.d + -(ν * (M.c * M.c)),235      M.d, M.c, hN hcd, K.mul_ne_zero hM (hN hcd), hcd, M2.ext' ?_ ?_ ?_ ?_⟩236    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν])237        (.mul (.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 0))238        (.add (.mul (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (.var 3)) (.mul (.add (.mul (.var 1) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 0) (.var 2))))) (.var 2))) (by decide +kernel)239    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν])240        (.mul (.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 1))241        (.add (.mul (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (.mul (.var 4) (.var 2))) (.mul (.add (.mul (.var 1) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 0) (.var 2))))) (.var 3))) (by decide +kernel)242    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν])243        (.mul (.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 2))244        (.add (.mul .zero (.var 3)) (.mul (.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 2))) (by decide +kernel)245    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν])246        (.mul (.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 3))247        (.add (.mul .zero (.mul (.var 4) (.var 2))) (.mul (.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 3))) (by decide +kernel)248  · -- (4) uniqueness: the torus class from the bottom row, the chart from the 2 × 2 system of determinant `N(α, β)`249    have ha : l * (a1 * α1 + b1 * β1) = a2 * α2 + b2 * β2 := congrArg M2.a h250    have hb : l * (a1 * (ν * β1) + b1 * α1) = a2 * (ν * β2) + b2 * α2 := congrArg M2.b h251    have hc : l * (0 * α1 + e1 * β1) = 0 * α2 + e2 * β2 := congrArg M2.c h252    have hd : l * (0 * (ν * β1) + e1 * α1) = 0 * (ν * β2) + e2 * α2 := congrArg M2.d h253    rw [zero_mul, zero_mul, zero_add, zero_add] at hc hd254    have hc' : e2 * β2 = l * (e1 * β1) := hc.symm255    have hd' : e2 * α2 = l * (e1 * α1) := hd.symm256    -- the torus class257    have t1 : e2 * (α1 * β2 + -(α2 * β1)) = α1 * (e2 * β2) + -(β1 * (e2 * α2)) := Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])258        (.mul (.var 8) (.add (.mul (.var 4) (.var 10)) (.neg (.mul (.var 9) (.var 5)))))259        (.add (.mul (.var 4) (.mul (.var 8) (.var 10))) (.neg (.mul (.var 5) (.mul (.var 8) (.var 9))))) (by decide +kernel)260    rw [hc', hd'] at t1261    have t2 : α1 * (l * (e1 * β1)) + -(β1 * (l * (e1 * α1))) = 0 := Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])262        (.add (.mul (.var 4) (.mul (.var 0) (.mul (.var 3) (.var 5)))) (.neg (.mul (.var 5) (.mul (.var 0) (.mul (.var 3) (.var 4))))))263        .zero (by decide +kernel)264    rw [t2] at t1265    have hT : α1 * β2 = α2 * β1 := eq_of_add_neg_eq_zero ((K.mul_eq_zero t1).resolve_left he2)266    -- the chart: X = e2 a1 − e1 a2, Y = e2 b1 − e1 b2 solve the system with matrix boost(α1, β1)267    have s1 : e2 * (l * (a1 * α1 + b1 * β1)) = a2 * (l * (e1 * α1)) + b2 * (l * (e1 * β1)) := by268      rw [ha, ← hd', ← hc']; exact Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])269        (.mul (.var 8) (.add (.mul (.var 6) (.var 9)) (.mul (.var 7) (.var 10))))270        (.add (.mul (.var 6) (.mul (.var 8) (.var 9))) (.mul (.var 7) (.mul (.var 8) (.var 10)))) (by decide +kernel)271    have s2 : e2 * (l * (a1 * (ν * β1) + b1 * α1)) = a2 * (ν * (l * (e1 * β1))) + b2 * (l * (e1 * α1)) := by272      rw [hb, ← hd', ← hc']; exact Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])273        (.mul (.var 8) (.add (.mul (.var 6) (.mul (.var 11) (.var 10))) (.mul (.var 7) (.var 9))))274        (.add (.mul (.var 6) (.mul (.var 11) (.mul (.var 8) (.var 10)))) (.mul (.var 7) (.mul (.var 8) (.var 9)))) (by decide +kernel)275    have u1 : l * ((e2 * a1 + -(e1 * a2)) * α1 + (e2 * b1 + -(e1 * b2)) * β1) =276        e2 * (l * (a1 * α1 + b1 * β1)) + -(a2 * (l * (e1 * α1)) + b2 * (l * (e1 * β1))) := Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])277        (.mul (.var 0) (.add (.mul (.add (.mul (.var 8) (.var 1)) (.neg (.mul (.var 3) (.var 6)))) (.var 4)) (.mul (.add (.mul (.var 8) (.var 2)) (.neg (.mul (.var 3) (.var 7)))) (.var 5))))278        (.add (.mul (.var 8) (.mul (.var 0) (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 5))))) (.neg (.add (.mul (.var 6) (.mul (.var 0) (.mul (.var 3) (.var 4)))) (.mul (.var 7) (.mul (.var 0) (.mul (.var 3) (.var 5))))))) (by decide +kernel)279    have u2 : l * ((e2 * a1 + -(e1 * a2)) * (ν * β1) + (e2 * b1 + -(e1 * b2)) * α1) =280        e2 * (l * (a1 * (ν * β1) + b1 * α1)) + -(a2 * (ν * (l * (e1 * β1))) + b2 * (l * (e1 * α1))) := Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])281        (.mul (.var 0) (.add (.mul (.add (.mul (.var 8) (.var 1)) (.neg (.mul (.var 3) (.var 6)))) (.mul (.var 11) (.var 5))) (.mul (.add (.mul (.var 8) (.var 2)) (.neg (.mul (.var 3) (.var 7)))) (.var 4))))282        (.add (.mul (.var 8) (.mul (.var 0) (.add (.mul (.var 1) (.mul (.var 11) (.var 5))) (.mul (.var 2) (.var 4))))) (.neg (.add (.mul (.var 6) (.mul (.var 11) (.mul (.var 0) (.mul (.var 3) (.var 5))))) (.mul (.var 7) (.mul (.var 0) (.mul (.var 3) (.var 4))))))) (by decide +kernel)283    rw [s1, add_neg] at u1284    rw [s2, add_neg] at u2285    have v1 := (K.mul_eq_zero u1).resolve_left hl286    have v2 := (K.mul_eq_zero u2).resolve_left hl287    have w1 : (e2 * a1 + -(e1 * a2)) * (α1 * α1 + -(ν * (β1 * β1))) =288        α1 * ((e2 * a1 + -(e1 * a2)) * α1 + (e2 * b1 + -(e1 * b2)) * β1) +289        -(β1 * ((e2 * a1 + -(e1 * a2)) * (ν * β1) + (e2 * b1 + -(e1 * b2)) * α1)) := Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])290        (.mul (.add (.mul (.var 8) (.var 1)) (.neg (.mul (.var 3) (.var 6)))) (.add (.mul (.var 4) (.var 4)) (.neg (.mul (.var 11) (.mul (.var 5) (.var 5))))))291        (.add (.mul (.var 4) (.add (.mul (.add (.mul (.var 8) (.var 1)) (.neg (.mul (.var 3) (.var 6)))) (.var 4)) (.mul (.add (.mul (.var 8) (.var 2)) (.neg (.mul (.var 3) (.var 7)))) (.var 5)))) (.neg (.mul (.var 5) (.add (.mul (.add (.mul (.var 8) (.var 1)) (.neg (.mul (.var 3) (.var 6)))) (.mul (.var 11) (.var 5))) (.mul (.add (.mul (.var 8) (.var 2)) (.neg (.mul (.var 3) (.var 7)))) (.var 4)))))) (by decide +kernel)292    have w2 : (e2 * b1 + -(e1 * b2)) * (α1 * α1 + -(ν * (β1 * β1))) =293        α1 * ((e2 * a1 + -(e1 * a2)) * (ν * β1) + (e2 * b1 + -(e1 * b2)) * α1) +294        -(ν * β1 * ((e2 * a1 + -(e1 * a2)) * α1 + (e2 * b1 + -(e1 * b2)) * β1)) := Shell.Frame.RE.sound (Shell.Frame.look [l, a1, b1, e1, α1, β1, a2, b2, e2, α2, β2, ν])295        (.mul (.add (.mul (.var 8) (.var 2)) (.neg (.mul (.var 3) (.var 7)))) (.add (.mul (.var 4) (.var 4)) (.neg (.mul (.var 11) (.mul (.var 5) (.var 5))))))296        (.add (.mul (.var 4) (.add (.mul (.add (.mul (.var 8) (.var 1)) (.neg (.mul (.var 3) (.var 6)))) (.mul (.var 11) (.var 5))) (.mul (.add (.mul (.var 8) (.var 2)) (.neg (.mul (.var 3) (.var 7)))) (.var 4)))) (.neg (.mul (.mul (.var 11) (.var 5)) (.add (.mul (.add (.mul (.var 8) (.var 1)) (.neg (.mul (.var 3) (.var 6)))) (.var 4)) (.mul (.add (.mul (.var 8) (.var 2)) (.neg (.mul (.var 3) (.var 7)))) (.var 5)))))) (by decide +kernel)297    rw [v1, v2, mul_zero, mul_zero, neg_zero, add_zero] at w1298    rw [v1, v2, mul_zero, mul_zero, neg_zero, add_zero] at w2299    exact ⟨hT, eq_of_add_neg_eq_zero ((K.mul_eq_zero w1).resolve_right (hN hαβ)),300      eq_of_add_neg_eq_zero ((K.mul_eq_zero w2).resolve_right (hN hαβ))⟩301  · -- (5) the boost classes are the points of `ℙ¹`302    constructor303    · intro ⟨μ, _, h⟩304      have hα : α' = μ * α := congrArg M2.a h305      have hβ : β' = μ * β := congrArg M2.c h306      rw [hα, hβ, mul_left_comm, mul_assoc]307    · intro e308      match Shell.instDecidableEq α 0 with309      | .isFalse hα =>310        obtain ⟨s, hs⟩ := K.exists_inv hα311        have hb' : β' = α' * s * β :=312          calc β' = β' * (α * s) := by rw [hs, mul_one]313            _ = (α * β') * s := by rw [mul_left_comm, ← mul_assoc]314            _ = (α' * β) * s := by rw [e]315            _ = α' * s * β := by rw [mul_assoc, mul_comm β s, ← mul_assoc]316        have hμ : α' * s ≠ 0 := fun h0 => by317          have hα' : α' = 0 := by rw [← mul_one α', ← hs, mul_left_comm, h0, mul_zero]318          have hβ' : β' = 0 := by rw [hb', h0, zero_mul]319          exact h2.elim (fun h => h hα') (fun h => h hβ')320        refine ⟨α' * s, hμ, M2.ext' ?_ ?_ ?_ ?_⟩321        · show α' = α' * s * α; rw [mul_assoc, mul_comm s, hs, mul_one]322        · show ν * β' = α' * s * (ν * β); rw [hb', mul_left_comm]323        · show β' = α' * s * β; exact hb'324        · show α' = α' * s * α; rw [mul_assoc, mul_comm s, hs, mul_one]325      | .isTrue hα =>326        have hβ : β ≠ 0 := h1.resolve_left (fun h => h hα)327        have hα' : α' = 0 := by328          have : α' * β = 0 := by rw [← e, hα, zero_mul]329          exact (K.mul_eq_zero this).resolve_right hβ330        have hβ' : β' ≠ 0 := h2.resolve_left (fun h => h hα')331        obtain ⟨s, hs⟩ := K.exists_inv hβ332        refine ⟨β' * s, K.mul_ne_zero hβ' (fun h0 => K.one_ne_zero (by rw [← hs, h0, mul_zero])), M2.ext' ?_ ?_ ?_ ?_⟩333        · show α' = β' * s * α; rw [hα, hα', mul_zero]334        · show ν * β' = β' * s * (ν * β); rw [mul_left_comm, mul_assoc, mul_comm s, hs, mul_one]335        · show β' = β' * s * β; rw [mul_assoc, mul_comm s, hs, mul_one]336        · show α' = β' * s * α; rw [hα, hα', mul_zero]337  · -- (7) the spin cover338    refine ⟨M2.ext' rfl (mul_zero ν) rfl rfl, by rw [mul_zero, mul_zero, neg_zero, add_zero, neg_mul_neg, one_mul],339      by rw [neg_mul_neg, one_mul], fun α β a b e h hn => ?_, fun M N => M2.ext' ?_ ?_ ?_ ?_⟩340    · have hβ : β = 0 := congrArg M2.c h341      refine ⟨hβ, K.sq_eq_one ?_⟩342      rw [hβ, mul_zero, mul_zero, neg_zero, add_zero] at hn; exact hn343    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d])344        (.add (.mul (.mul (.neg .one) (.var 0)) (.mul (.neg .one) (.var 4))) (.mul (.mul (.neg .one) (.var 1)) (.mul (.neg .one) (.var 6))))345        (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 6))) (by decide +kernel)346    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d])347        (.add (.mul (.mul (.neg .one) (.var 0)) (.mul (.neg .one) (.var 5))) (.mul (.mul (.neg .one) (.var 1)) (.mul (.neg .one) (.var 7))))348        (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 7))) (by decide +kernel)349    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d])350        (.add (.mul (.mul (.neg .one) (.var 2)) (.mul (.neg .one) (.var 4))) (.mul (.mul (.neg .one) (.var 3)) (.mul (.neg .one) (.var 6))))351        (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) (.var 6))) (by decide +kernel)352    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d])353        (.add (.mul (.mul (.neg .one) (.var 2)) (.mul (.neg .one) (.var 5))) (.mul (.mul (.neg .one) (.var 3)) (.mul (.neg .one) (.var 7))))354        (.add (.mul (.var 2) (.var 5)) (.mul (.var 3) (.var 7))) (by decide +kernel)355356/-- 38:A7, 38:A9 — on a frame (`Frame.fld`): `Fld.hopf_section`. -/357theorem hopf_section (F : Frame p κ g) {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) :358    (∀ α β x y : Shell p, β ≠ 0 → (x ≠ 0 ∨ y ≠ 0) → ¬ PEq ((boost ν α β).act x y) (x, y)) ∧359    (∀ α β a b e l : Shell p, boost ν α β = M2.smul l (borel a b e) → β = 0) ∧360    (∀ M : M2 p, M.det ≠ 0 → ∃ N a b e α β : Shell p, N ≠ 0 ∧ a * e ≠ 0 ∧ (α ≠ 0 ∨ β ≠ 0) ∧361      M2.smul N M = (borel a b e).mul (boost ν α β)) ∧362    (∀ l a1 b1 e1 α1 β1 a2 b2 e2 α2 β2 : Shell p, l ≠ 0 → e2 ≠ 0 → (α1 ≠ 0 ∨ β1 ≠ 0) →363      M2.smul l ((borel a1 b1 e1).mul (boost ν α1 β1)) = (borel a2 b2 e2).mul (boost ν α2 β2) →364      α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) ∧365    (∀ α β α' β' : Shell p, (α ≠ 0 ∨ β ≠ 0) → (α' ≠ 0 ∨ β' ≠ 0) →366      ((∃ μ : Shell p, μ ≠ 0 ∧ boost ν α' β' = M2.smul μ (boost ν α β)) ↔ α * β' = α' * β)) ∧367    natCount (fun _ => True) p * natCount (fun b => b ≠ 0) p = p * (p - 1) ∧368    (boost ν (-1) 0 = borel (-1) 0 (-1) ∧ (-1 : Shell p) * -1 + -(ν * (0 * 0)) = 1 ∧ (-1 : Shell p) * -1 = 1 ∧369      (∀ α β a b e : Shell p, boost ν α β = borel a b e → α * α + -(ν * (β * β)) = 1 → β = 0 ∧ (α = 1 ∨ α = -1)) ∧370      ∀ M N : M2 p, (M2.smul (-1) M).mul (M2.smul (-1) N) = M.mul N) :=371  F.fld.hopf_section hν372373/-- 38:A7, 38:A9, 38:X4, 00:C19 — the fibration counted by representatives. Every Borel class (an upper-triangular `[[a, b], [0, e]]`,374`a e ≠ 0`, up to a nonzero scalar) has exactly one representative `[[i, j], [0, 1]]` with `i, j < p` and `i ≠ 0`, and375these number `p (p − 1)`. Every boost class has exactly one representative among `[[i, ν], [1, i]]` (`i < p`) and the376identity `[[1, 0], [0, 1]]`, and these number `p + 1`. With the factorisation (`hopf_section`), the frames are377`p (p − 1)` fibres of `p + 1`. -/378theorem Fld.hopf_counts (K : Fld p) (ν : Shell p) :379    (∀ a b e : Shell p, a * e ≠ 0 → ∃ i j : Nat, i < p ∧ j < p ∧ i ≠ 0 ∧380      ∃ l : Shell p, l ≠ 0 ∧ M2.smul l (borel a b e) = borel (ofNat i) (ofNat j) 1) ∧381    (∀ i j i' j' : Nat, i < p → j < p → i' < p → j' < p → ∀ l : Shell p,382      M2.smul l (borel (ofNat i) (ofNat j) 1) = borel (ofNat i') (ofNat j') 1 → i = i' ∧ j = j') ∧383    natCount (fun _ => True) p * natCount (fun b => b ≠ 0) p = p * (p - 1) ∧384    (∀ α β : Shell p, (α ≠ 0 ∨ β ≠ 0) →385      (∃ i : Nat, i < p ∧ ∃ μ : Shell p, μ ≠ 0 ∧ M2.smul μ (boost ν α β) = boost ν (ofNat i) 1) ∨386      (∃ μ : Shell p, μ ≠ 0 ∧ M2.smul μ (boost ν α β) = boost ν 1 0)) ∧387    (∀ i i' : Nat, i < p → i' < p → ∀ μ : Shell p, M2.smul μ (boost ν (ofNat i) 1) = boost ν (ofNat i') 1 → i = i') ∧388    (∀ i : Nat, ∀ μ : Shell p, μ ≠ 0 → M2.smul μ (boost ν (ofNat i) 1) ≠ boost ν 1 0) ∧389    (∀ i : Nat, ∀ μ : Shell p, M2.smul μ (boost ν 1 0) ≠ boost ν (ofNat i) 1) ∧390    natCount (fun _ => True) p + 1 = p + 1 := by391  have hT : ∀ n, natCount (fun _ => True) n = n := fun n => by392    induction n with393    | zero => rfl394    | succ n ih => show natCount (fun _ => True) n + (if True then 1 else 0) = n + 1; rw [ih, ite_eq_left trivial]395  have ofNat_inj : ∀ {i j : Nat}, i < p → j < p → (ofNat i : Shell p) = ofNat j → i = j := fun hi hj h => by396    have := val_injective h397    rw [val_ofNat, val_ofNat, FRC.Nat.mod_eq_of_lt hi, FRC.Nat.mod_eq_of_lt hj] at this398    exact this399  have hval : ∀ x : Shell p, x ≠ 0 → x.val ≠ 0 := fun x hx h0 => hx (by rw [← ofNat_val x, h0]; rfl)400  have hl1 : ∀ l : Shell p, l * 1 = 1 → l = 1 := fun l h => by rw [mul_one] at h; exact h401  -- the boost scaled: `μ · [[α, νβ], [β, α]] = [[μα, ν(μβ)], [μβ, μα]]`402  have hsb : ∀ μ α β : Shell p, M2.smul μ (boost ν α β) = boost ν (μ * α) (μ * β) := fun μ α β =>403    M2.ext' rfl (by show μ * (ν * β) = ν * (μ * β); rw [mul_left_comm]) rfl rfl404  refine ⟨fun a b e hae => ?_, fun i j i' j' hi hj hi' hj' l h => ?_, frame_count, fun α β hαβ => ?_,405    fun i i' hi hi' μ h => ?_, fun i μ hμ h => ?_, fun i μ h => ?_, by rw [hT]⟩406  · have he : e ≠ 0 := fun h0 => hae (by rw [h0, mul_zero])407    have ha : a ≠ 0 := fun h0 => hae (by rw [h0, zero_mul])408    obtain ⟨y, hy⟩ := K.exists_inv he409    have hy0 : y ≠ 0 := fun h0 => K.one_ne_zero (by rw [← hy, h0, mul_zero])410    refine ⟨(y * a).val, (y * b).val, (y * a).lt, (y * b).lt, hval _ (K.mul_ne_zero hy0 ha), y, hy0, ?_⟩411    rw [ofNat_val, ofNat_val]412    exact M2.ext' rfl rfl (mul_zero y) (by show y * e = 1; rw [mul_comm]; exact hy)413  · have hl : l = 1 := hl1 l (M2.ext'_d h)414    rw [hl] at h415    have ha : 1 * ofNat i = (ofNat i' : Shell p) := M2.ext'_a h416    have hb : 1 * ofNat j = (ofNat j' : Shell p) := M2.ext'_b h417    rw [one_mul] at ha hb418    exact ⟨ofNat_inj hi hi' ha, ofNat_inj hj hj' hb⟩419  · match Shell.instDecidableEq β 0 with420    | .isFalse hβ =>421      obtain ⟨y, hy⟩ := K.exists_inv hβ422      have hy0 : y ≠ 0 := fun h0 => K.one_ne_zero (by rw [← hy, h0, mul_zero])423      refine .inl ⟨(y * α).val, (y * α).lt, y, hy0, ?_⟩424      rw [hsb, ofNat_val, mul_comm y β, hy]425    | .isTrue hβ =>426      have hα : α ≠ 0 := match hαβ with | .inl h => h | .inr h => absurd hβ h427      obtain ⟨y, hy⟩ := K.exists_inv hα428      have hy0 : y ≠ 0 := fun h0 => K.one_ne_zero (by rw [← hy, h0, mul_zero])429      refine .inr ⟨y, hy0, ?_⟩430      rw [hsb, hβ, mul_zero, mul_comm y α, hy]431  · rw [hsb] at h432    have hμ : μ = 1 := hl1 μ (M2.ext'_c h)433    rw [hμ, one_mul] at h434    exact ofNat_inj hi hi' (M2.ext'_a h)435  · rw [hsb] at h436    exact hμ (by have := M2.ext'_c h; rwa [mul_one] at this)437  · rw [hsb, mul_zero] at h438    exact K.one_ne_zero (M2.ext'_c h).symm439440441/-- 38:A7, 38:A9, 38:X4, 00:C19 — on a frame (`Frame.fld`): `Fld.hopf_counts`. -/442theorem hopf_counts (F : Frame p κ g) (ν : Shell p) :443    (∀ a b e : Shell p, a * e ≠ 0 → ∃ i j : Nat, i < p ∧ j < p ∧ i ≠ 0 ∧444      ∃ l : Shell p, l ≠ 0 ∧ M2.smul l (borel a b e) = borel (ofNat i) (ofNat j) 1) ∧445    (∀ i j i' j' : Nat, i < p → j < p → i' < p → j' < p → ∀ l : Shell p,446      M2.smul l (borel (ofNat i) (ofNat j) 1) = borel (ofNat i') (ofNat j') 1 → i = i' ∧ j = j') ∧447    natCount (fun _ => True) p * natCount (fun b => b ≠ 0) p = p * (p - 1) ∧448    (∀ α β : Shell p, (α ≠ 0 ∨ β ≠ 0) →449      (∃ i : Nat, i < p ∧ ∃ μ : Shell p, μ ≠ 0 ∧ M2.smul μ (boost ν α β) = boost ν (ofNat i) 1) ∨450      (∃ μ : Shell p, μ ≠ 0 ∧ M2.smul μ (boost ν α β) = boost ν 1 0)) ∧451    (∀ i i' : Nat, i < p → i' < p → ∀ μ : Shell p, M2.smul μ (boost ν (ofNat i) 1) = boost ν (ofNat i') 1 → i = i') ∧452    (∀ i : Nat, ∀ μ : Shell p, μ ≠ 0 → M2.smul μ (boost ν (ofNat i) 1) ≠ boost ν 1 0) ∧453    (∀ i : Nat, ∀ μ : Shell p, M2.smul μ (boost ν 1 0) ≠ boost ν (ofNat i) 1) ∧454    natCount (fun _ => True) p + 1 = p + 1 :=455  F.fld.hopf_counts ν456457/-! ## 38:A9, 38:X4, 38:B6: the frame triple and the split fibration (12 October 2026)458459The adjugate `adj M = [[d, −b], [−c, a]]` with `M · adj M = adj M · M = det M · I`; the frame triple460`G ≅ ℙ¹ × B`: every invertible `M` factors as (boost carrying the horizon to its direction `M·[1 : 0]`) × (cone chart),461uniquely up to scalars (`frame_triple`); the split fibration by the unit `i = diag(r, −r)`, `r = g^κ`, `r² = −1`: the462centraliser of `i` is the diagonal torus inside the Borel, `i` is not scalar, the circle `x² + y² = 1` is the torus's463norm-one part, the conjugates of `i` fill the trace-zero quadric `a² + bc = −1` and every point of it is reached, and464the quadric is the unit sphere `x² + y² + z² = 1` under a linear change of chart (`unit_split`); the sphere's465`p(p + 1)` points are the gravity theme's `Grav.sphere_area_rung`, the circle's `p − 1` its `conic_count`. -/466467namespace M2468469/-- The adjugate `[[d, −b], [−c, a]]`. -/470def adj (M : M2 p) : M2 p := ⟨M.d, -M.b, -M.c, M.a⟩471472/-- `M · adj M = det M · I`. -/473theorem mul_adj (M : M2 p) : M.mul M.adj = ⟨M.det, 0, 0, M.det⟩ :=474  ext' (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.var 0) (.var 3)) (.mul (.var 1) (.neg (.var 2)))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.var 0) (.neg (.var 1))) (.mul (.var 1) (.var 0))) .zero (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.var 2) (.var 3)) (.mul (.var 3) (.neg (.var 2)))) .zero (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.var 2) (.neg (.var 1))) (.mul (.var 3) (.var 0))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (by decide +kernel))475476/-- `adj M · M = det M · I`. -/477theorem adj_mul (M : M2 p) : M.adj.mul M = ⟨M.det, 0, 0, M.det⟩ :=478  ext' (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.var 3) (.var 0)) (.mul (.neg (.var 1)) (.var 2))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.var 3) (.var 1)) (.mul (.neg (.var 1)) (.var 3))) .zero (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.neg (.var 2)) (.var 0)) (.mul (.var 0) (.var 2))) .zero (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d]) (.add (.mul (.neg (.var 2)) (.var 1)) (.mul (.var 0) (.var 3))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (by decide +kernel))479480theorem mul_assoc' (M N K : M2 p) : (M.mul N).mul K = M.mul (N.mul K) :=481  ext' (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d, K.a, K.b, K.c, K.d]) (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 6))) (.var 8)) (.mul (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 7))) (.var 10))) (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 8)) (.mul (.var 5) (.var 10)))) (.mul (.var 1) (.add (.mul (.var 6) (.var 8)) (.mul (.var 7) (.var 10))))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d, K.a, K.b, K.c, K.d]) (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) (.var 6))) (.var 9)) (.mul (.add (.mul (.var 0) (.var 5)) (.mul (.var 1) (.var 7))) (.var 11))) (.add (.mul (.var 0) (.add (.mul (.var 4) (.var 9)) (.mul (.var 5) (.var 11)))) (.mul (.var 1) (.add (.mul (.var 6) (.var 9)) (.mul (.var 7) (.var 11))))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d, K.a, K.b, K.c, K.d]) (.add (.mul (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) (.var 6))) (.var 8)) (.mul (.add (.mul (.var 2) (.var 5)) (.mul (.var 3) (.var 7))) (.var 10))) (.add (.mul (.var 2) (.add (.mul (.var 4) (.var 8)) (.mul (.var 5) (.var 10)))) (.mul (.var 3) (.add (.mul (.var 6) (.var 8)) (.mul (.var 7) (.var 10))))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d, K.a, K.b, K.c, K.d]) (.add (.mul (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) (.var 6))) (.var 9)) (.mul (.add (.mul (.var 2) (.var 5)) (.mul (.var 3) (.var 7))) (.var 11))) (.add (.mul (.var 2) (.add (.mul (.var 4) (.var 9)) (.mul (.var 5) (.var 11)))) (.mul (.var 3) (.add (.mul (.var 6) (.var 9)) (.mul (.var 7) (.var 11))))) (by decide +kernel))482483theorem smul_mul (l : Shell p) (M N : M2 p) : (smul l M).mul N = smul l (M.mul N) :=484  ext' (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.mul (.var 0) (.var 1)) (.var 5)) (.mul (.mul (.var 0) (.var 2)) (.var 7))) (.mul (.var 0) (.add (.mul (.var 1) (.var 5)) (.mul (.var 2) (.var 7)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.mul (.var 0) (.var 1)) (.var 6)) (.mul (.mul (.var 0) (.var 2)) (.var 8))) (.mul (.var 0) (.add (.mul (.var 1) (.var 6)) (.mul (.var 2) (.var 8)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.mul (.var 0) (.var 3)) (.var 5)) (.mul (.mul (.var 0) (.var 4)) (.var 7))) (.mul (.var 0) (.add (.mul (.var 3) (.var 5)) (.mul (.var 4) (.var 7)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.mul (.var 0) (.var 3)) (.var 6)) (.mul (.mul (.var 0) (.var 4)) (.var 8))) (.mul (.var 0) (.add (.mul (.var 3) (.var 6)) (.mul (.var 4) (.var 8)))) (by decide +kernel))485486theorem mul_smul (l : Shell p) (M N : M2 p) : M.mul (smul l N) = smul l (M.mul N) :=487  ext' (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.var 1) (.mul (.var 0) (.var 5))) (.mul (.var 2) (.mul (.var 0) (.var 7)))) (.mul (.var 0) (.add (.mul (.var 1) (.var 5)) (.mul (.var 2) (.var 7)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.var 1) (.mul (.var 0) (.var 6))) (.mul (.var 2) (.mul (.var 0) (.var 8)))) (.mul (.var 0) (.add (.mul (.var 1) (.var 6)) (.mul (.var 2) (.var 8)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.var 3) (.mul (.var 0) (.var 5))) (.mul (.var 4) (.mul (.var 0) (.var 7)))) (.mul (.var 0) (.add (.mul (.var 3) (.var 5)) (.mul (.var 4) (.var 7)))) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d, N.a, N.b, N.c, N.d]) (.add (.mul (.var 3) (.mul (.var 0) (.var 6))) (.mul (.var 4) (.mul (.var 0) (.var 8)))) (.mul (.var 0) (.add (.mul (.var 3) (.var 6)) (.mul (.var 4) (.var 8)))) (by decide +kernel))488489/-- A scalar matrix acts as the scalar. -/490theorem diag_mul (l : Shell p) (M : M2 p) : (⟨l, 0, 0, l⟩ : M2 p).mul M = smul l M :=491  ext' (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul (.var 0) (.var 1)) (.mul .zero (.var 3))) (.mul (.var 0) (.var 1)) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul (.var 0) (.var 2)) (.mul .zero (.var 4))) (.mul (.var 0) (.var 2)) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul .zero (.var 1)) (.mul (.var 0) (.var 3))) (.mul (.var 0) (.var 3)) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul .zero (.var 2)) (.mul (.var 0) (.var 4))) (.mul (.var 0) (.var 4)) (by decide +kernel))492493494/-- A scalar matrix on the right acts as the scalar. -/495theorem mul_diag (l : Shell p) (M : M2 p) : M.mul ⟨l, 0, 0, l⟩ = smul l M :=496  ext' (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul (.var 1) (.var 0)) (.mul (.var 2) .zero)) (.mul (.var 0) (.var 1)) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul (.var 1) .zero) (.mul (.var 2) (.var 0))) (.mul (.var 0) (.var 2)) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul (.var 3) (.var 0)) (.mul (.var 4) .zero)) (.mul (.var 0) (.var 3)) (by decide +kernel)) (Shell.Frame.RE.sound (Shell.Frame.look [l, M.a, M.b, M.c, M.d]) (.add (.mul (.var 3) .zero) (.mul (.var 4) (.var 0))) (.mul (.var 0) (.var 4)) (by decide +kernel))497498/-- A nonzero scalar cancels. -/499theorem smul_cancel (K : Fld p) {l : Shell p} (hl : l ≠ 0) {A B : M2 p} (h : smul l A = smul l B) : A = B :=500  ext' (K.mul_left_cancel hl (ext'_a h)) (K.mul_left_cancel hl (ext'_b h)) (K.mul_left_cancel hl (ext'_c h))501    (K.mul_left_cancel hl (ext'_d h))502503end M2504505/-- 38:A9, 38:X4 — **the frame triple** (Theorem *The two fibrations and the frame triple*, the master's C22). On a506frame with `ν` a nonsquare: (1) an invertible `M` has a nonzero first column, its direction `M·[1 : 0] = [a : c]` is the507boost `[[a, νc], [c, a]]`'s direction, that boost has nonzero norm `N = a² − νc²`, and `N·M = boost(a, c) · borel(N, ab − νcd, det M)`:508every frame is (boost carrying the horizon to its direction) × (cone chart); (2) the cone charts fix the horizon;509(3) the factorisation is unique up to scalars — two factorisations of proportional frames have the same boost class and510the same chart class. With `hopf_counts` (`p + 1` boost classes, `p(p − 1)` charts) the frames number511`(p + 1)·p·(p − 1)`: one direction, one shell cell, one drive phase. -/512theorem Fld.frame_triple (K : Fld p) {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) :513    (∀ M : M2 p, M.det ≠ 0 → (M.a ≠ 0 ∨ M.c ≠ 0) ∧ M.act 1 0 = (M.a, M.c) ∧ (boost ν M.a M.c).act 1 0 = (M.a, M.c) ∧514      M.a * M.a + -(ν * (M.c * M.c)) ≠ 0 ∧515      M2.smul (M.a * M.a + -(ν * (M.c * M.c))) M =516        (boost ν M.a M.c).mul (borel (M.a * M.a + -(ν * (M.c * M.c))) (M.a * M.b + -(ν * (M.c * M.d))) M.det)) ∧517    (∀ a b e : Shell p, (borel a b e).act 1 0 = (a, 0)) ∧518    (∀ l α1 β1 a1 b1 e1 α2 β2 a2 b2 e2 : Shell p, l ≠ 0 → a1 ≠ 0 → a2 ≠ 0 → (α1 ≠ 0 ∨ β1 ≠ 0) →519      M2.smul l ((boost ν α1 β1).mul (borel a1 b1 e1)) = (boost ν α2 β2).mul (borel a2 b2 e2) →520      α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) := by521  have hN : ∀ {x y : Shell p}, (x ≠ 0 ∨ y ≠ 0) → x * x + -(ν * (y * y)) ≠ 0 := fun hxy => K.norm_ne_zero hν hxy522  refine ⟨fun M hM => ?_, fun a b e => ?_, fun l α1 β1 a1 b1 e1 α2 β2 a2 b2 e2 hl ha1 ha2 hαβ h => ?_⟩523  · have hac : M.a ≠ 0 ∨ M.c ≠ 0 := by524      match Shell.instDecidableEq M.a 0, Shell.instDecidableEq M.c 0 with525      | .isTrue ha, .isTrue hc =>526        exact absurd (show M.det = 0 by527          show M.a * M.d + -(M.b * M.c) = 0; rw [ha, hc, zero_mul, mul_zero, neg_zero, add_zero]) hM528      | .isFalse ha, _ => exact .inl ha529      | _, .isFalse hc => exact .inr hc530    refine ⟨hac, ?_, ?_, hN hac, M2.ext' ?_ ?_ ?_ ?_⟩531    · show (M.a * 1 + M.b * 0, M.c * 1 + M.d * 0) = (M.a, M.c)532      rw [mul_one, mul_zero, add_zero, mul_one, mul_zero, add_zero]533    · show (M.a * 1 + ν * M.c * 0, M.c * 1 + M.a * 0) = (M.a, M.c)534      rw [mul_one, mul_zero, add_zero, mul_one, mul_zero, add_zero]535    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν]) (.mul (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 0)) (.add (.mul (.var 0) (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2)))))) (.mul (.mul (.var 4) (.var 2)) .zero)) (by decide +kernel)536    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν]) (.mul (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 1)) (.add (.mul (.var 0) (.add (.mul (.var 0) (.var 1)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 3)))))) (.mul (.mul (.var 4) (.var 2)) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))))) (by decide +kernel)537    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν]) (.mul (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 2)) (.add (.mul (.var 2) (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2)))))) (.mul (.var 0) .zero)) (by decide +kernel)538    · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, ν]) (.mul (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 2))))) (.var 3)) (.add (.mul (.var 2) (.add (.mul (.var 0) (.var 1)) (.neg (.mul (.var 4) (.mul (.var 2) (.var 3)))))) (.mul (.var 0) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))))) (by decide +kernel)539  · show (a * 1 + b * 0, 0 * 1 + e * 0) = (a, 0)540    rw [mul_one, mul_zero, add_zero, zero_mul, mul_zero, add_zero]541  · have ha : l * (α1 * a1 + ν * β1 * 0) = α2 * a2 + ν * β2 * 0 := congrArg M2.a h542    have hb : l * (α1 * b1 + ν * β1 * e1) = α2 * b2 + ν * β2 * e2 := congrArg M2.b h543    have hc : l * (β1 * a1 + α1 * 0) = β2 * a2 + α2 * 0 := congrArg M2.c h544    have hd : l * (β1 * b1 + α1 * e1) = β2 * b2 + α2 * e2 := congrArg M2.d h545    rw [mul_zero, add_zero, mul_zero, add_zero] at ha hc546    -- the boost class: `(l a1)(α1 β2 − α2 β1) = 0`547    have t1 : (l * a1) * (α1 * β2 + -(α2 * β1)) = (l * (α1 * a1)) * β2 + -(α2 * (l * (β1 * a1))) := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.mul (.mul (.var 0) (.var 3)) (.add (.mul (.var 1) (.var 7)) (.neg (.mul (.var 6) (.var 2))))) (.add (.mul (.mul (.var 0) (.mul (.var 1) (.var 3))) (.var 7)) (.neg (.mul (.var 6) (.mul (.var 0) (.mul (.var 2) (.var 3)))))) (by decide +kernel)548    rw [ha, hc] at t1549    have t2 : α2 * a2 * β2 + -(α2 * (β2 * a2)) = 0 := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.add (.mul (.mul (.var 6) (.var 8)) (.var 7)) (.neg (.mul (.var 6) (.mul (.var 7) (.var 8))))) .zero (by decide +kernel)550    rw [t2] at t1551    have hT : α1 * β2 = α2 * β1 := eq_of_add_neg_eq_zero ((K.mul_eq_zero t1).resolve_left (K.mul_ne_zero hl ha1))552    -- the chart class: scale the `b`, `d` rows by `a2` and read the boost classes equal553    have s1 : a2 * (α2 * b2 + ν * β2 * e2) = l * (a1 * (α1 * b2 + ν * β1 * e2)) := by554      have e : a2 * (α2 * b2 + ν * β2 * e2) = (α2 * a2) * b2 + ν * ((β2 * a2) * e2) := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.mul (.var 8) (.add (.mul (.var 6) (.var 9)) (.mul (.mul (.var 11) (.var 7)) (.var 10)))) (.add (.mul (.mul (.var 6) (.var 8)) (.var 9)) (.mul (.var 11) (.mul (.mul (.var 7) (.var 8)) (.var 10)))) (by decide +kernel)555      rw [e, ← ha, ← hc]; exact Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.add (.mul (.mul (.var 0) (.mul (.var 1) (.var 3))) (.var 9)) (.mul (.var 11) (.mul (.mul (.var 0) (.mul (.var 2) (.var 3))) (.var 10)))) (.mul (.var 0) (.mul (.var 3) (.add (.mul (.var 1) (.var 9)) (.mul (.mul (.var 11) (.var 2)) (.var 10))))) (by decide +kernel)556    have s2 : a2 * (β2 * b2 + α2 * e2) = l * (a1 * (β1 * b2 + α1 * e2)) := by557      have e : a2 * (β2 * b2 + α2 * e2) = (β2 * a2) * b2 + (α2 * a2) * e2 := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.mul (.var 8) (.add (.mul (.var 7) (.var 9)) (.mul (.var 6) (.var 10)))) (.add (.mul (.mul (.var 7) (.var 8)) (.var 9)) (.mul (.mul (.var 6) (.var 8)) (.var 10))) (by decide +kernel)558      rw [e, ← ha, ← hc]; exact Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.add (.mul (.mul (.var 0) (.mul (.var 2) (.var 3))) (.var 9)) (.mul (.mul (.var 0) (.mul (.var 1) (.var 3))) (.var 10))) (.mul (.var 0) (.mul (.var 3) (.add (.mul (.var 2) (.var 9)) (.mul (.var 1) (.var 10))))) (by decide +kernel)559    have X1 : a2*(α1*b1 + ν*β1*e1) = a1*(α1*b2 + ν*β1*e2) := by560      have e : l * (a2*(α1*b1 + ν*β1*e1)) = a2 * (l * (α1 * b1 + ν * β1 * e1)) := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.mul (.var 0) (.mul (.var 8) (.add (.mul (.var 1) (.var 4)) (.mul (.mul (.var 11) (.var 2)) (.var 5))))) (.mul (.var 8) (.mul (.var 0) (.add (.mul (.var 1) (.var 4)) (.mul (.mul (.var 11) (.var 2)) (.var 5))))) (by decide +kernel)561      rw [hb, s1] at e562      exact K.mul_left_cancel hl e563    have X2 : a2*(β1*b1 + α1*e1) = a1*(β1*b2 + α1*e2) := by564      have e : l * (a2*(β1*b1 + α1*e1)) = a2 * (l * (β1 * b1 + α1 * e1)) := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.mul (.var 0) (.mul (.var 8) (.add (.mul (.var 2) (.var 4)) (.mul (.var 1) (.var 5))))) (.mul (.var 8) (.mul (.var 0) (.add (.mul (.var 2) (.var 4)) (.mul (.var 1) (.var 5))))) (by decide +kernel)565      rw [hd, s2] at e566      exact K.mul_left_cancel hl e567    -- invert the boost: `N(α1, β1) ≠ 0`568    have w1 : (a2 * b1 + -(a1 * b2)) * (α1*α1 + -(ν*(β1*β1))) = α1 * (a2*(α1*b1 + ν*β1*e1) + -(a1*(α1*b2 + ν*β1*e2))) + -(ν * β1 * (a2*(β1*b1 + α1*e1) + -(a1*(β1*b2 + α1*e2)))) := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.mul (.add (.mul (.var 8) (.var 4)) (.neg (.mul (.var 3) (.var 9)))) (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 11) (.mul (.var 2) (.var 2)))))) (.add (.mul (.var 1) (.add (.mul (.var 8) (.add (.mul (.var 1) (.var 4)) (.mul (.mul (.var 11) (.var 2)) (.var 5)))) (.neg (.mul (.var 3) (.add (.mul (.var 1) (.var 9)) (.mul (.mul (.var 11) (.var 2)) (.var 10))))))) (.neg (.mul (.mul (.var 11) (.var 2)) (.add (.mul (.var 8) (.add (.mul (.var 2) (.var 4)) (.mul (.var 1) (.var 5)))) (.neg (.mul (.var 3) (.add (.mul (.var 2) (.var 9)) (.mul (.var 1) (.var 10))))))))) (by decide +kernel)569    have w2 : (a2 * e1 + -(a1 * e2)) * (α1*α1 + -(ν*(β1*β1))) = α1 * (a2*(β1*b1 + α1*e1) + -(a1*(β1*b2 + α1*e2))) + -(β1 * (a2*(α1*b1 + ν*β1*e1) + -(a1*(α1*b2 + ν*β1*e2)))) := Shell.Frame.RE.sound (Shell.Frame.look [l, α1, β1, a1, b1, e1, α2, β2, a2, b2, e2, ν]) (.mul (.add (.mul (.var 8) (.var 5)) (.neg (.mul (.var 3) (.var 10)))) (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 11) (.mul (.var 2) (.var 2)))))) (.add (.mul (.var 1) (.add (.mul (.var 8) (.add (.mul (.var 2) (.var 4)) (.mul (.var 1) (.var 5)))) (.neg (.mul (.var 3) (.add (.mul (.var 2) (.var 9)) (.mul (.var 1) (.var 10))))))) (.neg (.mul (.var 2) (.add (.mul (.var 8) (.add (.mul (.var 1) (.var 4)) (.mul (.mul (.var 11) (.var 2)) (.var 5)))) (.neg (.mul (.var 3) (.add (.mul (.var 1) (.var 9)) (.mul (.mul (.var 11) (.var 2)) (.var 10))))))))) (by decide +kernel)570    rw [X1, X2, add_neg, add_neg, mul_zero, mul_zero, neg_zero, add_zero] at w1 w2571    have hB : a2 * b1 = a1 * b2 := eq_of_add_neg_eq_zero ((K.mul_eq_zero w1).resolve_right (hN hαβ))572    have hE : a2 * e1 = a1 * e2 := eq_of_add_neg_eq_zero ((K.mul_eq_zero w2).resolve_right (hN hαβ))573    refine ⟨hT, by rw [mul_comm e2 a1, ← hE, mul_comm], ?_⟩574    apply K.mul_left_cancel ha2575    calc a2 * (e2 * b1) = e2 * (a2 * b1) := mul_left_comm a2 e2 b1576      _ = e2 * a1 * b2 := by rw [hB, mul_assoc]577      _ = a1 * e2 * b2 := by rw [mul_comm e2 a1]578      _ = a2 * e1 * b2 := by rw [hE]579      _ = a2 * (e1 * b2) := mul_assoc a2 e1 b2580581/-- 38:A9, 38:X4 — on a frame (`Frame.fld`): `Fld.frame_triple`. -/582theorem frame_triple (F : Frame p κ g) {ν : Shell p} (hν : ¬ ∃ y : Shell p, y * y = ν) :583    (∀ M : M2 p, M.det ≠ 0 → (M.a ≠ 0 ∨ M.c ≠ 0) ∧ M.act 1 0 = (M.a, M.c) ∧ (boost ν M.a M.c).act 1 0 = (M.a, M.c) ∧584      M.a * M.a + -(ν * (M.c * M.c)) ≠ 0 ∧585      M2.smul (M.a * M.a + -(ν * (M.c * M.c))) M =586        (boost ν M.a M.c).mul (borel (M.a * M.a + -(ν * (M.c * M.c))) (M.a * M.b + -(ν * (M.c * M.d))) M.det)) ∧587    (∀ a b e : Shell p, (borel a b e).act 1 0 = (a, 0)) ∧588    (∀ l α1 β1 a1 b1 e1 α2 β2 a2 b2 e2 : Shell p, l ≠ 0 → a1 ≠ 0 → a2 ≠ 0 → (α1 ≠ 0 ∨ β1 ≠ 0) →589      M2.smul l ((boost ν α1 β1).mul (borel a1 b1 e1)) = (boost ν α2 β2).mul (borel a2 b2 e2) →590      α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) :=591  F.fld.frame_triple hν592593/-- The split fibration (`unit_split` states it with the unit and the diagonal matrices named) by the unit `i = diag(r, −r)`, `r = g^κ`, `r² = −1`, on every frame594`p = 4κ + 1`: (1) a matrix commuting with `i` is diagonal — the centraliser is the diagonal torus, inside the Borel595(`diag(a, d) = borel a 0 d`); (2) every diagonal matrix commutes with `i`; (3) `i` is not scalar: the torus is split;596(4) the circle `x² + y² = 1` lands in the torus with determinant `1`, as `x + yi ↦ diag(x + ry, x − ry)`; (5) every597conjugate `M i adj(M)` is trace-zero with `a² + bc = −(det M)²`: the orbit lies in the quadric `a² + bc = −1` up to the598scalar; (6) every point of the quadric is reached: for `N` trace-zero with `a² + bc = −1` there is an invertible `M`599with `M i = N M`; (7) the quadric is the unit sphere `x² + y² + z² = 1` under `(x, y, z) ↦ (rx, y + rz, −(y − rz))`,600and back with `h = 2⁻¹`; (8) two frames over one point of the quadric differ by an element commuting with `i`: the601fibres of the conjugation map are the cosets of the centraliser, by (1). The sphere has `p(p + 1)` points602(`Grav.sphere_area_rung`) and the circle `p − 1` (`Grav.conic_count`). -/603theorem unit_split_let (F : Frame p κ g) :604    let r : Shell p := g ^ κ605    let I : M2 p := ⟨r, 0, 0, -r⟩606    (∀ M : M2 p, M.mul I = I.mul M → M.b = 0 ∧ M.c = 0) ∧607    (∀ a d : Shell p, (⟨a, 0, 0, d⟩ : M2 p).mul I = I.mul ⟨a, 0, 0, d⟩ ∧ (⟨a, 0, 0, d⟩ : M2 p) = borel a 0 d) ∧608    (∀ l : Shell p, I ≠ ⟨l, 0, 0, l⟩) ∧609    (∀ x y : Shell p, x * x + y * y = 1 → (⟨x + r * y, 0, 0, x + -(r * y)⟩ : M2 p).det = 1) ∧610    (∀ M : M2 p, ((M.mul I).mul M.adj).a + ((M.mul I).mul M.adj).d = 0 ∧611      ((M.mul I).mul M.adj).a * ((M.mul I).mul M.adj).a + ((M.mul I).mul M.adj).b * ((M.mul I).mul M.adj).c =612        -(M.det * M.det)) ∧613    (∀ N : M2 p, N.a + N.d = 0 → N.a * N.a + N.b * N.c = -1 → ∃ M : M2 p, M.det ≠ 0 ∧ M.mul I = N.mul M) ∧614    (∀ x y z : Shell p, x * x + y * y + z * z = 1 → (r * x) * (r * x) + (y + r * z) * (-(y + -(r * z))) = -1) ∧615    (∀ h : Shell p, (1 + 1) * h = 1 → ∀ a b c : Shell p, a * a + b * c = -1 →616      (-(r * a)) * (-(r * a)) + (h * (b + -c)) * (h * (b + -c)) + (-(h * (r * (b + c)))) * (-(h * (r * (b + c)))) = 1) ∧617    (∀ N M M' : M2 p, M'.det ≠ 0 → M.mul I = N.mul M → M'.mul I = N.mul M' →618      (M'.adj.mul M).mul I = I.mul (M'.adj.mul M)) := by619  intro r I620  have hr : r * r = -1 := by have e := (F.quarter_turn_order).1; rwa [pow_two] at e621  have hr0 : r ≠ 0 := F.pow_ne_zero κ622  have h2 : (1 : Shell p) + 1 ≠ 0 := by rw [← Frame.two_eq_one_add_one]; exact F.two_ne_zero623  have hm1 : (-1 : Shell p) ≠ 0 := fun e => F.one_ne_zero (by rw [← neg_neg (1 : Shell p), e, neg_zero])624  refine ⟨fun M hM => ?_, fun a d => ⟨M2.ext' ?_ ?_ ?_ ?_, rfl⟩, fun l hl => ?_, fun x y hxy => ?_, fun M => ⟨?_, ?_⟩,625    fun N ht hq => ?_, fun x y z hs => ?_, fun h hh a b c hq => ?_, fun N M M' hM' hM hM'' => ?_⟩626  · -- (1) the `b` and `c` entries of `M i − i M` are `−2 r b` and `2 r c`627    have eb : M.a * 0 + M.b * -r = r * M.b + 0 * M.d := congrArg M2.b hM628    have ec : M.c * r + M.d * 0 = 0 * M.a + -r * M.c := congrArg M2.c hM629    have ub : (1 + 1) * (r * M.b) = (r * M.b + 0 * M.d) + -(M.a * 0 + M.b * -r) := Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, r]) (.mul (.add .one .one) (.mul (.var 4) (.var 1))) (.add (.add (.mul (.var 4) (.var 1)) (.mul .zero (.var 3))) (.neg (.add (.mul (.var 0) .zero) (.mul (.var 1) (.neg (.var 4)))))) (by decide +kernel)630    have uc : (1 + 1) * (r * M.c) = (M.c * r + M.d * 0) + -(0 * M.a + -r * M.c) := Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, r]) (.mul (.add .one .one) (.mul (.var 4) (.var 2))) (.add (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) .zero)) (.neg (.add (.mul .zero (.var 0)) (.mul (.neg (.var 4)) (.var 2))))) (by decide +kernel)631    rw [← eb, add_neg] at ub632    rw [ec, add_neg] at uc633    exact ⟨(F.mul_eq_zero ((F.mul_eq_zero ub).resolve_left h2)).resolve_left hr0,634      (F.mul_eq_zero ((F.mul_eq_zero uc).resolve_left h2)).resolve_left hr0⟩635  · exact Shell.Frame.RE.sound (Shell.Frame.look [a, d, r]) (.add (.mul (.var 0) (.var 2)) (.mul .zero .zero)) (.add (.mul (.var 2) (.var 0)) (.mul .zero .zero)) (by decide +kernel)636  · exact Shell.Frame.RE.sound (Shell.Frame.look [a, d, r]) (.add (.mul (.var 0) .zero) (.mul .zero (.neg (.var 2)))) (.add (.mul (.var 2) .zero) (.mul .zero (.var 1))) (by decide +kernel)637  · exact Shell.Frame.RE.sound (Shell.Frame.look [a, d, r]) (.add (.mul .zero (.var 2)) (.mul (.var 1) .zero)) (.add (.mul .zero (.var 0)) (.mul (.neg (.var 2)) .zero)) (by decide +kernel)638  · exact Shell.Frame.RE.sound (Shell.Frame.look [a, d, r]) (.add (.mul .zero .zero) (.mul (.var 1) (.neg (.var 2)))) (.add (.mul .zero .zero) (.mul (.neg (.var 2)) (.var 1))) (by decide +kernel)639  · -- (3) `r = l = −r` forces `r = 0`640    have e1 : r = l := congrArg M2.a hl641    have e2 : -r = l := congrArg M2.d hl642    exact hr0 (F.eq_zero_of_eq_neg (e1.trans e2.symm))643  · -- (4) `(x + ry)(x − ry) = x² − r²y²`644    show (x + r * y) * (x + -(r * y)) + -(0 * 0) = 1645    have e : (x + r * y) * (x + -(r * y)) + -(0 * 0) + (r * r + 1) * (y * y) = x * x + y * y := Shell.Frame.RE.sound (Shell.Frame.look [x, y, r]) (.add (.add (.mul (.add (.var 0) (.mul (.var 2) (.var 1))) (.add (.var 0) (.neg (.mul (.var 2) (.var 1))))) (.neg (.mul .zero .zero))) (.mul (.add (.mul (.var 2) (.var 2)) .one) (.mul (.var 1) (.var 1)))) (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (by decide +kernel)646    rw [hr, neg_add, zero_mul (y * y), add_zero, hxy] at e647    exact e648  · exact Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, r]) (.add (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) .zero)) (.var 3)) (.mul (.add (.mul (.var 0) .zero) (.mul (.var 1) (.neg (.var 4)))) (.neg (.var 2)))) (.add (.mul (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) .zero)) (.neg (.var 1))) (.mul (.add (.mul (.var 2) .zero) (.mul (.var 3) (.neg (.var 4)))) (.var 0)))) .zero (by decide +kernel)649  · have e : ((M.mul I).mul M.adj).a * ((M.mul I).mul M.adj).a + ((M.mul I).mul M.adj).b * ((M.mul I).mul M.adj).c =650        (r * r + 1) * (M.det * M.det) + -(M.det * M.det) := Shell.Frame.RE.sound (Shell.Frame.look [M.a, M.b, M.c, M.d, r]) (.add (.mul (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) .zero)) (.var 3)) (.mul (.add (.mul (.var 0) .zero) (.mul (.var 1) (.neg (.var 4)))) (.neg (.var 2)))) (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) .zero)) (.var 3)) (.mul (.add (.mul (.var 0) .zero) (.mul (.var 1) (.neg (.var 4)))) (.neg (.var 2))))) (.mul (.add (.mul (.add (.mul (.var 0) (.var 4)) (.mul (.var 1) .zero)) (.neg (.var 1))) (.mul (.add (.mul (.var 0) .zero) (.mul (.var 1) (.neg (.var 4)))) (.var 0))) (.add (.mul (.add (.mul (.var 2) (.var 4)) (.mul (.var 3) .zero)) (.var 3)) (.mul (.add (.mul (.var 2) .zero) (.mul (.var 3) (.neg (.var 4)))) (.neg (.var 2)))))) (.add (.mul (.add (.mul (.var 4) (.var 4)) .one) (.mul (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))))) (.neg (.mul (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2)))) (.add (.mul (.var 0) (.var 3)) (.neg (.mul (.var 1) (.var 2))))))) (by decide +kernel)651    rw [e, hr, neg_add, zero_mul, zero_add]652  · -- (6) three cases: `b ≠ 0`; `b = 0` and `a = r`; `b = 0` and `a = −r`, with `w = (2r)⁻¹`653    have hd : N.d = -N.a := (neg_eq_of_add_eq_zero ht).symm654    obtain ⟨w, hw⟩ := F.exists_inv (F.mul_ne_zero h2 hr0)655    match Shell.instDecidableEq N.b 0 with656    | .isFalse hb =>657      refine ⟨⟨N.b, N.b, r + -N.a, -(r + N.a)⟩, ?_, M2.ext' ?_ ?_ ?_ ?_⟩658      · show N.b * -(r + N.a) + -(N.b * (r + -N.a)) ≠ 0659        have e : N.b * -(r + N.a) + -(N.b * (r + -N.a)) = -((1 + 1) * (N.b * r)) := Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul (.var 1) (.neg (.add (.var 4) (.var 0)))) (.neg (.mul (.var 1) (.add (.var 4) (.neg (.var 0)))))) (.neg (.mul (.add .one .one) (.mul (.var 1) (.var 4)))) (by decide +kernel)660        rw [e]661        intro h0662        have h1 : (1 + 1) * (N.b * r) = 0 := by rw [← neg_neg ((1 + 1) * (N.b * r)), h0, neg_zero]663        exact hr0 ((F.mul_eq_zero ((F.mul_eq_zero h1).resolve_left h2)).resolve_left hb)664      · exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul (.var 1) (.var 4)) (.mul (.var 1) .zero)) (.add (.mul (.var 0) (.var 1)) (.mul (.var 1) (.add (.var 4) (.neg (.var 0))))) (by decide +kernel)665      · exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul (.var 1) .zero) (.mul (.var 1) (.neg (.var 4)))) (.add (.mul (.var 0) (.var 1)) (.mul (.var 1) (.neg (.add (.var 4) (.var 0))))) (by decide +kernel)666      · show (r + -N.a) * r + -(r + N.a) * 0 = N.c * N.b + N.d * (r + -N.a)667        rw [hd]668        have e : (r + -N.a) * r + -(r + N.a) * 0 = N.c * N.b + -N.a * (r + -N.a) + (r * r + 1) + -(N.a * N.a + N.b * N.c + 1) := Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul (.add (.var 4) (.neg (.var 0))) (.var 4)) (.mul (.neg (.add (.var 4) (.var 0))) .zero)) (.add (.add (.add (.mul (.var 2) (.var 1)) (.mul (.neg (.var 0)) (.add (.var 4) (.neg (.var 0))))) (.add (.mul (.var 4) (.var 4)) .one)) (.neg (.add (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 2))) .one))) (by decide +kernel)669        rw [e, hr, hq, neg_add, add_zero, neg_zero, add_zero]670      · show (r + -N.a) * 0 + -(r + N.a) * -r = N.c * N.b + N.d * -(r + N.a)671        rw [hd]672        have e : (r + -N.a) * 0 + -(r + N.a) * -r = N.c * N.b + -N.a * -(r + N.a) + (r * r + 1) + -(N.a * N.a + N.b * N.c + 1) := Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul (.add (.var 4) (.neg (.var 0))) .zero) (.mul (.neg (.add (.var 4) (.var 0))) (.neg (.var 4)))) (.add (.add (.add (.mul (.var 2) (.var 1)) (.mul (.neg (.var 0)) (.neg (.add (.var 4) (.var 0))))) (.add (.mul (.var 4) (.var 4)) .one)) (.neg (.add (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 2))) .one))) (by decide +kernel)673        rw [e, hr, hq, neg_add, add_zero, neg_zero, add_zero]674    | .isTrue hb =>675      have ha2 : N.a * N.a = r * r := by rw [hr, ← hq, hb, zero_mul, add_zero]676      have hsq : (N.a + -r) * (N.a + r) = 0 := by677        have e : (N.a + -r) * (N.a + r) = N.a * N.a + -(r * r) := Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.mul (.add (.var 0) (.neg (.var 4))) (.add (.var 0) (.var 4))) (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.var 4) (.var 4)))) (by decide +kernel)678        rw [e, ha2, add_neg]679      match F.mul_eq_zero hsq with680      | .inl h1 =>681        have ha : N.a = r := eq_of_add_neg_eq_zero h1682        refine ⟨⟨1, 0, N.c * w, 1⟩, ?_, M2.ext' ?_ ?_ ?_ ?_⟩683        · show 1 * 1 + -(0 * (N.c * w)) ≠ 0684          rw [mul_one, zero_mul, neg_zero, add_zero]; exact F.one_ne_zero685        · show 1 * r + 0 * 0 = N.a * 1 + N.b * (N.c * w)686          rw [ha, hb]; exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul .one (.var 4)) (.mul .zero .zero)) (.add (.mul (.var 4) .one) (.mul .zero (.mul (.var 2) (.var 5)))) (by decide +kernel)687        · show 1 * 0 + 0 * -r = N.a * 0 + N.b * 1688          rw [hb]; exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul .one .zero) (.mul .zero (.neg (.var 4)))) (.add (.mul (.var 0) .zero) (.mul .zero .one)) (by decide +kernel)689        · show N.c * w * r + 1 * 0 = N.c * 1 + N.d * (N.c * w)690          rw [hd, ha]691          have e : N.c * w * r + 1 * 0 = N.c * 1 + -r * (N.c * w) + N.c * ((1 + 1) * r * w + -1) := Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul (.mul (.var 2) (.var 5)) (.var 4)) (.mul .one .zero)) (.add (.add (.mul (.var 2) .one) (.mul (.neg (.var 4)) (.mul (.var 2) (.var 5)))) (.mul (.var 2) (.add (.mul (.mul (.add .one .one) (.var 4)) (.var 5)) (.neg .one)))) (by decide +kernel)692          rw [e, hw, add_neg, mul_zero, add_zero]693        · show N.c * w * 0 + 1 * -r = N.c * 0 + N.d * 1694          rw [hd, ha]; exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul (.mul (.var 2) (.var 5)) .zero) (.mul .one (.neg (.var 4)))) (.add (.mul (.var 2) .zero) (.mul (.neg (.var 4)) .one)) (by decide +kernel)695      | .inr h1 =>696        have ha : N.a = -r := eq_neg_of_add_eq_zero h1697        refine ⟨⟨0, 1, 1, -(N.c * w)⟩, ?_, M2.ext' ?_ ?_ ?_ ?_⟩698        · show 0 * -(N.c * w) + -(1 * 1) ≠ 0699          rw [zero_mul, mul_one, zero_add]; exact hm1700        · show 0 * r + 1 * 0 = N.a * 0 + N.b * 1701          rw [ha, hb]; exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul .zero (.var 4)) (.mul .one .zero)) (.add (.mul (.neg (.var 4)) .zero) (.mul .zero .one)) (by decide +kernel)702        · show 0 * 0 + 1 * -r = N.a * 1 + N.b * -(N.c * w)703          rw [ha, hb]; exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul .zero .zero) (.mul .one (.neg (.var 4)))) (.add (.mul (.neg (.var 4)) .one) (.mul .zero (.neg (.mul (.var 2) (.var 5))))) (by decide +kernel)704        · show 1 * r + -(N.c * w) * 0 = N.c * 0 + N.d * 1705          rw [hd, ha]; exact Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul .one (.var 4)) (.mul (.neg (.mul (.var 2) (.var 5))) .zero)) (.add (.mul (.var 2) .zero) (.mul (.neg (.neg (.var 4))) .one)) (by decide +kernel)706        · show 1 * 0 + -(N.c * w) * -r = N.c * 1 + N.d * -(N.c * w)707          rw [hd, ha]708          have e : 1 * 0 + -(N.c * w) * -r = N.c * 1 + - -r * -(N.c * w) + N.c * ((1 + 1) * r * w + -1) := Shell.Frame.RE.sound (Shell.Frame.look [N.a, N.b, N.c, N.d, r, w]) (.add (.mul .one .zero) (.mul (.neg (.mul (.var 2) (.var 5))) (.neg (.var 4)))) (.add (.add (.mul (.var 2) .one) (.mul (.neg (.neg (.var 4))) (.neg (.mul (.var 2) (.var 5))))) (.mul (.var 2) (.add (.mul (.mul (.add .one .one) (.var 4)) (.var 5)) (.neg .one)))) (by decide +kernel)709          rw [e, hw, add_neg, mul_zero, add_zero]710  · -- (7) forward711    have e : (r * x) * (r * x) + (y + r * z) * (-(y + -(r * z))) = (r * r + 1) * (x * x + z * z) + -(x * x + y * y + z * z) := Shell.Frame.RE.sound (Shell.Frame.look [x, y, z, r]) (.add (.mul (.mul (.var 3) (.var 0)) (.mul (.var 3) (.var 0))) (.mul (.add (.var 1) (.mul (.var 3) (.var 2))) (.neg (.add (.var 1) (.neg (.mul (.var 3) (.var 2))))))) (.add (.mul (.add (.mul (.var 3) (.var 3)) .one) (.add (.mul (.var 0) (.var 0)) (.mul (.var 2) (.var 2)))) (.neg (.add (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (.mul (.var 2) (.var 2))))) (by decide +kernel)712    rw [e, hr, neg_add, zero_mul, zero_add, hs]713  · -- (7) back714    have e : (-(r * a)) * (-(r * a)) + (h * (b + -c)) * (h * (b + -c)) + (-(h * (r * (b + c)))) * (-(h * (r * (b + c)))) =715        (a * a + (h * (b + c)) * (h * (b + c))) * (r * r + 1) + -(a * a + b * c) + -(b * c * (((1 + 1) * h + -1) * ((1 + 1) * h + 1))) := Shell.Frame.RE.sound (Shell.Frame.look [a, b, c, r, h]) (.add (.add (.mul (.neg (.mul (.var 3) (.var 0))) (.neg (.mul (.var 3) (.var 0)))) (.mul (.mul (.var 4) (.add (.var 1) (.neg (.var 2)))) (.mul (.var 4) (.add (.var 1) (.neg (.var 2)))))) (.mul (.neg (.mul (.var 4) (.mul (.var 3) (.add (.var 1) (.var 2))))) (.neg (.mul (.var 4) (.mul (.var 3) (.add (.var 1) (.var 2))))))) (.add (.add (.mul (.add (.mul (.var 0) (.var 0)) (.mul (.mul (.var 4) (.add (.var 1) (.var 2))) (.mul (.var 4) (.add (.var 1) (.var 2))))) (.add (.mul (.var 3) (.var 3)) .one)) (.neg (.add (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 2))))) (.neg (.mul (.mul (.var 1) (.var 2)) (.mul (.add (.mul (.add .one .one) (.var 4)) (.neg .one)) (.add (.mul (.add .one .one) (.var 4)) .one))))) (by decide +kernel)716    rw [e, hr, hq, hh, neg_add, mul_zero, zero_add, neg_neg, add_neg, zero_mul, mul_zero, neg_zero, add_zero]717  · -- (8) two frames over one point of the quadric differ by an element commuting with `i`718    have k1 : M'.adj.mul (M'.mul I) = M'.adj.mul (N.mul M') := congrArg M'.adj.mul hM''719    rw [← M2.mul_assoc', M2.adj_mul, M2.diag_mul, ← M2.mul_assoc'] at k1720    have k2 : (M2.smul M'.det I).mul M'.adj = ((M'.adj.mul N).mul M').mul M'.adj := congrArg (fun X => X.mul M'.adj) k1721    rw [M2.smul_mul, M2.mul_assoc', M2.mul_adj, M2.mul_diag] at k2722    have k3 : I.mul M'.adj = M'.adj.mul N := M2.smul_cancel F.fld hM' k2723    calc (M'.adj.mul M).mul I = M'.adj.mul (M.mul I) := M2.mul_assoc' _ _ _724      _ = (M'.adj.mul N).mul M := by rw [hM, M2.mul_assoc']725      _ = (I.mul M'.adj).mul M := by rw [k3]726      _ = I.mul (M'.adj.mul M) := M2.mul_assoc' _ _ _727728/-- The unit as a matrix, `diag(r, −r)` with `r = g^κ`: the corpus's unit is `i = −g^κ` (`quarterTurn`), so this is the729matrix of `−i`; projectively the same class as `diag(−r, r)`, with the same centraliser and the same quadric. -/730def unit (g : Shell p) (κ : Nat) : M2 p := ⟨g ^ κ, 0, 0, -(g ^ κ)⟩731732/-- A diagonal matrix `diag(a, d)`. -/733def diag (a d : Shell p) : M2 p := ⟨a, 0, 0, d⟩734735/-- 38:A9, 38:B6, 38:X4 — **the split fibration**, `unit_split_let`'s statement with the unit `unit g κ = diag(g^κ, −g^κ)` and the736diagonal matrices `diag a d` named (so that the key files re-elaborate it); the clauses are `unit_split_let`'s (1)–(8): the737centraliser of the unit is the diagonal torus inside the Borel, the unit is not scalar, the circle lands in the torus, the738conjugates fill the quadric `a² + bc = −1` and every point is reached, the quadric is the unit sphere, and two frames over739one point differ by an element of the centraliser. -/740theorem unit_split (F : Frame p κ g) :741    (∀ M : M2 p, M.mul (unit g κ) = (unit g κ).mul M → M.b = 0 ∧ M.c = 0) ∧742    (∀ a d : Shell p, (diag a d).mul (unit g κ) = (unit g κ).mul (diag a d) ∧ (diag a d) = borel a 0 d) ∧743    (∀ l : Shell p, (unit g κ) ≠ diag l l) ∧744    (∀ x y : Shell p, x * x + y * y = 1 → (diag (x + g ^ κ * y) (x + -(g ^ κ * y))).det = 1) ∧745    (∀ M : M2 p, ((M.mul (unit g κ)).mul M.adj).a + ((M.mul (unit g κ)).mul M.adj).d = 0 ∧746      ((M.mul (unit g κ)).mul M.adj).a * ((M.mul (unit g κ)).mul M.adj).a + ((M.mul (unit g κ)).mul M.adj).b * ((M.mul (unit g κ)).mul M.adj).c =747        -(M.det * M.det)) ∧748    (∀ N : M2 p, N.a + N.d = 0 → N.a * N.a + N.b * N.c = -1 → ∃ M : M2 p, M.det ≠ 0 ∧ M.mul (unit g κ) = N.mul M) ∧749    (∀ x y z : Shell p, x * x + y * y + z * z = 1 → (g ^ κ * x) * (g ^ κ * x) + (y + g ^ κ * z) * (-(y + -(g ^ κ * z))) = -1) ∧750    (∀ h : Shell p, (1 + 1) * h = 1 → ∀ a b c : Shell p, a * a + b * c = -1 →751      (-(g ^ κ * a)) * (-(g ^ κ * a)) + (h * (b + -c)) * (h * (b + -c)) + (-(h * (g ^ κ * (b + c)))) * (-(h * (g ^ κ * (b + c)))) = 1) ∧752    (∀ N M M' : M2 p, M'.det ≠ 0 → M.mul (unit g κ) = N.mul M → M'.mul (unit g κ) = N.mul M' →753      (M'.adj.mul M).mul (unit g κ) = (unit g κ).mul (M'.adj.mul M)) :=754  unit_split_let F755756/-- 38:A9, 38:A7 — the frame counts: `(p + 1)·p·(p − 1) = 14·13·12 = 2184 = 156·14`, the Borel `156 = 13·12`, the spin cover757twice the rotation half `2·1092 = 2184`, and `PGL₂` carries `169 = 13²` involutions against `SL₂`'s one. -/758theorem frame_counts :759    (14 : Nat) * 13 * 12 = 2184 ∧ (2184 : Nat) = 156 * 14 ∧ (156 : Nat) = 13 * 12 ∧ (2 : Nat) * 1092 = 2184 ∧760    (13 : Nat) * 13 = 169 ∧ (182 : Nat) = 13 * 14 ∧ (2184 : Nat) = 12 * 182 := by decide +kernel761762/-- The quaternion `x + y i + z j + w k` as a matrix, `[[x + r y, z + r w], [−z + r w, x − r y]]` with `r² = −1`. -/763def quat (r x y z w : Shell p) : M2 p := ⟨x + r * y, z + r * w, -z + r * w, x + -(r * y)⟩764765/-- 38:A7 — the norm-one sphere is `SL₂`: with `r² = −1` the quaternion `x + y i + z j + w k` is the matrix `quat`766(`1, i, j, k ↦ I, diag(r, −r), [[0, 1], [−1, 0]], [[0, r], [r, 0]]`) and its norm is the determinant. -/767theorem sphere_det {r : Shell p} (hr : r * r = -1) (x y z w : Shell p) :768    M2.det (quat r x y z w) = x * x + y * y + z * z + w * w := by769  have e : M2.det (quat r x y z w) =770      x * x + -((r * r) * (y * y)) + (z * z + -((r * r) * (w * w))) :=771    Shell.Frame.RE.sound (Shell.Frame.look [x, y, z, w, r]) (.add (.mul (.add (.var 0) (.mul (.var 4) (.var 1))) (.add (.var 0) (.neg (.mul (.var 4) (.var 1))))) (.neg (.mul (.add (.var 2) (.mul (.var 4) (.var 3))) (.add (.neg (.var 2)) (.mul (.var 4) (.var 3)))))) (.add (.add (.mul (.var 0) (.var 0)) (.neg (.mul (.mul (.var 4) (.var 4)) (.mul (.var 1) (.var 1))))) (.add (.mul (.var 2) (.var 2)) (.neg (.mul (.mul (.var 4) (.var 4)) (.mul (.var 3) (.var 3)))))) (by decide +kernel)772  rw [e, hr, neg_one_mul, neg_one_mul, neg_neg, neg_neg, ← add_assoc]773774end Frame775end Shell776end FRC777