Theme/Quaternion.lean — FrcCore

1import FrcCore.Theme.Framed2import FrcCore.Theme.Extension34/-!5# FrcCore.Theme.Quaternion — rotations in the window (the algebra theme)671-algebra's framed quaternions and their rotations (6 November 2026), moved here from the paper module8`FrcCore/Quaternion.lean`, every name unchanged, and completed in the core. The revision of 1-algebra of the same day9moved the rotations out of that paper's ledger; they wait for a paper of their own:1011* the framed quaternions compose exactly: with coordinates in the window `H` and a shell `p > 8H²` the product12  lies in the window `4H²` and the shell reading determines it (`quaternion_window`, `read_mul`);13* one axis: the rotation `x ↦ q x q̄ / N(q)` is the Cayley step of `S_v` (`rot_cayley`, `cayley_inj`), the14  half-turn at `a = 0` (`half_turn`), with kernel the scalars (`rot_trivial`) and `ρ_{−q} = ρ_q` (`rot_neg`); a quaternion15  `a + tv` with `a ≠ 0` is the scalar `a` times `1 + sv`, `s = t/a` (`axis_param`, `rot_smul`), distinct parameters16  give distinct rotations (`axis_inj`) and none of them is the half-turn (`axis_half`), and the parameter `s` fails exactly where `s² = −N(v)⁻¹`17  (`axis_exceptional`), at two values `±x` when `N(v)` is a square and at none otherwise (`neg_inv_square_iff`,18  `root_pair`); the window pairs `±(a, t)`, `|a|, |t| ≤ H`, number `2H² + 2H` (`box_count`);19* two axes: `(1 + u)(1 + w) = (1 − u·w) + (u + w + u × w)` (`one_add_mul`), the composition law (`compose`), the20  half-turn case (`one_add_mul_half`), the bracket (`bracket`), and the multiplicative norm (`nrm_mul`, `rot_mul`).2122No axioms.23-/2425namespace FRC26namespace Shell27namespace Frame2829variable {p : Nat} [Pos p]303132/-- A framed quaternion with signed window coordinates. -/33structure IQuat where34  a : SInt35  b : SInt36  c : SInt37  d : SInt3839/-- The Hamilton product on the window pairs, the same formula. -/40def IQuat.mul (q r : IQuat) : IQuat :=41  ⟨sadd (sadd (smul q.a r.a) (sneg (smul q.b r.b))) (sadd (sneg (smul q.c r.c)) (sneg (smul q.d r.d))),42   sadd (sadd (smul q.a r.b) (smul q.b r.a)) (sadd (smul q.c r.d) (sneg (smul q.d r.c))),43   sadd (sadd (smul q.a r.c) (sneg (smul q.b r.d))) (sadd (smul q.c r.a) (smul q.d r.b)),44   sadd (sadd (smul q.a r.d) (smul q.b r.c)) (sadd (sneg (smul q.c r.b)) (smul q.d r.a))⟩4546def IQuat.read (q : IQuat) : Quat p := ⟨sread q.a, sread q.b, sread q.c, sread q.d⟩47def IQuat.norm (q : IQuat) : IQuat := ⟨snorm q.a, snorm q.b, snorm q.c, snorm q.d⟩48def QBound (H : Nat) (q : IQuat) : Prop := SBound H q.a ∧ SBound H q.b ∧ SBound H q.c ∧ SBound H q.d4950theorem IQuat.ext' {q r : IQuat} (ha : q.a = r.a) (hb : q.b = r.b) (hc : q.c = r.c) (hd : q.d = r.d) : q = r := by51  cases q; cases r; cases ha; cases hb; cases hc; cases hd; rfl5253/-- Exact composition — the reading of the integer product is the product of the readings. -/54theorem read_mul (q r : IQuat) : ((IQuat.mul q r).read : Quat p) = Quat.mul q.read r.read := by55  unfold IQuat.mul IQuat.read Quat.mul56  rw [sread_add, sread_add, sread_add, sread_add, sread_add, sread_add, sread_add, sread_add, sread_add,57    sread_add, sread_add, sread_add, sread_neg, sread_neg, sread_neg, sread_neg, sread_neg, sread_neg,58    sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul,59    sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul]6061theorem read_norm (q : IQuat) : (q.norm.read : Quat p) = q.read := by62  unfold IQuat.norm IQuat.read63  rw [sread_norm, sread_norm, sread_norm, sread_norm]6465theorem norm_bound {H : Nat} {q r : IQuat} (hq : QBound H q) (hr : QBound H r) :66    QBound (4 * (H * H)) (IQuat.mul q r).norm := by67  have m := fun {x y : SInt} (hx : SBound H x) (hy : SBound H y) => smul_bound hx hy68  refine ⟨?_, ?_, ?_, ?_⟩69  · have := sum4_bound (m hq.1 hr.1) (sneg_bound (m hq.2.1 hr.2.1)) (sneg_bound (m hq.2.2.1 hr.2.2.1))70      (sneg_bound (m hq.2.2.2 hr.2.2.2))71    exact snorm_bound this.1 this.272  · have := sum4_bound (m hq.1 hr.2.1) (m hq.2.1 hr.1) (m hq.2.2.1 hr.2.2.2) (sneg_bound (m hq.2.2.2 hr.2.2.1))73    exact snorm_bound this.1 this.274  · have := sum4_bound (m hq.1 hr.2.2.1) (sneg_bound (m hq.2.1 hr.2.2.2)) (m hq.2.2.1 hr.1) (m hq.2.2.2 hr.2.1)75    exact snorm_bound this.1 this.276  · have := sum4_bound (m hq.1 hr.2.2.2) (m hq.2.1 hr.2.2.1) (sneg_bound (m hq.2.2.1 hr.2.1)) (m hq.2.2.2 hr.1)77    exact snorm_bound this.1 this.27879/-- The finitary clause — framed quaternions with window coordinates `≤ H`, read in a shell `p > 8H²`,80compose exactly: the product of the readings is the reading of the integer product; that product's81coordinates lie in the window `4H²`; and the reading determines it among the window's quaternions. -/82theorem quaternion_window {H : Nat} (hH : 8 * (H * H) < p) {q r : IQuat} (hq : QBound H q) (hr : QBound H r) :83    ((IQuat.mul q r).read : Quat p) = Quat.mul q.read r.read ∧84    QBound (4 * (H * H)) (IQuat.mul q r).norm ∧85    ∀ s : IQuat, QBound (4 * (H * H)) s → (s.read : Quat p) = (IQuat.mul q r).read → s = (IQuat.mul q r).norm := by86  refine ⟨read_mul q r, norm_bound hq hr, ?_⟩87  intro s hs he88  have hn := norm_bound hq hr89  have hM : 2 * (4 * (H * H)) < p := by rw [← Nat.mul_assoc]; exact hH90  rw [← read_norm (IQuat.mul q r)] at he91  unfold IQuat.read at he92  exact IQuat.ext' (sread_inj hM hs.1 hn.1 (congrArg Quat.a he)) (sread_inj hM hs.2.1 hn.2.1 (congrArg Quat.b he))93    (sread_inj hM hs.2.2.1 hn.2.2.1 (congrArg Quat.c he)) (sread_inj hM hs.2.2.2 hn.2.2.2 (congrArg Quat.d he))9495/-! ## The Lie-algebra layer, one axis -/9697/-- Conjugation keeps a pure quaternion pure: the scalar part of `q x q̄` vanishes. -/98theorem rot_pure (q x : Quat p) (hx : x.a = 0) : (Quat.conjBy q x).a = 0 := by99  rw [Quat.pure_eq hx]100  exact RE.sound (look [q.a, q.b, q.c, q.d, x.b, x.c, x.d]) (QR.conjBy (QR.v 0) (QR.pv 4)).a .zero (by decide +kernel)101102/-- The Cayley form cleared of the norm: for `q = a + v` and a pure `x`, the conjugate `y = q x q̄` satisfies103`(aI − S_v) y = N(q) (aI + S_v) x`, where `S_v x = v × x`. -/104theorem rot_cayley (q x : Quat p) (hx : x.a = 0) :105    Quat.add (Quat.smul q.a (Quat.conjBy q x)) (Quat.neg (Quat.cross (Quat.vec q) (Quat.conjBy q x))) =106      Quat.smul (Quat.nrm q) (Quat.add (Quat.smul q.a x) (Quat.cross (Quat.vec q) x)) := by107  rw [Quat.pure_eq hx]108  exact QR.sound (look [q.a, q.b, q.c, q.d, x.b, x.c, x.d])109    (QR.add (QR.smul (.var 0) (QR.conjBy (QR.v 0) (QR.pv 4))) (QR.neg (QR.cross (QR.vec (QR.v 0)) (QR.conjBy (QR.v 0) (QR.pv 4)))))110    (QR.smul (QR.nrm (QR.v 0)) (QR.add (QR.smul (.var 0) (QR.pv 4)) (QR.cross (QR.vec (QR.v 0)) (QR.pv 4)))) (by decide +kernel)111112/-- The half-turn: for pure `v` and `x`, `v x v̄ = N(v) x + 2 v × (v × x)`, so `ρ_v = I + 2N(v)⁻¹ S_v²`. -/113theorem half_turn (v x : Quat p) (hv : v.a = 0) (hx : x.a = 0) :114    Quat.conjBy v x = Quat.add (Quat.smul (Quat.nrm v) x) (Quat.add (Quat.cross v (Quat.cross v x)) (Quat.cross v (Quat.cross v x))) := by115  rw [Quat.pure_eq hv, Quat.pure_eq hx]116  exact QR.sound (look [v.b, v.c, v.d, x.b, x.c, x.d])117    (QR.conjBy (QR.pv 0) (QR.pv 3))118    (QR.add (QR.smul (QR.nrm (QR.pv 0)) (QR.pv 3)) (QR.add (QR.cross (QR.pv 0) (QR.cross (QR.pv 0) (QR.pv 3))) (QR.cross (QR.pv 0) (QR.cross (QR.pv 0) (QR.pv 3))))) (by decide +kernel)119120/-- The key identity of uniqueness: with `w = a z − v × z`, `a (a² + N(v)) z = a² w + a (v × w) + (v · w) v`. -/121theorem cayley_key (a : Shell p) (v z : Quat p) (hv : v.a = 0) (hz : z.a = 0) :122    Quat.smul (a * (a * a + Quat.dot v v)) z =123      Quat.add (Quat.add (Quat.smul (a * a) (Quat.add (Quat.smul a z) (Quat.neg (Quat.cross v z))))124        (Quat.smul a (Quat.cross v (Quat.add (Quat.smul a z) (Quat.neg (Quat.cross v z))))))125        (Quat.smul (Quat.dot v (Quat.add (Quat.smul a z) (Quat.neg (Quat.cross v z)))) v) := by126  rw [Quat.pure_eq hv, Quat.pure_eq hz]127  exact QR.sound (look [a, v.b, v.c, v.d, z.b, z.c, z.d])128    (QR.smul (.mul (.var 0) (.add (.mul (.var 0) (.var 0)) (QR.dot (QR.pv 1) (QR.pv 1)))) (QR.pv 4))129    (QR.add (QR.add (QR.smul (.mul (.var 0) (.var 0)) (QR.add (QR.smul (.var 0) (QR.pv 4)) (QR.neg (QR.cross (QR.pv 1) (QR.pv 4)))))130        (QR.smul (.var 0) (QR.cross (QR.pv 1) (QR.add (QR.smul (.var 0) (QR.pv 4)) (QR.neg (QR.cross (QR.pv 1) (QR.pv 4)))))))131      (QR.smul (QR.dot (QR.pv 1) (QR.add (QR.smul (.var 0) (QR.pv 4)) (QR.neg (QR.cross (QR.pv 1) (QR.pv 4))))) (QR.pv 1))) (by decide +kernel)132133theorem add_neg_q (q : Quat p) : Quat.add q (Quat.neg q) = ⟨0, 0, 0, 0⟩ :=134  QR.sound (look [q.a, q.b, q.c, q.d]) (QR.add (QR.v 0) (QR.neg (QR.v 0))) ⟨.zero, .zero, .zero, .zero⟩ (by decide +kernel)135136theorem key_zero (a : Shell p) (v : Quat p) :137    Quat.add (Quat.add (Quat.smul (a * a) ⟨0, 0, 0, 0⟩) (Quat.smul a (Quat.cross v ⟨0, 0, 0, 0⟩)))138      (Quat.smul (Quat.dot v ⟨0, 0, 0, 0⟩) v) = ⟨0, 0, 0, 0⟩ :=139  QR.sound (look [a, v.a, v.b, v.c, v.d])140    (QR.add (QR.add (QR.smul (.mul (.var 0) (.var 0)) ⟨.zero, .zero, .zero, .zero⟩) (QR.smul (.var 0) (QR.cross (QR.v 1) ⟨.zero, .zero, .zero, .zero⟩)))141      (QR.smul (QR.dot (QR.v 1) ⟨.zero, .zero, .zero, .zero⟩) (QR.v 1))) ⟨.zero, .zero, .zero, .zero⟩ (by decide +kernel)142143/-- `aI − S_v` is injective on pure quaternions when `a ≠ 0` and `a² + N(v) ≠ 0` (a field shell). -/144theorem cayley_inj {κ : Nat} {g : Shell p} (F : Frame p κ g) {a : Shell p} {v z : Quat p} (hv : v.a = 0) (hz : z.a = 0)145    (ha : a ≠ 0) (hn : a * a + Quat.dot v v ≠ 0) (h : Quat.smul a z = Quat.cross v z) : z = ⟨0, 0, 0, 0⟩ := by146  have hw : Quat.add (Quat.smul a z) (Quat.neg (Quat.cross v z)) = ⟨0, 0, 0, 0⟩ := by rw [h]; exact add_neg_q _147  have key := cayley_key a v z hv hz148  rw [hw, key_zero] at key149  have hc : a * (a * a + Quat.dot v v) ≠ 0 := fun e =>150    match F.mul_eq_zero e with151    | .inl e1 => ha e1152    | .inr e2 => hn e2153  have comp : ∀ t : Shell p, a * (a * a + Quat.dot v v) * t = 0 → t = 0 := fun t e =>154    match F.mul_eq_zero e with155    | .inl e1 => absurd e1 hc156    | .inr e2 => e2157  exact Quat.ext4 hz (comp _ (congrArg Quat.b key)) (comp _ (congrArg Quat.c key)) (comp _ (congrArg Quat.d key))158159/-! ## The Lie-algebra layer, two axes and range -/160161/-- The product of two Gibbs quaternions: `(1 + u)(1 + w) = (1 − u·w) + (u + w + u × w)` for pure `u`, `w`. -/162theorem one_add_mul (u w : Quat p) (hu : u.a = 0) (hw : w.a = 0) :163    Quat.mul (Quat.add (Quat.sc 1) u) (Quat.add (Quat.sc 1) w) =164      Quat.add (Quat.sc (1 + -(Quat.dot u w))) (Quat.add (Quat.add u w) (Quat.cross u w)) := by165  rw [Quat.pure_eq hu, Quat.pure_eq hw]166  exact QR.sound (look [u.b, u.c, u.d, w.b, w.c, w.d])167    (QR.mul (QR.add (QR.sc .one) (QR.pv 0)) (QR.add (QR.sc .one) (QR.pv 3)))168    (QR.add (QR.sc (.add .one (.neg (QR.dot (QR.pv 0) (QR.pv 3))))) (QR.add (QR.add (QR.pv 0) (QR.pv 3)) (QR.cross (QR.pv 0) (QR.pv 3)))) (by decide +kernel)169170/-- The bracket: `uw − wu = 2 u × w` for pure `u`, `w`. -/171theorem bracket (u w : Quat p) (hu : u.a = 0) (hw : w.a = 0) :172    Quat.add (Quat.mul u w) (Quat.neg (Quat.mul w u)) = Quat.add (Quat.cross u w) (Quat.cross u w) := by173  rw [Quat.pure_eq hu, Quat.pure_eq hw]174  exact QR.sound (look [u.b, u.c, u.d, w.b, w.c, w.d])175    (QR.add (QR.mul (QR.pv 0) (QR.pv 3)) (QR.neg (QR.mul (QR.pv 3) (QR.pv 0)))) (QR.add (QR.cross (QR.pv 0) (QR.pv 3)) (QR.cross (QR.pv 0) (QR.pv 3))) (by decide +kernel)176177/-- Conjugation is multiplicative: `(qr) x (qr)‾ = q (r x r̄) q̄`. -/178theorem rot_mul (q r x : Quat p) : Quat.conjBy (Quat.mul q r) x = Quat.conjBy q (Quat.conjBy r x) :=179  QR.sound (look [q.a, q.b, q.c, q.d, r.a, r.b, r.c, r.d, x.a, x.b, x.c, x.d]) (QR.conjBy (QR.mul (QR.v 0) (QR.v 4)) (QR.v 8))180    (QR.conjBy (QR.v 0) (QR.conjBy (QR.v 4) (QR.v 8))) (by decide +kernel)181182/-- Scaling: `(sq) x (sq)‾ = s² q x q̄` and `N(sq) = s² N(q)`, so the rotation of `q` depends on `q` up to a scalar. -/183theorem rot_smul (s : Shell p) (q x : Quat p) :184    Quat.conjBy (Quat.smul s q) x = Quat.smul (s * s) (Quat.conjBy q x) ∧ Quat.nrm (Quat.smul s q) = s * s * Quat.nrm q :=185  ⟨QR.sound (look [s, q.a, q.b, q.c, q.d, x.a, x.b, x.c, x.d]) (QR.conjBy (QR.smul (.var 0) (QR.v 1)) (QR.v 5))186      (QR.smul (.mul (.var 0) (.var 0)) (QR.conjBy (QR.v 1) (QR.v 5))) (by decide +kernel),187   RE.sound (look [s, q.a, q.b, q.c, q.d]) (QR.nrm (QR.smul (.var 0) (QR.v 1))) (.mul (.mul (.var 0) (.var 0)) (QR.nrm (QR.v 1))) (by decide +kernel)⟩188189/-- The half-turn case: at `u · w = 1` the product `(1 + u)(1 + w)` is the pure quaternion `u + w + u × w`. -/190theorem one_add_mul_half (u w : Quat p) (hu : u.a = 0) (hw : w.a = 0) (h1 : Quat.dot u w = 1) :191    Quat.mul (Quat.add (Quat.sc 1) u) (Quat.add (Quat.sc 1) w) = Quat.add (Quat.sc 0) (Quat.add (Quat.add u w) (Quat.cross u w)) := by192  rw [one_add_mul u w hu hw, h1, add_neg]193194/-- The sign: `ρ_{−q} = ρ_q` (`(−q) x (−q)‾ = q x q̄`, `N(−q) = N(q)`); the window rotations of an axis come in195pairs `±(a, t)`, which bounds them by `2H² + 2H` (`FRC.Algebra.card_image_le_of_neg`). -/196theorem rot_neg (q x : Quat p) : Quat.conjBy (Quat.neg q) x = Quat.conjBy q x ∧ Quat.nrm (Quat.neg q) = Quat.nrm q :=197  ⟨QR.sound (look [q.a, q.b, q.c, q.d, x.a, x.b, x.c, x.d]) (QR.conjBy (QR.neg (QR.v 0)) (QR.v 4)) (QR.conjBy (QR.v 0) (QR.v 4)) (by decide +kernel),198   RE.sound (look [q.a, q.b, q.c, q.d]) (QR.nrm (QR.neg (QR.v 0))) (QR.nrm (QR.v 0)) (by decide +kernel)⟩199200theorem smul_sc_add (s s' : Shell p) (m : Quat p) :201    Quat.smul s (Quat.add (Quat.sc 1) (Quat.smul s' m)) = Quat.add (Quat.sc s) (Quat.smul (s * s') m) :=202  QR.sound (look [s, s', m.a, m.b, m.c, m.d]) (QR.smul (.var 0) (QR.add (QR.sc .one) (QR.smul (.var 1) (QR.v 2))))203    (QR.add (QR.sc (.var 0)) (QR.smul (.mul (.var 0) (.var 1)) (QR.v 2))) (by decide +kernel)204205theorem smul_one_q (m : Quat p) : Quat.smul 1 m = m :=206  QR.sound (look [m.a, m.b, m.c, m.d]) (QR.smul .one (QR.v 0)) (QR.v 0) (by decide +kernel)207208theorem smul_smul_q (s t : Shell p) (m : Quat p) : Quat.smul s (Quat.smul t m) = Quat.smul (s * t) m :=209  QR.sound (look [s, t, m.a, m.b, m.c, m.d]) (QR.smul (.var 0) (QR.smul (.var 1) (QR.v 2))) (QR.smul (.mul (.var 0) (.var 1)) (QR.v 2)) (by decide +kernel)210211theorem conjBy_smul (q y : Quat p) (t : Shell p) : Quat.conjBy q (Quat.smul t y) = Quat.smul t (Quat.conjBy q y) :=212  QR.sound (look [q.a, q.b, q.c, q.d, t, y.a, y.b, y.c, y.d]) (QR.conjBy (QR.v 0) (QR.smul (.var 4) (QR.v 5)))213    (QR.smul (.var 4) (QR.conjBy (QR.v 0) (QR.v 5))) (by decide +kernel)214215theorem inv_chain (nu nw s nc Nu Nw Nc : Shell p) (hu : Nu * nu = 1) (hw : Nw * nw = 1) (hc : Nc * nc = 1)216    (hN : Nu * Nw = s * s * Nc) : nu * nw * (s * s) = nc := by217  have e1 : nu * nw * (s * s) = nc * (nu * nw * (s * s * Nc)) := by218    calc nu * nw * (s * s) = nu * nw * (s * s) * (Nc * nc) := by rw [hc, mul_one]219      _ = nc * (nu * nw * (s * s * Nc)) :=220        RE.sound (look [nu, nw, s, nc, Nc])221          (.mul (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 2))) (.mul (.var 4) (.var 3)))222          (.mul (.var 3) (.mul (.mul (.var 0) (.var 1)) (.mul (.mul (.var 2) (.var 2)) (.var 4)))) (by decide +kernel)223  have e2 : nu * nw * (Nu * Nw) = (Nu * nu) * (Nw * nw) :=224    RE.sound (look [nu, nw, Nu, Nw]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))225      (.mul (.mul (.var 2) (.var 0)) (.mul (.var 3) (.var 1))) (by decide +kernel)226  rw [e1, ← hN, e2, hu, hw, mul_one, mul_one]227228/-- The composition law: for pure `u`, `w` with `1 + N(u)`, `1 + N(w)`, `1 − u·w` and `1 + N(u∘w)` invertible229(inverses `nu`, `nw`, `s'`, `nc`), `ρ_{1+u} ρ_{1+w} = ρ_{1+u∘w}` with `u∘w = (u + w + u × w)/(1 − u·w)`; here230`ρ_q x = N(q)⁻¹ q x q̄`. -/231theorem compose (u w x : Quat p) (hu : u.a = 0) (hw : w.a = 0) (s' nu nw nc : Shell p)232    (hs : (1 + -(Quat.dot u w)) * s' = 1)233    (hnu : Quat.nrm (Quat.add (Quat.sc 1) u) * nu = 1) (hnw : Quat.nrm (Quat.add (Quat.sc 1) w) * nw = 1)234    (hnc : Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s' (Quat.add (Quat.add u w) (Quat.cross u w)))) * nc = 1) :235    Quat.smul nu (Quat.conjBy (Quat.add (Quat.sc 1) u) (Quat.smul nw (Quat.conjBy (Quat.add (Quat.sc 1) w) x))) =236      Quat.smul nc (Quat.conjBy (Quat.add (Quat.sc 1) (Quat.smul s' (Quat.add (Quat.add u w) (Quat.cross u w)))) x) := by237  have hP : Quat.mul (Quat.add (Quat.sc 1) u) (Quat.add (Quat.sc 1) w) =238      Quat.smul (1 + -(Quat.dot u w)) (Quat.add (Quat.sc 1) (Quat.smul s' (Quat.add (Quat.add u w) (Quat.cross u w)))) := by239    rw [smul_sc_add, hs, smul_one_q, one_add_mul u w hu hw]240  have hN : Quat.nrm (Quat.add (Quat.sc 1) u) * Quat.nrm (Quat.add (Quat.sc 1) w) =241      (1 + -(Quat.dot u w)) * (1 + -(Quat.dot u w)) *242        Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s' (Quat.add (Quat.add u w) (Quat.cross u w)))) := by243    rw [← nrm_mul, hP, (rot_smul _ _ x).2]244  rw [conjBy_smul, smul_smul_q, ← rot_mul, hP, (rot_smul _ _ x).1, smul_smul_q, inv_chain nu nw _ nc _ _ _ hnu hnw hnc hN]245246theorem add_cancel_q {r m : Quat p} (h : Quat.add r m = r) : m = ⟨0, 0, 0, 0⟩ := by247  have c : ∀ x y : Shell p, x + y = x → y = 0 := fun x y e => add_right_cancel (c := x) (by rw [add_comm, e, zero_add])248  exact Quat.ext4 (c _ _ (congrArg Quat.a h)) (c _ _ (congrArg Quat.b h)) (c _ _ (congrArg Quat.c h)) (c _ _ (congrArg Quat.d h))249250theorem cayley_trivial_id (q x : Quat p) (hx : x.a = 0) :251    Quat.add (Quat.add (Quat.smul q.a (Quat.smul (Quat.nrm q) x)) (Quat.neg (Quat.cross (Quat.vec q) (Quat.smul (Quat.nrm q) x))))252      (Quat.smul (1 + 1) (Quat.smul (Quat.nrm q) (Quat.cross (Quat.vec q) x))) =253      Quat.smul (Quat.nrm q) (Quat.add (Quat.smul q.a x) (Quat.cross (Quat.vec q) x)) := by254  rw [Quat.pure_eq hx]255  exact QR.sound (look [q.a, q.b, q.c, q.d, x.b, x.c, x.d])256    (QR.add (QR.add (QR.smul (.var 0) (QR.smul (QR.nrm (QR.v 0)) (QR.pv 4))) (QR.neg (QR.cross (QR.vec (QR.v 0)) (QR.smul (QR.nrm (QR.v 0)) (QR.pv 4)))))257      (QR.smul (.add .one .one) (QR.smul (QR.nrm (QR.v 0)) (QR.cross (QR.vec (QR.v 0)) (QR.pv 4)))))258    (QR.smul (QR.nrm (QR.v 0)) (QR.add (QR.smul (.var 0) (QR.pv 4)) (QR.cross (QR.vec (QR.v 0)) (QR.pv 4)))) (by decide +kernel)259260/-- The kernel: on a field shell, a rotation `ρ_q` (`N(q) ≠ 0`) that fixes every pure quaternion has `q` a261scalar — so `a + t v ↦ ρ_{a+tv}` is injective on the pairs modulo the scalars, and the axis group of262`FRC.Algebra.axis_group` is the rotation group of the axis. -/263theorem rot_trivial {κ : Nat} {g : Shell p} (F : Frame p κ g) (q : Quat p) (hN : Quat.nrm q ≠ 0)264    (h : ∀ x : Quat p, x.a = 0 → Quat.conjBy q x = Quat.smul (Quat.nrm q) x) : q.b = 0 ∧ q.c = 0 ∧ q.d = 0 := by265  have key : ∀ x : Quat p, x.a = 0 → Quat.smul (1 + 1) (Quat.smul (Quat.nrm q) (Quat.cross (Quat.vec q) x)) = ⟨0, 0, 0, 0⟩ := by266    intro x hx267    have E := rot_cayley q x hx268    rw [h x hx] at E269    have I := cayley_trivial_id q x hx270    rw [← E] at I271    exact add_cancel_q I272  have h2 : (1 + 1 : Shell p) ≠ 0 := by rw [← two_eq_one_add_one]; exact F.two_ne_zero273  have z : ∀ t : Shell p, (1 + 1) * (Quat.nrm q * t) = 0 → t = 0 := fun t e =>274    match F.mul_eq_zero e with275    | .inl e1 => absurd e1 h2276    | .inr e2 => match F.mul_eq_zero e2 with277      | .inl e3 => absurd e3 hN278      | .inr e4 => e4279  have kb := key ⟨0, 1, 0, 0⟩ rfl280  have kc := key ⟨0, 0, 1, 0⟩ rfl281  have hd : q.d = 0 := z _ (by282    have := congrArg Quat.c kb283    simp only [Quat.smul, Quat.cross, Quat.vec] at this284    rw [mul_one, mul_zero, neg_zero, add_zero] at this; exact this)285  have hcneg : -q.c = 0 := z _ (by286    have := congrArg Quat.d kb287    simp only [Quat.smul, Quat.cross, Quat.vec] at this288    rw [mul_zero, mul_one] at this289    rw [zero_add] at this; exact this)290  have hb : q.b = 0 := z _ (by291    have := congrArg Quat.d kc292    simp only [Quat.smul, Quat.cross, Quat.vec] at this293    rw [mul_one, mul_zero, neg_zero, add_zero] at this; exact this)294  refine ⟨hb, ?_, hd⟩295  rw [← neg_neg q.c, hcneg, neg_zero]296297298299/-! ## The axis: parameters, injectivity, exceptional values, the window count -/300301/-- On the axis of `v`, `a + t v` (`a y = 1`) is the scalar `a` times `1 + s v` with `s = t y`. -/302theorem axis_param {a t y : Shell p} (hay : a * y = 1) (v : Quat p) :303    Quat.add (Quat.sc a) (Quat.smul t v) = Quat.smul a (Quat.add (Quat.sc 1) (Quat.smul (t * y) v)) := by304  have key : ∀ w : Shell p, t * w = a * (t * y * w) := fun w => by305    calc t * w = (a * y) * (t * w) := by rw [hay, one_mul]306      _ = a * (t * y * w) := RE.sound (look [a, y, t, w]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))307            (.mul (.var 0) (.mul (.mul (.var 2) (.var 1)) (.var 3))) (by decide +kernel)308  apply Quat.ext4309  · show a + t * v.a = a * (1 + t * y * v.a)310    rw [left_distrib, mul_one, ← key]311  · show 0 + t * v.b = a * (0 + t * y * v.b)312    rw [zero_add, zero_add, ← key]313  · show 0 + t * v.c = a * (0 + t * y * v.c)314    rw [zero_add, zero_add, ← key]315  · show 0 + t * v.d = a * (0 + t * y * v.d)316    rw [zero_add, zero_add, ← key]317318/-- `q̄ (q x q̄) q = N(q)² x`. -/319theorem conj_conjBy (q x : Quat p) : Quat.conjBy (Quat.conj q) (Quat.conjBy q x) = Quat.smul (Quat.nrm q * Quat.nrm q) x :=320  QR.sound (look [q.a, q.b, q.c, q.d, x.a, x.b, x.c, x.d]) (QR.conjBy (QR.conj (QR.v 0)) (QR.conjBy (QR.v 0) (QR.v 4)))321    (QR.smul (.mul (QR.nrm (QR.v 0)) (QR.nrm (QR.v 0))) (QR.v 4)) (by decide +kernel)322323theorem nrm_conj (q : Quat p) : Quat.nrm (Quat.conj q) = Quat.nrm q :=324  RE.sound (look [q.a, q.b, q.c, q.d]) (QR.nrm (QR.conj (QR.v 0))) (QR.nrm (QR.v 0)) (by decide +kernel)325326/-- `(1 − s v)(1 + t v) = (1 + st N(v)) + (t − s) v` for a pure `v = (0, b, c, d)`. -/327theorem axis_quotient (s t b c d : Shell p) :328    Quat.mul (Quat.conj (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩))) (Quat.add (Quat.sc 1) (Quat.smul t ⟨0, b, c, d⟩)) =329    Quat.add (Quat.sc (1 + s * t * (b * b + c * c + d * d))) (Quat.smul (t + -s) ⟨0, b, c, d⟩) :=330  QR.sound (look [s, t, b, c, d])331    (QR.mul (QR.conj (QR.add (QR.sc .one) (QR.smul (.var 0) ⟨.zero, .var 2, .var 3, .var 4⟩)))332      (QR.add (QR.sc .one) (QR.smul (.var 1) ⟨.zero, .var 2, .var 3, .var 4⟩)))333    (QR.add (QR.sc (.add .one (.mul (.mul (.var 0) (.var 1)) (.add (.add (.mul (.var 2) (.var 2)) (.mul (.var 3) (.var 3))) (.mul (.var 4) (.var 4))))))334      (QR.smul (.add (.var 1) (.neg (.var 0))) ⟨.zero, .var 2, .var 3, .var 4⟩)) (by decide +kernel)335336/-- Distinct parameters give distinct rotations: if `1 + s v` and `1 + t v` (`v` pure and nonzero, both norms337nonzero) rotate every pure quaternion alike, `N(r) ρ_q = N(q) ρ_r`, then `s = t`. -/338theorem axis_inj {κ : Nat} {g : Shell p} (F : Frame p κ g) {b c d s t : Shell p} (hv0 : b ≠ 0 ∨ c ≠ 0 ∨ d ≠ 0)339    (hq : Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩)) ≠ 0)340    (hr : Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul t ⟨0, b, c, d⟩)) ≠ 0)341    (h : ∀ x : Quat p, x.a = 0 →342      Quat.smul (Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul t ⟨0, b, c, d⟩))) (Quat.conjBy (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩)) x) =343      Quat.smul (Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩))) (Quat.conjBy (Quat.add (Quat.sc 1) (Quat.smul t ⟨0, b, c, d⟩)) x)) :344    s = t := by345  generalize hQ : Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩) = q at hq h346  generalize hR : Quat.add (Quat.sc 1) (Quat.smul t ⟨0, b, c, d⟩) = r at hr h347  have hw : Quat.mul (Quat.conj q) r = Quat.add (Quat.sc (1 + s * t * (b * b + c * c + d * d))) (Quat.smul (t + -s) ⟨0, b, c, d⟩) := by348    rw [← hQ, ← hR]; exact axis_quotient s t b c d349  have hNw : Quat.nrm (Quat.mul (Quat.conj q) r) = Quat.nrm q * Quat.nrm r := by rw [nrm_mul, nrm_conj]350  have hNw0 : Quat.nrm (Quat.mul (Quat.conj q) r) ≠ 0 := by rw [hNw]; exact F.mul_ne_zero hq hr351  have triv : ∀ x : Quat p, x.a = 0 → Quat.conjBy (Quat.mul (Quat.conj q) r) x = Quat.smul (Quat.nrm (Quat.mul (Quat.conj q) r)) x := by352    intro x hx353    have e1 : Quat.smul (Quat.nrm q) (Quat.conjBy (Quat.mul (Quat.conj q) r) x) =354        Quat.smul (Quat.nrm q) (Quat.smul (Quat.nrm (Quat.mul (Quat.conj q) r)) x) := by355      rw [rot_mul, ← conjBy_smul, ← h x hx, conjBy_smul, conj_conjBy, smul_smul_q, smul_smul_q, hNw]356      congr 1357      exact RE.sound (look [Quat.nrm q, Quat.nrm r]) (.mul (.var 1) (.mul (.var 0) (.var 0))) (.mul (.var 0) (.mul (.var 0) (.var 1))) (by decide +kernel)358    have cancel : ∀ u w : Shell p, Quat.nrm q * u = Quat.nrm q * w → u = w := fun u w e => F.mul_left_cancel hq e359    exact Quat.ext4 (cancel _ _ (congrArg Quat.a e1)) (cancel _ _ (congrArg Quat.b e1)) (cancel _ _ (congrArg Quat.c e1)) (cancel _ _ (congrArg Quat.d e1))360  obtain ⟨hb, hc, hd⟩ := rot_trivial F _ hNw0 triv361  rw [hw] at hb hc hd362  have hb' : (t + -s) * b = 0 := by have := hb; simp only [Quat.add, Quat.sc, Quat.smul] at this; rw [zero_add] at this; exact this363  have hc' : (t + -s) * c = 0 := by have := hc; simp only [Quat.add, Quat.sc, Quat.smul] at this; rw [zero_add] at this; exact this364  have hd' : (t + -s) * d = 0 := by have := hd; simp only [Quat.add, Quat.sc, Quat.smul] at this; rw [zero_add] at this; exact this365  have hts : t + -s = 0 := by366    match hv0 with367    | Or.inl hb0 => exact (F.mul_eq_zero hb').resolve_right hb0368    | Or.inr (Or.inl hc0) => exact (F.mul_eq_zero hc').resolve_right hc0369    | Or.inr (Or.inr hd0) => exact (F.mul_eq_zero hd').resolve_right hd0370  exact (Prime.eq_of_sub_eq_zero hts).symm371372/-- `(1 − s v) v = s N(v) + v` for a pure `v = (0, b, c, d)`. -/373theorem axis_half_quotient (s b c d : Shell p) :374    Quat.mul (Quat.conj (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩))) ⟨0, b, c, d⟩ =375    Quat.add (Quat.sc (s * (b * b + c * c + d * d))) ⟨0, b, c, d⟩ :=376  QR.sound (look [s, b, c, d])377    (QR.mul (QR.conj (QR.add (QR.sc .one) (QR.smul (.var 0) ⟨.zero, .var 1, .var 2, .var 3⟩))) ⟨.zero, .var 1, .var 2, .var 3⟩)378    (QR.add (QR.sc (.mul (.var 0) (.add (.add (.mul (.var 1) (.var 1)) (.mul (.var 2) (.var 2))) (.mul (.var 3) (.var 3)))))379      ⟨.zero, .var 1, .var 2, .var 3⟩) (by decide +kernel)380381/-- The half-turn is not among the parameters: `ρ_{1+sv} ≠ ρ_v` for a pure nonzero `v` (the quotient382`(1 − s v) v = sN(v) + v` is never a scalar). -/383theorem axis_half {κ : Nat} {g : Shell p} (F : Frame p κ g) {b c d s : Shell p} (hv0 : b ≠ 0 ∨ c ≠ 0 ∨ d ≠ 0)384    (hq : Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩)) ≠ 0)385    (hr : Quat.nrm (⟨0, b, c, d⟩ : Quat p) ≠ 0)386    (h : ∀ x : Quat p, x.a = 0 →387      Quat.smul (Quat.nrm (⟨0, b, c, d⟩ : Quat p)) (Quat.conjBy (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩)) x) =388      Quat.smul (Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩))) (Quat.conjBy ⟨0, b, c, d⟩ x)) : False := by389  generalize hQ : Quat.add (Quat.sc 1) (Quat.smul s ⟨0, b, c, d⟩) = q at hq h390  generalize hR : (⟨0, b, c, d⟩ : Quat p) = r at hr h391  have hw : Quat.mul (Quat.conj q) r = Quat.add (Quat.sc (s * (b * b + c * c + d * d))) ⟨0, b, c, d⟩ := by392    rw [← hQ, ← hR]; exact axis_half_quotient s b c d393  have hNw : Quat.nrm (Quat.mul (Quat.conj q) r) = Quat.nrm q * Quat.nrm r := by rw [nrm_mul, nrm_conj]394  have hNw0 : Quat.nrm (Quat.mul (Quat.conj q) r) ≠ 0 := by rw [hNw]; exact F.mul_ne_zero hq hr395  have triv : ∀ x : Quat p, x.a = 0 → Quat.conjBy (Quat.mul (Quat.conj q) r) x = Quat.smul (Quat.nrm (Quat.mul (Quat.conj q) r)) x := by396    intro x hx397    have e1 : Quat.smul (Quat.nrm q) (Quat.conjBy (Quat.mul (Quat.conj q) r) x) =398        Quat.smul (Quat.nrm q) (Quat.smul (Quat.nrm (Quat.mul (Quat.conj q) r)) x) := by399      rw [rot_mul, ← conjBy_smul, ← h x hx, conjBy_smul, conj_conjBy, smul_smul_q, smul_smul_q, hNw]400      congr 1401      exact RE.sound (look [Quat.nrm q, Quat.nrm r]) (.mul (.var 1) (.mul (.var 0) (.var 0))) (.mul (.var 0) (.mul (.var 0) (.var 1))) (by decide +kernel)402    have cancel : ∀ u w : Shell p, Quat.nrm q * u = Quat.nrm q * w → u = w := fun u w e => F.mul_left_cancel hq e403    exact Quat.ext4 (cancel _ _ (congrArg Quat.a e1)) (cancel _ _ (congrArg Quat.b e1)) (cancel _ _ (congrArg Quat.c e1)) (cancel _ _ (congrArg Quat.d e1))404  obtain ⟨hb, hc, hd⟩ := rot_trivial F _ hNw0 triv405  rw [hw] at hb hc hd406  have hb' : b = 0 := by have := hb; simp only [Quat.add, Quat.sc] at this; rw [zero_add] at this; exact this407  have hc' : c = 0 := by have := hc; simp only [Quat.add, Quat.sc] at this; rw [zero_add] at this; exact this408  have hd' : d = 0 := by have := hd; simp only [Quat.add, Quat.sc] at this; rw [zero_add] at this; exact this409  match hv0 with410  | Or.inl h0 => exact h0 hb'411  | Or.inr (Or.inl h0) => exact h0 hc'412  | Or.inr (Or.inr h0) => exact h0 hd'413414/-- The parameter `s` fails exactly at the roots of `1 + N s² = 0`, that is `s² = −N⁻¹` (`N m = 1`). -/415theorem axis_exceptional {N m : Shell p} (hm : N * m = 1) (s : Shell p) : (1 : Shell p) + N * (s * s) = 0 ↔ s * s = -m := by416  constructor417  · intro h418    have h1 : N * (s * s) = -1 := (eq_neg_of_add_eq_zero (by rw [add_comm]; exact h))419    calc s * s = (m * N) * (s * s) := by rw [mul_comm m N, hm, one_mul]420      _ = m * (N * (s * s)) := mul_assoc _ _ _421      _ = -m := by rw [h1, ← mul_neg, mul_one]422  · intro h423    rw [h, ← mul_neg, hm]424    exact add_neg 1425426/-- On a framed shell `−N⁻¹` is a square exactly when `N` is (the quarter-turn turns one into the other), so the427exceptional parameters are two (`root_pair`) when `N` is a square and none otherwise. -/428theorem neg_inv_square_iff {κ : Nat} {g : Shell p} (F : Frame p κ g) {N m : Shell p} (hm : N * m = 1) :429    (∃ x : Shell p, x * x = -m) ↔ (∃ y : Shell p, y * y = N) := by430  have hm0 : m ≠ 0 := fun e => F.one_ne_zero (by rw [← hm, e, mul_zero])431  have hN0 : N ≠ 0 := fun e => F.one_ne_zero (by rw [← hm, e, zero_mul])432  have hi := F.quarter_turn_sq433  constructor434  · intro ⟨x, hx⟩435    have hx0 : x ≠ 0 := fun e => hm0 (by436      have : -m = 0 := by rw [← hx, e, mul_zero]437      rw [← neg_neg m, this, neg_zero])438    obtain ⟨xi, hxi⟩ := F.exists_inv hx0439    refine ⟨quarterTurn g κ * xi, ?_⟩440    -- (i xi)² = −xi², and −xi² · m = (xi x)² = 1, so −xi² = N441    apply inv_unique (y := m)442    · calc quarterTurn g κ * xi * (quarterTurn g κ * xi) * m = (quarterTurn g κ * quarterTurn g κ) * (xi * xi) * m :=443            RE.sound (look [quarterTurn g κ, xi, m]) (.mul (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (.var 2))444              (.mul (.mul (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (.var 2)) (by decide +kernel)445        _ = (xi * xi) * (x * x) := by446            rw [hi, hx]447            exact RE.sound (look [xi, m]) (.mul (.mul (.neg .one) (.mul (.var 0) (.var 0))) (.var 1))448              (.mul (.mul (.var 0) (.var 0)) (.neg (.var 1))) (by decide +kernel)449        _ = (x * xi) * (x * xi) := RE.sound (look [x, xi]) (.mul (.mul (.var 1) (.var 1)) (.mul (.var 0) (.var 0)))450              (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (by decide +kernel)451        _ = 1 := by rw [hxi, one_mul]452    · exact hm453  · intro ⟨y, hy⟩454    have hy0 : y ≠ 0 := fun e => hN0 (by rw [← hy, e, mul_zero])455    obtain ⟨yi, hyi⟩ := F.exists_inv hy0456    refine ⟨quarterTurn g κ * yi, ?_⟩457    have hyim : yi * yi = m := by458      apply inv_unique (y := N)459      · calc yi * yi * N = (y * yi) * (y * yi) := by460              rw [← hy]461              exact RE.sound (look [y, yi]) (.mul (.mul (.var 1) (.var 1)) (.mul (.var 0) (.var 0)))462                (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1))) (by decide +kernel)463          _ = 1 := by rw [hyi, one_mul]464      · rw [mul_comm]; exact hm465    calc quarterTurn g κ * yi * (quarterTurn g κ * yi) = (quarterTurn g κ * quarterTurn g κ) * (yi * yi) :=466          RE.sound (look [quarterTurn g κ, yi]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 0) (.var 1)))467            (.mul (.mul (.var 0) (.var 0)) (.mul (.var 1) (.var 1))) (by decide +kernel)468      _ = -m := by rw [hi, hyim, neg_one_mul]469470/-- The window box: the `(2H + 1)²` pairs `(a, t)`, `|a|, |t| ≤ H`, are the origin and `2(2H² + 2H)` others,471which the sign `(a, t) ↦ (−a, −t)` (`window_signed`, `rot_neg`) pairs into `2H² + 2H` classes. -/472theorem box_count (H : Nat) : (2 * H + 1) * (2 * H + 1) = 2 * (2 * H * H + 2 * H) + 1 := by473  have hA : 2 * (2 * H * H) = 2 * H * (2 * H) := by474    rw [Nat.mul_comm 2 (2 * H * H), FRC.Nat.mul_assoc (2 * H) H 2, Nat.mul_comm H 2]475  calc (2 * H + 1) * (2 * H + 1) = (2 * H + 1) * (2 * H) + (2 * H + 1) := Nat.mul_succ _ _476    _ = 2 * H * (2 * H) + 1 * (2 * H) + (2 * H + 1) := by rw [FRC.Nat.add_mul]477    _ = 2 * H * (2 * H) + (2 * H + 2 * H) + 1 := by rw [Nat.one_mul, Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]478    _ = 2 * (2 * H * H) + 2 * (2 * H) + 1 := by rw [hA, ← Nat.two_mul]479    _ = 2 * (2 * H * H + 2 * H) + 1 := by rw [Nat.left_distrib]480481end Frame482end Shell483end FRC484