Theme/Quadratic.lean — FrcCore

1import FrcCore.Ring23/-!4# FrcCore.Theme.Quadratic — the quadratic extension of the shell, frame-free (the extension theme)56`FRC.Extension.Ext p ν`: the elements `a + b w` of `𝔽_p[w]/(w² − ν)` on components, with addition, the product7`(a + bw)(c + dw) = (ac + νbd) + (ad + bc)w`, powers, Frobenius conjugation, the trace and the norm `N = a² − νb²`;8`z z̄ = N(z)`, conjugation is a ring map and an involution, the norm scales by squares, and on the circle `N = 1` the9conjugate is the inverse. One structure for 8-dirac's coefficient field and 20-rh's extension, which keep their old names10as aliases. Split from `Theme/Extension.lean` by the ledger migration (task LM24), every name unchanged, with the ring11laws of `Ext` and the multiplicativity of the norm, decided by the normaliser (`Ring.lean`); the frame-dependent12`fixed_conj`, the quaternions and the Lorentzian plane stay in `Theme/Extension.lean`. No axioms.13-/1415namespace FRC.Extension1617open FRC.Shell1819variable {p : Nat} [Pos p]202122/-- 8:B1 — an element `a + b w` of the coefficient field, on components. -/23structure Ext (p : Nat) [Pos p] (ν : Shell p) where24  re : Shell p25  im : Shell p2627namespace Ext28variable {ν : Shell p}2930theorem ext {z z' : Ext p ν} (h1 : z.re = z'.re) (h2 : z.im = z'.im) : z = z' := by31  cases z; cases z'; cases h1; cases h2; rfl3233theorem re_congr {a b : Ext p ν} (h : a = b) : a.re = b.re := by cases h; rfl34theorem im_congr {a b : Ext p ν} (h : a = b) : a.im = b.im := by cases h; rfl3536instance : DecidableEq (Ext p ν) := fun a b =>37  if h1 : a.re = b.re then38    if h2 : a.im = b.im then isTrue (ext h1 h2) else isFalse (fun e => h2 (by cases e; rfl))39  else isFalse (fun e => h1 (by cases e; rfl))4041/-- The base field inside `K`. -/42def ofShell (a : Shell p) : Ext p ν := ⟨a, 0⟩43/-- The adjoined root `w`, `w² = ν`. -/44def w : Ext p ν := ⟨0, 1⟩45instance (n : Nat) : OfNat (Ext p ν) n := ⟨ofShell (OfNat.ofNat n)⟩46instance : Add (Ext p ν) := ⟨fun z z' => ⟨z.re + z'.re, z.im + z'.im⟩⟩47instance : Neg (Ext p ν) := ⟨fun z => ⟨-z.re, -z.im⟩⟩48instance : Mul (Ext p ν) := ⟨fun z z' => ⟨z.re * z'.re + ν * (z.im * z'.im), z.re * z'.im + z.im * z'.re⟩⟩49/-- Frobenius conjugation `a + b w ↦ a − b w`. -/50def conj (z : Ext p ν) : Ext p ν := ⟨z.re, -z.im⟩51/-- The trace `Tr(a + b w) = 2a`. -/52def trace (z : Ext p ν) : Shell p := z.re + z.re53/-- The norm `N(z) = z z̄ = a² − ν b²`. -/54def norm (z : Ext p ν) : Shell p := z.re * z.re + -(ν * (z.im * z.im))55/-- Powers by structural recursion. -/56def pow (z : Ext p ν) : Nat → Ext p ν57  | 0 => 158  | n + 1 => pow z n * z59instance : Pow (Ext p ν) Nat := ⟨pow⟩6061theorem mul_re (z z' : Ext p ν) : (z * z').re = z.re * z'.re + ν * (z.im * z'.im) := rfl62theorem mul_im (z z' : Ext p ν) : (z * z').im = z.re * z'.im + z.im * z'.re := rfl63theorem ofShell_re (a : Shell p) : (ofShell a : Ext p ν).re = a := rfl64theorem ofShell_im (a : Shell p) : (ofShell a : Ext p ν).im = 0 := rfl65theorem conj_re (z : Ext p ν) : (conj z).re = z.re := rfl66theorem conj_im (z : Ext p ν) : (conj z).im = -z.im := rfl6768/-- 8:A2 — `w² = ν`. -/69theorem w_sq : (w : Ext p ν) * w = ofShell ν :=70  ext (by show 0 * 0 + ν * (1 * 1) = ν; rw [Shell.zero_mul, Shell.one_mul, Shell.mul_one, Shell.zero_add])71      (by show 0 * 1 + 1 * 0 = 0; rw [Shell.zero_mul, Shell.mul_zero, Shell.zero_add])7273/-- 8:A2 — the norm is the product with the conjugate: `z z̄ = N(z)`, a base-field element. -/74theorem mul_conj (z : Ext p ν) : z * conj z = ofShell (norm z) :=75  ext (by show z.re * z.re + ν * (z.im * -z.im) = z.re * z.re + -(ν * (z.im * z.im))76          rw [← Shell.mul_neg, ← Shell.mul_neg])77      (by show z.re * -z.im + z.im * z.re = 078          rw [← Shell.mul_neg, Shell.mul_comm z.im z.re, Shell.neg_add])7980/-- 8:A2 — conjugation is multiplicative (the Frobenius involution is a ring map). -/81theorem conj_mul (z z' : Ext p ν) : conj (z * z') = conj z * conj z' :=82  ext (by show z.re * z'.re + ν * (z.im * z'.im) = z.re * z'.re + ν * (-z.im * -z'.im)83          rw [Shell.neg_mul_neg])84      (by show -(z.re * z'.im + z.im * z'.re) = z.re * -z'.im + -z.im * z'.re85          rw [Shell.neg_add_rev, ← Shell.mul_neg, ← Shell.neg_mul])8687/-- 8:B6 — norm growth: `N(c z) = c² N(z)` for every base residue `c`; one chronon of drive multiplies every88norm by `g²`, a square. -/89theorem norm_scale (c : Shell p) (z : Ext p ν) : norm (ofShell c * z) = c * c * norm z := by90  unfold norm91  rw [mul_re, mul_im, ofShell_re, ofShell_im, Shell.zero_mul, Shell.mul_zero, Shell.add_zero,92    Shell.zero_mul, Shell.add_zero, FRC.Shell.mul_mul_mul_comm, FRC.Shell.mul_mul_mul_comm c z.im c z.im,93    Shell.mul_left_comm ν (c * c), Shell.left_distrib, ← Shell.mul_neg]9495/-- 20:B9 — conjugation is an involution. -/96theorem conj_conj (z : Ext p ν) : conj (conj z) = z := ext rfl (Shell.neg_neg z.im)9798/-- 20:B6 — on the circle `N(z) = 1` the conjugate is the inverse: `z z̄ = 1`. -/99theorem conj_inv_of_norm_one (z : Ext p ν) (hz : norm z = 1) : z * conj z = 1 := by100  rw [mul_conj, hz]; rfl101102103104/-! ## Ring laws and the norm's multiplicativity (task LM24; the identities decided by `Ring.lean`'s normaliser) -/105106theorem ofShell_mul_eq (c : Shell p) (z : Ext p ν) : ofShell c * z = ⟨c * z.re, c * z.im⟩ :=107  ext (by show c * z.re + ν * (0 * z.im) = c * z.re; rw [Shell.zero_mul, Shell.mul_zero, Shell.add_zero])108      (by show c * z.im + 0 * z.re = c * z.im; rw [Shell.zero_mul, Shell.add_zero])109110theorem ofShell_mul (a b : Shell p) : (ofShell a : Ext p ν) * ofShell b = ofShell (a * b) := by111  rw [ofShell_mul_eq]; exact ext rfl (Shell.mul_zero a)112113theorem one_mul (z : Ext p ν) : (1 : Ext p ν) * z = z := by114  show ofShell 1 * z = z115  rw [ofShell_mul_eq, Shell.one_mul, Shell.one_mul]116117theorem mul_comm (z z' : Ext p ν) : z * z' = z' * z :=118  ext (by show z.re * z'.re + ν * (z.im * z'.im) = z'.re * z.re + ν * (z'.im * z.im)119          rw [Shell.mul_comm z.re, Shell.mul_comm z.im])120      (by show z.re * z'.im + z.im * z'.re = z'.re * z.im + z'.im * z.re121          rw [Shell.add_comm, Shell.mul_comm z.im, Shell.mul_comm z.re])122123theorem mul_assoc (z z' z'' : Ext p ν) : z * z' * z'' = z * (z' * z'') :=124  ext (Shell.Frame.RE.sound (Shell.Frame.look [ν, z.re, z.im, z'.re, z'.im, z''.re, z''.im])125        (.add (.mul (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4)))) (.var 5)) (.mul (.var 0) (.mul (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3))) (.var 6))))126        (.add (.mul (.var 1) (.add (.mul (.var 3) (.var 5)) (.mul (.var 0) (.mul (.var 4) (.var 6))))) (.mul (.var 0) (.mul (.var 2) (.add (.mul (.var 3) (.var 6)) (.mul (.var 4) (.var 5))))))127        (by decide +kernel))128      (Shell.Frame.RE.sound (Shell.Frame.look [ν, z.re, z.im, z'.re, z'.im, z''.re, z''.im])129        (.add (.mul (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4)))) (.var 6)) (.mul (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3))) (.var 5)))130        (.add (.mul (.var 1) (.add (.mul (.var 3) (.var 6)) (.mul (.var 4) (.var 5)))) (.mul (.var 2) (.add (.mul (.var 3) (.var 5)) (.mul (.var 0) (.mul (.var 4) (.var 6))))))131        (by decide +kernel))132133/-- The norm is multiplicative: `N(z z') = N(z) N(z')`. -/134theorem norm_mul (z z' : Ext p ν) : norm (z * z') = norm z * norm z' :=135  Shell.Frame.RE.sound (Shell.Frame.look [ν, z.re, z.im, z'.re, z'.im])136    (.add (.mul (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4)))) (.add (.mul (.var 1) (.var 3)) (.mul (.var 0) (.mul (.var 2) (.var 4))))) (.neg (.mul (.var 0) (.mul (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3))) (.add (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 3)))))))137    (.mul (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2))))) (.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 0) (.mul (.var 4) (.var 4))))))138    (by decide +kernel)139140theorem norm_ofShell (c : Shell p) : norm (ofShell c : Ext p ν) = c * c := by141  show c * c + -(ν * (0 * 0)) = c * c142  rw [Shell.zero_mul, Shell.mul_zero, Shell.neg_zero, Shell.add_zero]143144theorem mul_one (z : Ext p ν) : z * 1 = z := by rw [mul_comm]; exact one_mul z145146theorem pow_add (z : Ext p ν) (m : Nat) : ∀ n : Nat, z ^ (m + n) = z ^ m * z ^ n147  | 0 => (mul_one _).symm148  | n + 1 => by show z ^ (m + n) * z = z ^ m * (z ^ n * z); rw [pow_add z m n, mul_assoc]149150/-- The norm of a power: `N(zⁿ) = N(z)ⁿ`. -/151theorem norm_pow (z : Ext p ν) : ∀ n : Nat, norm (z ^ n) = norm z ^ n152  | 0 => by show norm (ofShell 1 : Ext p ν) = 1; rw [norm_ofShell, Shell.one_mul]153  | n + 1 => by show norm (z ^ n * z) = norm z ^ n * norm z; rw [norm_mul, norm_pow z n]154155end Ext156157end FRC.Extension158