The core module lean/FrcCore/Quaternion.lean — the substrate from first principles, no Mathlib, no axioms (the modules in order: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Projective, Theme/Fourier, Theme/Fractional, Theme/Lifts, Theme/Dichotomy, Theme/Rotations, Theme/Heisenberg, Theme/Spectra, Theme/Exclusivity, Theme/Quadratic, Theme/Extension, Theme/Tally, Theme/Numbers, Theme/Logic, Theme/SecondOrder, Theme/Formation, Theme/Field, Theme/Foundation, Theme/Drive, Theme/Carrier, Theme/Subject, Theme/Pair, Theme/Hopf, Theme/Symbol, Theme/Gravity, Theme/Quantum, Theme/Unitary, Theme/Interactions, Theme/Horizon, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Observation, Theme/Interference, Theme/Composite, Theme/Ladder, Meridian, Fourier, Algebra, Epi, Dimensions, Poly, Quaternion, Causality, Representation, Reductio, Godel, Finitism, Geometry, Complex, Instances, Rh, Entropy, Dirac, Gravity, S13, Qm, Pnp, Keys/Frame, Keys/Extension, Keys/Projective, Keys/Fourier, Keys/Numbers, Keys/Logic, Keys/Foundation, Keys/Carrier, Keys/Subject, Keys/Gravity, Keys/Quantum, Keys/Interactions, Keys/Horizon): 40 theorems (12 definitions): 40 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Algebra2import FrcCore.Theme.Extension34/-!5# FrcCore.Quaternion — the framed quaternions and the window (1:E6, the finitary clause); the Lie-algebra layer (1:E7, 1:E8)67A signed window integer is a pair of naturals `(u, v)` read as `u − v` in the shell (no `Int`: the core's8integers are the shell's own readings). A framed quaternion is four such pairs; the Hamilton product is9computed on the pairs, and `read_mul` says the product of the readings is the reading of the product — the10composition is exact. `quaternion_window` adds the bounds: with coordinates in the window `H` and a shell11`p > 8H²`, the product's coordinates lie in the window `4H²`, and the shell reading determines the integer12product among the window's quaternions. No axioms.1314The Lie-algebra layer works on quaternions over the shell (`Quat`, with `conj`, `nrm`, `cross`, `dot`). Its identities are15decided by a normaliser: `RE.sound` expands both sides of an identity into sorted lists of monomials and compares them by a16kernel computation, so an identity is one `decide +kernel`. 1:E7: the rotation `x ↦ q x q̄ / N(q)` is the Cayley17transform `(aI − S_v)⁻¹(aI + S_v)` (`rot_cayley`, `cayley_inj`), the half-turn at `a = 0` (`half_turn`), with kernel the18scalars (`rot_trivial`) and `ρ_{−q} = ρ_q` (`rot_neg`). 1:E8: `(1+u)(1+w) = (1 − u·w) + (u + w + u × w)` (`one_add_mul`),19the composition law (`compose`), the bracket (`bracket`). No axioms.2021Since the ledger migration (task LM17) the quaternions over the shell, their norm and the ring normaliser live in the22extension theme (`Theme/Extension.lean`) under their names; this module keeps the window and the Lie-algebra layer.23-/2425namespace FRC26namespace Shell27namespace Frame2829variable {p : Nat} [Pos p]3031/-- A signed window integer: `(u, v)` stands for `u − v`. -/32
abbrev SInt := Nat × Nat3334def sread (x : SInt) : Shell p := ofNat x.1 + -(ofNat x.2)35def sadd (x y : SInt) : SInt := (x.1 + y.1, x.2 + y.2)36def sneg (x : SInt) : SInt := (x.2, x.1)37def smul (x y : SInt) : SInt := (x.1 * y.1 + x.2 * y.2, x.1 * y.2 + x.2 * y.1)38/-- The canonical pair of the same value: one component zero. -/39def snorm (x : SInt) : SInt := (x.1 - x.2, x.2 - x.1)4041
theorem prod_ext {x y : SInt} (h1 : x.1 = y.1) (h2 : x.2 = y.2) : x = y :=42 match x, y, h1, h2 with43 | (_, _), (_, _), h1, h2 => by cases h1; cases h2; rfl4445theorem sread_add (x y : SInt) : (sread (sadd x y) : Shell p) = sread x + sread y := by46 unfold sread sadd47 show ofNat (x.1 + y.1) + -(ofNat (x.2 + y.2)) = ofNat x.1 + -(ofNat x.2) + (ofNat y.1 + -(ofNat y.2))48 rw [← ofNat_add, ← ofNat_add, neg_add_rev, add_assoc, add_assoc, ← add_assoc (-(ofNat x.2)),49 add_comm (-(ofNat x.2)) (ofNat y.1), add_assoc]5051theorem sread_neg (x : SInt) : (sread (sneg x) : Shell p) = -(sread x) := by52 unfold sread sneg53 show ofNat x.2 + -(ofNat x.1) = -(ofNat x.1 + -(ofNat x.2))54 rw [neg_add_rev, neg_neg, add_comm]5556theorem sread_mul (x y : SInt) : (sread (smul x y) : Shell p) = sread x * sread y := by57 unfold sread smul58 show ofNat (x.1 * y.1 + x.2 * y.2) + -(ofNat (x.1 * y.2 + x.2 * y.1)) =59 (ofNat x.1 + -(ofNat x.2)) * (ofNat y.1 + -(ofNat y.2))60 rw [right_distrib, left_distrib, left_distrib, ← mul_neg, ← neg_mul, neg_mul_neg, ← ofNat_add, ← ofNat_add,61 ← ofNat_mul, ← ofNat_mul, ← ofNat_mul, ← ofNat_mul, neg_add_rev]62 -- a + d + (-b + -c) = a + -b + (-c + d)63 rw [add_assoc, add_assoc]64 refine congrArg (ofNat x.1 * ofNat y.1 + ·) ?_65 rw [← add_assoc, add_comm (ofNat x.2 * ofNat y.2), add_assoc, add_comm (ofNat x.2 * ofNat y.2)]6667theorem sread_norm (x : SInt) : (sread (snorm x) : Shell p) = sread x := by68 unfold sread snorm69 match Nat.decLe x.2 x.1 with70 | .isTrue h =>71 have e : x.2 - x.1 = 0 := FRC.Nat.sub_eq_zero_of_le h72 show ofNat (x.1 - x.2) + -(ofNat (x.2 - x.1)) = ofNat x.1 + -(ofNat x.2)73 rw [e]74 have e0 : (ofNat 0 : Shell p) = 0 := rfl75 rw [e0, neg_zero, add_zero]76 have e1 : x.1 = (x.1 - x.2) + x.2 := (FRC.Nat.sub_add_cancel h).symm77 calc ofNat (x.1 - x.2) = ofNat (x.1 - x.2) + 0 := (add_zero _).symm78 _ = ofNat (x.1 - x.2) + (ofNat x.2 + -(ofNat x.2)) := by rw [add_neg]79 _ = ofNat (x.1 - x.2 + x.2) + -(ofNat x.2) := by rw [← add_assoc, ofNat_add]80 _ = ofNat x.1 + -(ofNat x.2) := by rw [← e1]81 | .isFalse h =>82 have h' : x.1 ≤ x.2 := Nat.le_of_lt (Nat.lt_of_not_le h)83 have e : x.1 - x.2 = 0 := FRC.Nat.sub_eq_zero_of_le h'84 show ofNat (x.1 - x.2) + -(ofNat (x.2 - x.1)) = ofNat x.1 + -(ofNat x.2)85 rw [e]86 have e0 : (ofNat 0 : Shell p) = 0 := rfl87 rw [e0, zero_add]88 have e1 : x.2 = (x.2 - x.1) + x.1 := (FRC.Nat.sub_add_cancel h').symm89 calc (-(ofNat (x.2 - x.1)) : Shell p) = (0 : Shell p) + -(ofNat (x.2 - x.1)) := (zero_add _).symm90 _ = (ofNat x.1 + -(ofNat x.1)) + -(ofNat (x.2 - x.1)) := by rw [add_neg]91 _ = ofNat x.1 + -((ofNat (x.2 - x.1) : Shell p) + ofNat x.1) := by92 rw [add_assoc, neg_add_rev, add_comm (-(ofNat x.1))]93 _ = ofNat x.1 + -(ofNat x.2) := by rw [ofNat_add, ← e1]9495/-- The window bound: both components at most `H`, one of them zero. -/96def SBound (H : Nat) (x : SInt) : Prop := x.1 ≤ H ∧ x.2 ≤ H ∧ (x.1 = 0 ∨ x.2 = 0)9798theorem sneg_bound {H : Nat} {x : SInt} (h : SBound H x) : SBound H (sneg x) :=99 ⟨h.2.1, h.1, match h.2.2 with | Or.inl e => Or.inr e | Or.inr e => Or.inl e⟩100101theorem smul_bound {H : Nat} {x y : SInt} (hx : SBound H x) (hy : SBound H y) : SBound (H * H) (smul x y) := by102 unfold smul103 have b11 := Nat.mul_le_mul hx.1 hy.1104 have b22 := Nat.mul_le_mul hx.2.1 hy.2.1105 have b12 := Nat.mul_le_mul hx.1 hy.2.1106 have b21 := Nat.mul_le_mul hx.2.1 hy.1107 match hx.2.2, hy.2.2 with108 | Or.inl e, Or.inl f =>109 refine ⟨?_, ?_, Or.inr ?_⟩110 · show x.1 * y.1 + x.2 * y.2 ≤ H * H111 rw [e, Nat.zero_mul, Nat.zero_add]; exact b22112 · show x.1 * y.2 + x.2 * y.1 ≤ H * H113 rw [e, f, Nat.zero_mul, Nat.mul_zero]; exact Nat.zero_le _114 · show x.1 * y.2 + x.2 * y.1 = 0115 rw [e, f, Nat.zero_mul, Nat.mul_zero]116 | Or.inl e, Or.inr f =>117 refine ⟨?_, ?_, Or.inl ?_⟩118 · show x.1 * y.1 + x.2 * y.2 ≤ H * H119 rw [e, f, Nat.zero_mul, Nat.mul_zero]; exact Nat.zero_le _120 · show x.1 * y.2 + x.2 * y.1 ≤ H * H121 rw [e, Nat.zero_mul, Nat.zero_add]; exact b21122 · show x.1 * y.1 + x.2 * y.2 = 0123 rw [e, f, Nat.zero_mul, Nat.mul_zero]124 | Or.inr e, Or.inl f =>125 refine ⟨?_, ?_, Or.inl ?_⟩126 · show x.1 * y.1 + x.2 * y.2 ≤ H * H127 rw [e, f, Nat.mul_zero, Nat.zero_mul]; exact Nat.zero_le _128 · show x.1 * y.2 + x.2 * y.1 ≤ H * H129 rw [e, Nat.zero_mul, Nat.add_zero]; exact b12130 · show x.1 * y.1 + x.2 * y.2 = 0131 rw [e, f, Nat.mul_zero, Nat.zero_mul]132 | Or.inr e, Or.inr f =>133 refine ⟨?_, ?_, Or.inr ?_⟩134 · show x.1 * y.1 + x.2 * y.2 ≤ H * H135 rw [e, Nat.zero_mul, Nat.add_zero]; exact b11136 · show x.1 * y.2 + x.2 * y.1 ≤ H * H137 rw [e, f, Nat.mul_zero, Nat.zero_mul]; exact Nat.zero_le _138 · show x.1 * y.2 + x.2 * y.1 = 0139 rw [e, f, Nat.mul_zero, Nat.zero_mul]140141/-- Four window terms of size `M` add to a pair with both components at most `4M`. -/142theorem sum4_bound {M : Nat} {t1 t2 t3 t4 : SInt} (h1 : SBound M t1) (h2 : SBound M t2) (h3 : SBound M t3)143 (h4 : SBound M t4) :144 (sadd (sadd t1 t2) (sadd t3 t4)).1 ≤ 4 * M ∧ (sadd (sadd t1 t2) (sadd t3 t4)).2 ≤ 4 * M := by145 unfold sadd146 rw [four_mul_eq, Nat.add_assoc (M + M) M M]147 exact ⟨Nat.add_le_add (Nat.add_le_add h1.1 h2.1) (Nat.add_le_add h3.1 h4.1),148 Nat.add_le_add (Nat.add_le_add h1.2.1 h2.2.1) (Nat.add_le_add h3.2.1 h4.2.1)⟩149150theorem snorm_bound {M : Nat} {x : SInt} (h1 : x.1 ≤ M) (h2 : x.2 ≤ M) : SBound M (snorm x) := by151 unfold snorm152 refine ⟨Nat.le_trans (Nat.sub_le _ _) h1, Nat.le_trans (Nat.sub_le _ _) h2, ?_⟩153 match Nat.decLe x.2 x.1 with154 | .isTrue h => exact Or.inr (FRC.Nat.sub_eq_zero_of_le h)155 | .isFalse h => exact Or.inl (FRC.Nat.sub_eq_zero_of_le (Nat.le_of_lt (Nat.lt_of_not_le h)))156157/-- The signed window law: two canonical pairs of size `M`, `2M < p`, with the same reading are equal. -/158theorem sread_inj {M : Nat} (hM : 2 * M < p) {x y : SInt} (hx : SBound M x) (hy : SBound M y)159 (h : (sread x : Shell p) = sread y) : x = y := by160 unfold sread at h161 have h' : (ofNat (x.1 + y.2) : Shell p) = ofNat (y.1 + x.2) := by162 rw [← ofNat_add, ← ofNat_add]163 calc ofNat x.1 + ofNat y.2 = ofNat x.1 + -(ofNat x.2) + (ofNat x.2 + ofNat y.2) := by164 rw [add_assoc, ← add_assoc (-(ofNat x.2)), neg_add, zero_add]165 _ = ofNat y.1 + -(ofNat y.2) + (ofNat x.2 + ofNat y.2) := by rw [h]166 _ = ofNat y.1 + ofNat x.2 := by167 rw [add_assoc, add_comm (ofNat x.2), ← add_assoc (-(ofNat y.2)), neg_add, zero_add]168 have hv := val_injective h'169 rw [val_ofNat, val_ofNat] at hv170 have l1 : x.1 + y.2 < p := Nat.lt_of_le_of_lt (Nat.add_le_add hx.1 hy.2.1) (Nat.two_mul M ▸ hM)171 have l2 : y.1 + x.2 < p := Nat.lt_of_le_of_lt (Nat.add_le_add hy.1 hx.2.1) (Nat.two_mul M ▸ hM)172 rw [FRC.Nat.mod_eq_of_lt l1, FRC.Nat.mod_eq_of_lt l2] at hv173 -- hv : x.1 + y.2 = y.1 + x.2174 match hx.2.2, hy.2.2 with175 | Or.inl e, Or.inl f =>176 rw [e, f, Nat.zero_add, Nat.zero_add] at hv177 exact prod_ext (e.trans f.symm) hv.symm178 | Or.inl e, Or.inr f =>179 rw [e, f, Nat.zero_add] at hv180 -- hv : 0 = y.1 + x.2181 have hy1 : y.1 = 0 := Nat.eq_zero_of_add_eq_zero_right hv.symm182 have hx2 : x.2 = 0 := Nat.eq_zero_of_add_eq_zero_left hv.symm183 exact prod_ext (e.trans hy1.symm) (hx2.trans f.symm)184 | Or.inr e, Or.inl f =>185 rw [e, f, Nat.zero_add] at hv186 -- hv : x.1 + y.2 = 0187 have hx1 : x.1 = 0 := Nat.eq_zero_of_add_eq_zero_right hv188 have hy2 : y.2 = 0 := Nat.eq_zero_of_add_eq_zero_left hv189 exact prod_ext (hx1.trans f.symm) (e.trans hy2.symm)190 | Or.inr e, Or.inr f =>191 rw [e, f, Nat.add_zero, Nat.add_zero] at hv192 exact prod_ext hv (e.trans f.symm)193194/-- A framed quaternion with signed window coordinates. -/195structure IQuat where196 a : SInt197 b : SInt198 c : SInt199 d : SInt200201/-- The Hamilton product on the window pairs, the same formula. -/202def IQuat.mul (q r : IQuat) : IQuat :=203 ⟨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))),204 sadd (sadd (smul q.a r.b) (smul q.b r.a)) (sadd (smul q.c r.d) (sneg (smul q.d r.c))),205 sadd (sadd (smul q.a r.c) (sneg (smul q.b r.d))) (sadd (smul q.c r.a) (smul q.d r.b)),206 sadd (sadd (smul q.a r.d) (smul q.b r.c)) (sadd (sneg (smul q.c r.b)) (smul q.d r.a))⟩207208def IQuat.read (q : IQuat) : Quat p := ⟨sread q.a, sread q.b, sread q.c, sread q.d⟩209def IQuat.norm (q : IQuat) : IQuat := ⟨snorm q.a, snorm q.b, snorm q.c, snorm q.d⟩210def QBound (H : Nat) (q : IQuat) : Prop := SBound H q.a ∧ SBound H q.b ∧ SBound H q.c ∧ SBound H q.d211212theorem 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 := by213 cases q; cases r; cases ha; cases hb; cases hc; cases hd; rfl214215/-- 1:E6, exact composition — the reading of the integer product is the product of the readings. -/216theorem read_mul (q r : IQuat) : ((IQuat.mul q r).read : Quat p) = Quat.mul q.read r.read := by217 unfold IQuat.mul IQuat.read Quat.mul218 rw [sread_add, sread_add, sread_add, sread_add, sread_add, sread_add, sread_add, sread_add, sread_add,219 sread_add, sread_add, sread_add, sread_neg, sread_neg, sread_neg, sread_neg, sread_neg, sread_neg,220 sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul,221 sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul, sread_mul]222223theorem read_norm (q : IQuat) : (q.norm.read : Quat p) = q.read := by224 unfold IQuat.norm IQuat.read225 rw [sread_norm, sread_norm, sread_norm, sread_norm]226227theorem norm_bound {H : Nat} {q r : IQuat} (hq : QBound H q) (hr : QBound H r) :228 QBound (4 * (H * H)) (IQuat.mul q r).norm := by229 have m := fun {x y : SInt} (hx : SBound H x) (hy : SBound H y) => smul_bound hx hy230 refine ⟨?_, ?_, ?_, ?_⟩231 · 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))232 (sneg_bound (m hq.2.2.2 hr.2.2.2))233 exact snorm_bound this.1 this.2234 · 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))235 exact snorm_bound this.1 this.2236 · 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)237 exact snorm_bound this.1 this.2238 · 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)239 exact snorm_bound this.1 this.2240241/-- 1:E6, the finitary clause — framed quaternions with window coordinates `≤ H`, read in a shell `p > 8H²`,242compose exactly: the product of the readings is the reading of the integer product; that product's243coordinates lie in the window `4H²`; and the reading determines it among the window's quaternions. -/244theorem quaternion_window {H : Nat} (hH : 8 * (H * H) < p) {q r : IQuat} (hq : QBound H q) (hr : QBound H r) :245 ((IQuat.mul q r).read : Quat p) = Quat.mul q.read r.read ∧246 QBound (4 * (H * H)) (IQuat.mul q r).norm ∧247 ∀ s : IQuat, QBound (4 * (H * H)) s → (s.read : Quat p) = (IQuat.mul q r).read → s = (IQuat.mul q r).norm := by248 refine ⟨read_mul q r, norm_bound hq hr, ?_⟩249 intro s hs he250 have hn := norm_bound hq hr251 have hM : 2 * (4 * (H * H)) < p := by rw [← Nat.mul_assoc]; exact hH252 rw [← read_norm (IQuat.mul q r)] at he253 unfold IQuat.read at he254 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))255 (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))256257/-! ## 1:E7 — the Lie-algebra layer, one axis -/258259/-- 1:E7, conjugation keeps a pure quaternion pure: the scalar part of `q x q̄` vanishes. -/260theorem rot_pure (q x : Quat p) (hx : x.a = 0) : (Quat.conjBy q x).a = 0 := by261 rw [Quat.pure_eq hx]262 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)263264/-- 1:E7, the Cayley form cleared of the norm: for `q = a + v` and a pure `x`, the conjugate `y = q x q̄` satisfies265`(aI − S_v) y = N(q) (aI + S_v) x`, where `S_v x = v × x`. -/266theorem rot_cayley (q x : Quat p) (hx : x.a = 0) :267 Quat.add (Quat.smul q.a (Quat.conjBy q x)) (Quat.neg (Quat.cross (Quat.vec q) (Quat.conjBy q x))) =268 Quat.smul (Quat.nrm q) (Quat.add (Quat.smul q.a x) (Quat.cross (Quat.vec q) x)) := by269 rw [Quat.pure_eq hx]270 exact QR.sound (look [q.a, q.b, q.c, q.d, x.b, x.c, x.d])271 (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)))))272 (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)273274/-- 1:E7, 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²`. -/275theorem half_turn (v x : Quat p) (hv : v.a = 0) (hx : x.a = 0) :276 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))) := by277 rw [Quat.pure_eq hv, Quat.pure_eq hx]278 exact QR.sound (look [v.b, v.c, v.d, x.b, x.c, x.d])279 (QR.conjBy (QR.pv 0) (QR.pv 3))280 (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)281282/-- 1:E7, the key identity of uniqueness: with `w = a z − v × z`, `a (a² + N(v)) z = a² w + a (v × w) + (v · w) v`. -/283theorem cayley_key (a : Shell p) (v z : Quat p) (hv : v.a = 0) (hz : z.a = 0) :284 Quat.smul (a * (a * a + Quat.dot v v)) z =285 Quat.add (Quat.add (Quat.smul (a * a) (Quat.add (Quat.smul a z) (Quat.neg (Quat.cross v z))))286 (Quat.smul a (Quat.cross v (Quat.add (Quat.smul a z) (Quat.neg (Quat.cross v z))))))287 (Quat.smul (Quat.dot v (Quat.add (Quat.smul a z) (Quat.neg (Quat.cross v z)))) v) := by288 rw [Quat.pure_eq hv, Quat.pure_eq hz]289 exact QR.sound (look [a, v.b, v.c, v.d, z.b, z.c, z.d])290 (QR.smul (.mul (.var 0) (.add (.mul (.var 0) (.var 0)) (QR.dot (QR.pv 1) (QR.pv 1)))) (QR.pv 4))291 (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)))))292 (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)))))))293 (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)294295theorem add_neg_q (q : Quat p) : Quat.add q (Quat.neg q) = ⟨0, 0, 0, 0⟩ :=296 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)297298theorem key_zero (a : Shell p) (v : Quat p) :299 Quat.add (Quat.add (Quat.smul (a * a) ⟨0, 0, 0, 0⟩) (Quat.smul a (Quat.cross v ⟨0, 0, 0, 0⟩)))300 (Quat.smul (Quat.dot v ⟨0, 0, 0, 0⟩) v) = ⟨0, 0, 0, 0⟩ :=301 QR.sound (look [a, v.a, v.b, v.c, v.d])302 (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⟩)))303 (QR.smul (QR.dot (QR.v 1) ⟨.zero, .zero, .zero, .zero⟩) (QR.v 1))) ⟨.zero, .zero, .zero, .zero⟩ (by decide +kernel)304305/-- 1:E7, `aI − S_v` is injective on pure quaternions when `a ≠ 0` and `a² + N(v) ≠ 0` (a field shell). -/306theorem 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)307 (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⟩ := by308 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 _309 have key := cayley_key a v z hv hz310 rw [hw, key_zero] at key311 have hc : a * (a * a + Quat.dot v v) ≠ 0 := fun e =>312 match F.mul_eq_zero e with313 | .inl e1 => ha e1314 | .inr e2 => hn e2315 have comp : ∀ t : Shell p, a * (a * a + Quat.dot v v) * t = 0 → t = 0 := fun t e =>316 match F.mul_eq_zero e with317 | .inl e1 => absurd e1 hc318 | .inr e2 => e2319 exact Quat.ext4 hz (comp _ (congrArg Quat.b key)) (comp _ (congrArg Quat.c key)) (comp _ (congrArg Quat.d key))320321/-! ## 1:E8 — the Lie-algebra layer, two axes and range -/322323/-- 1:E8, the product of two Gibbs quaternions: `(1 + u)(1 + w) = (1 − u·w) + (u + w + u × w)` for pure `u`, `w`. -/324theorem one_add_mul (u w : Quat p) (hu : u.a = 0) (hw : w.a = 0) :325 Quat.mul (Quat.add (Quat.sc 1) u) (Quat.add (Quat.sc 1) w) =326 Quat.add (Quat.sc (1 + -(Quat.dot u w))) (Quat.add (Quat.add u w) (Quat.cross u w)) := by327 rw [Quat.pure_eq hu, Quat.pure_eq hw]328 exact QR.sound (look [u.b, u.c, u.d, w.b, w.c, w.d])329 (QR.mul (QR.add (QR.sc .one) (QR.pv 0)) (QR.add (QR.sc .one) (QR.pv 3)))330 (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)331332/-- 1:E8, the bracket: `uw − wu = 2 u × w` for pure `u`, `w`. -/333theorem bracket (u w : Quat p) (hu : u.a = 0) (hw : w.a = 0) :334 Quat.add (Quat.mul u w) (Quat.neg (Quat.mul w u)) = Quat.add (Quat.cross u w) (Quat.cross u w) := by335 rw [Quat.pure_eq hu, Quat.pure_eq hw]336 exact QR.sound (look [u.b, u.c, u.d, w.b, w.c, w.d])337 (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)338339/-- 1:E8, conjugation is multiplicative: `(qr) x (qr)‾ = q (r x r̄) q̄`. -/340theorem rot_mul (q r x : Quat p) : Quat.conjBy (Quat.mul q r) x = Quat.conjBy q (Quat.conjBy r x) :=341 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))342 (QR.conjBy (QR.v 0) (QR.conjBy (QR.v 4) (QR.v 8))) (by decide +kernel)343344/-- 1:E8, 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. -/345theorem rot_smul (s : Shell p) (q x : Quat p) :346 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 :=347 ⟨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))348 (QR.smul (.mul (.var 0) (.var 0)) (QR.conjBy (QR.v 1) (QR.v 5))) (by decide +kernel),349 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)⟩350351/-- 1:E8, the half-turn case: at `u · w = 1` the product `(1 + u)(1 + w)` is the pure quaternion `u + w + u × w`. -/352theorem one_add_mul_half (u w : Quat p) (hu : u.a = 0) (hw : w.a = 0) (h1 : Quat.dot u w = 1) :353 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)) := by354 rw [one_add_mul u w hu hw, h1, add_neg]355356/-- 1:E7, the sign: `ρ_{−q} = ρ_q` (`(−q) x (−q)‾ = q x q̄`, `N(−q) = N(q)`); the window rotations of an axis come in357pairs `±(a, t)`, which bounds them by `2H² + 2H` (`FRC.Algebra.card_image_le_of_neg`). -/358theorem rot_neg (q x : Quat p) : Quat.conjBy (Quat.neg q) x = Quat.conjBy q x ∧ Quat.nrm (Quat.neg q) = Quat.nrm q :=359 ⟨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),360 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)⟩361362theorem smul_sc_add (s s' : Shell p) (m : Quat p) :363 Quat.smul s (Quat.add (Quat.sc 1) (Quat.smul s' m)) = Quat.add (Quat.sc s) (Quat.smul (s * s') m) :=364 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))))365 (QR.add (QR.sc (.var 0)) (QR.smul (.mul (.var 0) (.var 1)) (QR.v 2))) (by decide +kernel)366367theorem smul_one_q (m : Quat p) : Quat.smul 1 m = m :=368 QR.sound (look [m.a, m.b, m.c, m.d]) (QR.smul .one (QR.v 0)) (QR.v 0) (by decide +kernel)369370theorem smul_smul_q (s t : Shell p) (m : Quat p) : Quat.smul s (Quat.smul t m) = Quat.smul (s * t) m :=371 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)372373theorem conjBy_smul (q y : Quat p) (t : Shell p) : Quat.conjBy q (Quat.smul t y) = Quat.smul t (Quat.conjBy q y) :=374 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)))375 (QR.smul (.var 4) (QR.conjBy (QR.v 0) (QR.v 5))) (by decide +kernel)376377theorem inv_chain (nu nw s nc Nu Nw Nc : Shell p) (hu : Nu * nu = 1) (hw : Nw * nw = 1) (hc : Nc * nc = 1)378 (hN : Nu * Nw = s * s * Nc) : nu * nw * (s * s) = nc := by379 have e1 : nu * nw * (s * s) = nc * (nu * nw * (s * s * Nc)) := by380 calc nu * nw * (s * s) = nu * nw * (s * s) * (Nc * nc) := by rw [hc, mul_one]381 _ = nc * (nu * nw * (s * s * Nc)) :=382 RE.sound (look [nu, nw, s, nc, Nc])383 (.mul (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 2))) (.mul (.var 4) (.var 3)))384 (.mul (.var 3) (.mul (.mul (.var 0) (.var 1)) (.mul (.mul (.var 2) (.var 2)) (.var 4)))) (by decide +kernel)385 have e2 : nu * nw * (Nu * Nw) = (Nu * nu) * (Nw * nw) :=386 RE.sound (look [nu, nw, Nu, Nw]) (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))387 (.mul (.mul (.var 2) (.var 0)) (.mul (.var 3) (.var 1))) (by decide +kernel)388 rw [e1, ← hN, e2, hu, hw, mul_one, mul_one]389390/-- 1:E8, the composition law: for pure `u`, `w` with `1 + N(u)`, `1 + N(w)`, `1 − u·w` and `1 + N(u∘w)` invertible391(inverses `nu`, `nw`, `s'`, `nc`), `ρ_{1+u} ρ_{1+w} = ρ_{1+u∘w}` with `u∘w = (u + w + u × w)/(1 − u·w)`; here392`ρ_q x = N(q)⁻¹ q x q̄`. -/393theorem compose (u w x : Quat p) (hu : u.a = 0) (hw : w.a = 0) (s' nu nw nc : Shell p)394 (hs : (1 + -(Quat.dot u w)) * s' = 1)395 (hnu : Quat.nrm (Quat.add (Quat.sc 1) u) * nu = 1) (hnw : Quat.nrm (Quat.add (Quat.sc 1) w) * nw = 1)396 (hnc : Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s' (Quat.add (Quat.add u w) (Quat.cross u w)))) * nc = 1) :397 Quat.smul nu (Quat.conjBy (Quat.add (Quat.sc 1) u) (Quat.smul nw (Quat.conjBy (Quat.add (Quat.sc 1) w) x))) =398 Quat.smul nc (Quat.conjBy (Quat.add (Quat.sc 1) (Quat.smul s' (Quat.add (Quat.add u w) (Quat.cross u w)))) x) := by399 have hP : Quat.mul (Quat.add (Quat.sc 1) u) (Quat.add (Quat.sc 1) w) =400 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)))) := by401 rw [smul_sc_add, hs, smul_one_q, one_add_mul u w hu hw]402 have hN : Quat.nrm (Quat.add (Quat.sc 1) u) * Quat.nrm (Quat.add (Quat.sc 1) w) =403 (1 + -(Quat.dot u w)) * (1 + -(Quat.dot u w)) *404 Quat.nrm (Quat.add (Quat.sc 1) (Quat.smul s' (Quat.add (Quat.add u w) (Quat.cross u w)))) := by405 rw [← nrm_mul, hP, (rot_smul _ _ x).2]406 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]407408theorem add_cancel_q {r m : Quat p} (h : Quat.add r m = r) : m = ⟨0, 0, 0, 0⟩ := by409 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])410 exact Quat.ext4 (c _ _ (congrArg Quat.a h)) (c _ _ (congrArg Quat.b h)) (c _ _ (congrArg Quat.c h)) (c _ _ (congrArg Quat.d h))411412theorem cayley_trivial_id (q x : Quat p) (hx : x.a = 0) :413 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))))414 (Quat.smul (1 + 1) (Quat.smul (Quat.nrm q) (Quat.cross (Quat.vec q) x))) =415 Quat.smul (Quat.nrm q) (Quat.add (Quat.smul q.a x) (Quat.cross (Quat.vec q) x)) := by416 rw [Quat.pure_eq hx]417 exact QR.sound (look [q.a, q.b, q.c, q.d, x.b, x.c, x.d])418 (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)))))419 (QR.smul (.add .one .one) (QR.smul (QR.nrm (QR.v 0)) (QR.cross (QR.vec (QR.v 0)) (QR.pv 4)))))420 (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)421422/-- 1:E7, the kernel: on a field shell, a rotation `ρ_q` (`N(q) ≠ 0`) that fixes every pure quaternion has `q` a423scalar — so `a + t v ↦ ρ_{a+tv}` is injective on the pairs modulo the scalars, and the axis group of424`FRC.Algebra.axis_group` is the rotation group of the axis. -/425theorem rot_trivial {κ : Nat} {g : Shell p} (F : Frame p κ g) (q : Quat p) (hN : Quat.nrm q ≠ 0)426 (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 := by427 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⟩ := by428 intro x hx429 have E := rot_cayley q x hx430 rw [h x hx] at E431 have I := cayley_trivial_id q x hx432 rw [← E] at I433 exact add_cancel_q I434 have h2 : (1 + 1 : Shell p) ≠ 0 := by rw [← two_eq_one_add_one]; exact F.two_ne_zero435 have z : ∀ t : Shell p, (1 + 1) * (Quat.nrm q * t) = 0 → t = 0 := fun t e =>436 match F.mul_eq_zero e with437 | .inl e1 => absurd e1 h2438 | .inr e2 => match F.mul_eq_zero e2 with439 | .inl e3 => absurd e3 hN440 | .inr e4 => e4441 have kb := key ⟨0, 1, 0, 0⟩ rfl442 have kc := key ⟨0, 0, 1, 0⟩ rfl443 have hd : q.d = 0 := z _ (by444 have := congrArg Quat.c kb445 simp only [Quat.smul, Quat.cross, Quat.vec] at this446 rw [mul_one, mul_zero, neg_zero, add_zero] at this; exact this)447 have hcneg : -q.c = 0 := z _ (by448 have := congrArg Quat.d kb449 simp only [Quat.smul, Quat.cross, Quat.vec] at this450 rw [mul_zero, mul_one] at this451 rw [zero_add] at this; exact this)452 have hb : q.b = 0 := z _ (by453 have := congrArg Quat.d kc454 simp only [Quat.smul, Quat.cross, Quat.vec] at this455 rw [mul_one, mul_zero, neg_zero, add_zero] at this; exact this)456 refine ⟨hb, ?_, hd⟩457 rw [← neg_neg q.c, hcneg, neg_zero]458459end Frame460end Shell461end FRC462463namespace FRC.Algebra464-- Ledger predicates of 1-algebra (generated by make_predicates.py from docs/1-algebra/1-algebra-ledger.json; edit the ledger, not this section)465set_option linter.defProp false in466/-- 1:E6 (p01030) — Continuous symmetry, the non-abelian case resolved by the window: the framed quaternions $W_H^{4}$, read in a shell $\p>8H^{2}$, compose exactly (products land in $W_{4H^{2}}$); normalised, they are an $\varepsilon$-net of $SO(3)$ with $\varepsilon\le2\arcsin(1/H)$ (round $Hs$ to the lattice). At $H=3$, $\p=73$: $38.9^\circ<\varepsilon_0$, finer than any finite subgroup; measured $30.0^\circ$. -/467def p01030 := And.intro @FRC.Shell.Frame.quaternion_window (@FRC.Shell.Frame.read_mul)468/-- 1:E7 (p01032) — The Lie-algebra layer, one axis: on a shell $\p>8H^{2}$, for $q=a+v\in W_H^{4}$ with $v\ne0$, the rotation $\rho_q\colon x\mapsto qxq^{-1}$ is the Cayley step (8:C3) of the self-adjoint $\eta S_v$ (E2's $\eta$, $S_vx=v\times x$, $N(v)=v\cdot v$) at $\alpha=\eta/(\nu a)$, and the half-turn $U_\infty=I+2N(v)^{-1}S_v^{2}$ at $a=0$. With $U_\infty$ these steps form a cyclic group of order $\p-\bigl(\tfrac{N(v)}{\p}\bigr)$ containing every iterate; at most $2H^{2}+2H$ of its elements are window rotations. -/469theorem p01032 : (∀ {p : Nat} [FRC.Pos p] (q x : FRC.Shell.Frame.Quat p), x.a = (0 : FRC.Shell p) → (FRC.Shell.Frame.Quat.smul q.a (q.conjBy x)).add (q.vec.cross (q.conjBy x)).neg = FRC.Shell.Frame.Quat.smul q.nrm ((FRC.Shell.Frame.Quat.smul q.a x).add (q.vec.cross x))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {a : FRC.Shell p} {v z : FRC.Shell.Frame.Quat p}, v.a = (0 : FRC.Shell p) → z.a = (0 : FRC.Shell p) → a ≠ (0 : FRC.Shell p) → a * a + v.dot v ≠ (0 : FRC.Shell p) → FRC.Shell.Frame.Quat.smul a z = v.cross z → z = { a := (0 : FRC.Shell p), b := (0 : FRC.Shell p), c := (0 : FRC.Shell p), d := (0 : FRC.Shell p) }) ∧ (∀ {p : Nat} [FRC.Pos p] (v x : FRC.Shell.Frame.Quat p), v.a = (0 : FRC.Shell p) → x.a = (0 : FRC.Shell p) → v.conjBy x = (FRC.Shell.Frame.Quat.smul v.nrm x).add ((v.cross (v.cross x)).add (v.cross (v.cross x)))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (q : FRC.Shell.Frame.Quat p), q.nrm ≠ (0 : FRC.Shell p) → (∀ (x : FRC.Shell.Frame.Quat p), x.a = (0 : FRC.Shell p) → q.conjBy x = FRC.Shell.Frame.Quat.smul q.nrm x) → q.b = (0 : FRC.Shell p) ∧ q.c = (0 : FRC.Shell p) ∧ q.d = (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] (q x : FRC.Shell.Frame.Quat p), q.neg.conjBy x = q.conjBy x ∧ q.neg.nrm = q.nrm :=470 And.intro @FRC.Shell.Frame.rot_cayley (And.intro @FRC.Shell.Frame.cayley_inj (And.intro @FRC.Shell.Frame.half_turn (And.intro @FRC.Shell.Frame.rot_trivial (@FRC.Shell.Frame.rot_neg))))471/-- 1:E8 (p01033) — The Lie-algebra layer, two axes and range: for pure quaternions $u,w$ with $1+N(u)$, $1+N(w)$ and $1-u\cdot w$ nonzero, $\rho_{1+u}\rho_{1+w}=\rho_{1+u\circ w}$ with $u\circ w=(u+w+u\times w)/(1-u\cdot w)$, the bracket being $[u,w]=2u\times w$; at $u\cdot w=1$ the product is the half-turn about $u+w+u\times w$. The entries of $q^{m}$, $q\in W_H^{4}$, are at most $(2H)^{m}$, and $q^{m}$ reads back from the shell iff $2\|q^{m}\|_\infty<\p$ (D2). -/472theorem p01033 : (∀ {p : Nat} [FRC.Pos p] (u w x : FRC.Shell.Frame.Quat p), u.a = (0 : FRC.Shell p) → w.a = (0 : FRC.Shell p) → ∀ (s' nu nw nc : FRC.Shell p), ((1 : FRC.Shell p) + -u.dot w) * s' = (1 : FRC.Shell p) → ((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add u).nrm * nu = (1 : FRC.Shell p) → ((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add w).nrm * nw = (1 : FRC.Shell p) → ((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add (FRC.Shell.Frame.Quat.smul s' ((u.add w).add (u.cross w)))).nrm * nc = (1 : FRC.Shell p) → FRC.Shell.Frame.Quat.smul nu (((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add u).conjBy (FRC.Shell.Frame.Quat.smul nw (((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add w).conjBy x))) = FRC.Shell.Frame.Quat.smul nc (((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add (FRC.Shell.Frame.Quat.smul s' ((u.add w).add (u.cross w)))).conjBy x)) ∧ (∀ {p : Nat} [FRC.Pos p] (u w : FRC.Shell.Frame.Quat p), u.a = (0 : FRC.Shell p) → w.a = (0 : FRC.Shell p) → ((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add u).mul ((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add w) = (FRC.Shell.Frame.Quat.sc ((1 : FRC.Shell p) + -u.dot w)).add ((u.add w).add (u.cross w))) ∧ (∀ {p : Nat} [FRC.Pos p] (u w : FRC.Shell.Frame.Quat p), u.a = (0 : FRC.Shell p) → w.a = (0 : FRC.Shell p) → u.dot w = (1 : FRC.Shell p) → ((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add u).mul ((FRC.Shell.Frame.Quat.sc (1 : FRC.Shell p)).add w) = (FRC.Shell.Frame.Quat.sc (0 : FRC.Shell p)).add ((u.add w).add (u.cross w))) ∧ (∀ {p : Nat} [FRC.Pos p] (u w : FRC.Shell.Frame.Quat p), u.a = (0 : FRC.Shell p) → w.a = (0 : FRC.Shell p) → (u.mul w).add (w.mul u).neg = (u.cross w).add (u.cross w)) ∧ (∀ {p : Nat} [FRC.Pos p] (q r x : FRC.Shell.Frame.Quat p), (q.mul r).conjBy x = q.conjBy (r.conjBy x)) ∧ ∀ {p : Nat} [FRC.Pos p] (q r : FRC.Shell.Frame.Quat p), (q.mul r).nrm = q.nrm * r.nrm :=473 And.intro @FRC.Shell.Frame.compose (And.intro @FRC.Shell.Frame.one_add_mul (And.intro @FRC.Shell.Frame.one_add_mul_half (And.intro @FRC.Shell.Frame.bracket (And.intro @FRC.Shell.Frame.rot_mul (@FRC.Shell.Frame.nrm_mul)))))474-- end ledger predicates475end FRC.Algebra476