Theme/Lorentz.lean — FrcCore

1import FrcCore.Theme.Spin23/-!4# FrcCore.Theme.Lorentz — the register square and the finite Lorentz group (7-spacetime)56The projective theme's third core file (31 October 2026; the verification package of 7-spacetime). On a shell7`p = 4κ + 1` with its quadratic extension `K = 𝔽_p(η)`, `η² = ν` the drive's generator, a nonsquare, with8`conj η = −η`:910* **The register square** (7:C1). `X(x) = [[x₀ + x₃, x₁ + ηx₂], [x₁ − ηx₂, x₀ − x₃]]` has `det X(x) = x₀² − x₁² − x₃² + ν x₂²`11  (`register_det`) and `X(x)† = X(x)` (`register_hermitian`); the time vector is `X(0, 0, 1, 0) = ηJ` (`time_vector`).12* **The congruence** (7:C2). `X ↦ A X A†` preserves the Hermitian matrices (`congruence_hermitian`) and multiplies the13  determinant by `N(det A)` (`congruence_det`); a unimodular matrix fixing the four basis vectors is `±I` (`kernel_pm`).14* **The cone** (7:C3, C4). `v v†` has `det = 0` (`cone_point`); a direction `[z : 1]`, `z ∉ 𝔽_p`, has a time component (`cone_time`).15* **The two classes** (7:C5). `det(u u† + v v†) = N(u₁v₂ − u₂v₁)` (`rank_two_det`), so two null points span no isotropic plane16  unless proportional over `K` (`register_elliptic`); the frame quadric has the isotropic plane of the first row (`frame_hyperbolic`).17* **No inertia** (7:C6). With `a² + b² = ν` the explicit map multiplies the form by `ν` (`similitude`); such `a, b` exist (`two_squares`).18* **The fibration** (7:C7, C8). The stabiliser of the ray `η` in `SL₂(𝔽_p)` is the torus `[[a, νc], [c, a]]` (`ray_stabiliser`);19  `−I` lies in both lifts (`minus_one_in_both`); the axis of a ray `z` has discriminant `ν (2 Im z)²` (`axis_discriminant`).20* **Time** (7:D3, D4). `diag(g, 1)` scales the time vector by `g` (`drive_time`); its lift `diag(η, η⁻¹)` is unimodular and21  negates it (`lift_det`, `lift_time`); the even transport fixes it and dilates origin and antipode (`even_transport`); `−I` acts22  trivially (`neg_one_trivial`) and `P` conjugates `N¹` to the torus lift (`torus_conjugate`).23* **The antipode** (7:D6). `η` has order two modulo `𝔽_p^×` (`antipode_order_two`), the half step `2κ + 1` is odd24  (`half_step_odd`), and no square of `K` lies on `𝔽_p^× η` (`even_never_antipode`).25* **The arrow** (7:F3, F4). No unimodular matrix realises the time reversal, the reflection `x₁ ↦ −x₁` or `X ↦ −X`26  (`no_time_reversal`, `no_reflection`, `no_inversion`); on a hosted pair the joint period is `lcm(4κ, 4S)` (`joint_period`) and27  the chart count is injective for `n < S / gcd(κ, S)` (`drift_injective`, `drift_injective_gcd`); on the physical pair28  `p² < Ω − 1`, so the drift is one-directional (`drift_one_directional`, `nesting_depth`).2930The identities are decided by the ring normaliser of `Ring.lean` lifted to the extension and to its two-by-two matrices31(`Theme/Spin.lean`'s `XR`, `MX`). No axioms.32-/3334namespace FRC.Lorentz3536open FRC.Shell FRC.Shell.Frame FRC.Extension FRC.Spin3738variable {p : Nat} [Pos p] {ν : Shell p}3940/-! ## The register square -/4142/-- The register matrix `X(x) = [[x₀ + x₃, x₁ + ηx₂], [x₁ − ηx₂, x₀ − x₃]]`. -/43def X (x0 x1 x2 x3 : Shell p) : M2x p ν := ⟨⟨x0 + x3, 0⟩, ⟨x1, x2⟩, ⟨x1, -x2⟩, ⟨x0 + -x3, 0⟩⟩4445/-- The determinant form `Q(x) = x₀² − x₁² − x₃² + ν x₂²`. -/46def Q (ν : Shell p) (x0 x1 x2 x3 : Shell p) : Shell p := x0 * x0 + -(x1 * x1) + -(x3 * x3) + ν * (x2 * x2)4748/-- The congruence `A X A†`. -/49def cong (A M : M2x p ν) : M2x p ν := (A.mul M).mul A.dagger5051/-- A diagonal matrix over the extension. -/52def diagx (a d : Ext p ν) : M2x p ν := ⟨a, 0, 0, d⟩5354/-- The identity over the extension. -/55def Ix : M2x p ν := ⟨1, 0, 0, 1⟩5657/-- A shell scalar as a symbolic element of the extension. -/58def sv (i : Nat) : XR := ⟨.var i, .zero⟩5960/-- The symbolic register matrix of four ring expressions. -/61def MXX' (a b c d : RE) : MX := ⟨⟨.add a d, .zero⟩, ⟨b, c⟩, ⟨b, .neg c⟩, ⟨.add a (.neg d), .zero⟩⟩6263/-- The symbolic register matrix on the variables `i, i + 1, i + 2, i + 3`. -/64def MXX (i : Nat) : MX := MXX' (.var i) (.var (i + 1)) (.var (i + 2)) (.var (i + 3))6566/-- The symbolic time vector `X(0, 0, 1, 0)`. -/67def MXT : MX := MXX' .zero .zero .one .zero6869/-- The symbolic form `Q` on the variables `i, …, i + 3`, `ν` the variable `0`. -/70def QX (i : Nat) : RE :=71  .add (.add (.add (.mul (.var i) (.var i)) (.neg (.mul (.var (i + 1)) (.var (i + 1))))) (.neg (.mul (.var (i + 3)) (.var (i + 3)))))72    (.mul (.var 0) (.mul (.var (i + 2)) (.var (i + 2))))7374/-- The symbolic congruence. -/75def MXcong (A M : MX) : MX := MX.mul (MX.mul A M) (MX.tr (MX.conj A))7677/-- The environment of a register vector after `ν`. -/78def envX (ν x0 x1 x2 x3 : Shell p) : Nat → Shell p := look [ν, x0, x1, x2, x3]7980/-- The environment of a matrix `A` (variables `1 … 8`) and a register vector (`9 … 12`). -/81def envAX (A : M2x p ν) (x0 x1 x2 x3 : Shell p) : Nat → Shell p :=82  look [ν, A.a.re, A.a.im, A.b.re, A.b.im, A.c.re, A.c.im, A.d.re, A.d.im, x0, x1, x2, x3]8384/-- The environment of two matrices (`1 … 8`, `9 … 16`). -/85def envAB (A B : M2x p ν) : Nat → Shell p :=86  look [ν, A.a.re, A.a.im, A.b.re, A.b.im, A.c.re, A.c.im, A.d.re, A.d.im,87        B.a.re, B.a.im, B.b.re, B.b.im, B.c.re, B.c.im, B.d.re, B.d.im]8889/-- 7:C1 — `det X(x) = x₀² − x₁² − x₃² + ν x₂²`. -/90theorem register_det (x0 x1 x2 x3 : Shell p) : (X (ν := ν) x0 x1 x2 x3).det = Ext.ofShell (Q ν x0 x1 x2 x3) :=91  XR.sound (envX ν x0 x1 x2 x3) (MX.det (MXX 1)) ⟨QX 1, .zero⟩ (by decide +kernel)9293/-- 7:C1 — `X(x)` is Hermitian: `X(x)† = X(x)`. -/94theorem register_hermitian (x0 x1 x2 x3 : Shell p) : (X (ν := ν) x0 x1 x2 x3).dagger = X x0 x1 x2 x3 :=95  MX.sound (envX ν x0 x1 x2 x3) (MX.tr (MX.conj (MXX 1))) (MXX 1) (by decide +kernel)9697/-- 7:C1, 7:D1 — the time vector `X(0, 0, 1, 0)` is the Hermitian form `ηJ` of 00:C27 (`Theme/Spin.lean`). -/98theorem time_vector : (X (ν := ν) 0 0 1 0) = M2x.wJ Ext.w :=99  MX.sound (look [ν]) MXT ⟨XR.zero, ⟨.zero, .one⟩, XR.neg ⟨.zero, .one⟩, XR.zero⟩ (by decide +kernel)100101/-! ## The congruence -/102103theorem det_mul (A B : M2x p ν) : (A.mul B).det = A.det * B.det :=104  XR.sound (envAB A B) (MX.det (MX.mul (MX.v 1) (MX.v 9))) (XR.mul (MX.det (MX.v 1)) (MX.det (MX.v 9))) (by decide +kernel)105106theorem det_dagger (A : M2x p ν) : A.dagger.det = Ext.conj A.det :=107  XR.sound (envAB A A) (MX.det (MX.tr (MX.conj (MX.v 1)))) (XR.conj (MX.det (MX.v 1))) (by decide +kernel)108109theorem dagger_mul (A B : M2x p ν) : (A.mul B).dagger = B.dagger.mul A.dagger :=110  MX.sound (envAB A B) (MX.tr (MX.conj (MX.mul (MX.v 1) (MX.v 9)))) (MX.mul (MX.tr (MX.conj (MX.v 9))) (MX.tr (MX.conj (MX.v 1)))) (by decide +kernel)111112theorem dagger_dagger (A : M2x p ν) : A.dagger.dagger = A :=113  MX.sound (envAB A A) (MX.tr (MX.conj (MX.tr (MX.conj (MX.v 1))))) (MX.v 1) (by decide +kernel)114115theorem mul_assocx (A B C : M2x p ν) : (A.mul B).mul C = A.mul (B.mul C) :=116  MX.sound (look [ν, A.a.re, A.a.im, A.b.re, A.b.im, A.c.re, A.c.im, A.d.re, A.d.im,117                  B.a.re, B.a.im, B.b.re, B.b.im, B.c.re, B.c.im, B.d.re, B.d.im,118                  C.a.re, C.a.im, C.b.re, C.b.im, C.c.re, C.c.im, C.d.re, C.d.im])119    (MX.mul (MX.mul (MX.v 1) (MX.v 9)) (MX.v 17)) (MX.mul (MX.v 1) (MX.mul (MX.v 9) (MX.v 17))) (by decide +kernel)120121/-- 7:C2 — the congruence multiplies the determinant by the norm of `det A`: `det(A X A†) = det A · conj(det A) · det X`. -/122theorem congruence_det (A : M2x p ν) (x0 x1 x2 x3 : Shell p) :123    (cong A (X x0 x1 x2 x3)).det = A.det * Ext.conj A.det * Ext.ofShell (Q ν x0 x1 x2 x3) := by124  unfold cong125  rw [det_mul, det_mul, det_dagger, register_det, Ext.mul_assoc, Ext.mul_comm (Ext.ofShell _), ← Ext.mul_assoc]126127/-- 7:C2 — the congruence of a Hermitian matrix is Hermitian. -/128theorem congruence_hermitian (A : M2x p ν) (x0 x1 x2 x3 : Shell p) :129    (cong A (X x0 x1 x2 x3)).dagger = cong A (X x0 x1 x2 x3) := by130  unfold cong131  rw [dagger_mul, dagger_mul, dagger_dagger, register_hermitian, mul_assocx]132133/-- 7:F3, 7:C2 — a congruence of determinant one preserves the form: `det(A X A†) = det X` when `det A = 1`. -/134theorem congruence_preserves (A : M2x p ν) (hA : A.det = 1) (x0 x1 x2 x3 : Shell p) :135    (cong A (X x0 x1 x2 x3)).det = Ext.ofShell (Q ν x0 x1 x2 x3) := by136  rw [congruence_det, hA]137  have c1 : Ext.conj (1 : Ext p ν) = 1 := Ext.ext rfl Shell.neg_zero138  rw [c1, Ext.one_mul, Ext.one_mul]139140/-! ## The cone -/141142/-- 7:C3 — the Hermitian matrix of `v = (v₁, v₂)`: `v v† = X(x)` with `x₀ = h(N v₁ + N v₂)`, `x₃ = h(N v₁ − N v₂)` (`2h = 1`),143`(x₁, x₂) = v₁ conj v₂`, and `Q(x) = 0`: a null point of the register square. -/144theorem cone_point (h : Shell p) (h2 : (1 + 1) * h = 1) (v1 v2 : Ext p ν) :145    (⟨v1 * Ext.conj v1, v1 * Ext.conj v2, v2 * Ext.conj v1, v2 * Ext.conj v2⟩ : M2x p ν) =146      X (h * (Ext.norm v1 + Ext.norm v2)) (v1 * Ext.conj v2).re (v1 * Ext.conj v2).im (h * (Ext.norm v1 + -Ext.norm v2)) ∧147    Q ν (h * (Ext.norm v1 + Ext.norm v2)) (v1 * Ext.conj v2).re (v1 * Ext.conj v2).im (h * (Ext.norm v1 + -Ext.norm v2)) = 0 := by148  have e := look (p := p) [ν, v1.re, v1.im, v2.re, v2.im, h]149  -- the entries: `x₀ + x₃ = (2h) N v₁`, `x₀ − x₃ = (2h) N v₂`150  have ea : h * (Ext.norm v1 + Ext.norm v2) + h * (Ext.norm v1 + -Ext.norm v2) = (1 + 1) * h * Ext.norm v1 :=151    RE.sound (look [h, Ext.norm v1, Ext.norm v2]) (.add (.mul (.var 0) (.add (.var 1) (.var 2))) (.mul (.var 0) (.add (.var 1) (.neg (.var 2)))))152      (.mul (.mul (.add .one .one) (.var 0)) (.var 1)) (by decide +kernel)153  have ed : h * (Ext.norm v1 + Ext.norm v2) + -(h * (Ext.norm v1 + -Ext.norm v2)) = (1 + 1) * h * Ext.norm v2 :=154    RE.sound (look [h, Ext.norm v1, Ext.norm v2]) (.add (.mul (.var 0) (.add (.var 1) (.var 2))) (.neg (.mul (.var 0) (.add (.var 1) (.neg (.var 2))))))155      (.mul (.mul (.add .one .one) (.var 0)) (.var 2)) (by decide +kernel)156  rw [h2, Shell.one_mul] at ea ed157  have ec : v2 * Ext.conj v1 = ⟨(v1 * Ext.conj v2).re, -(v1 * Ext.conj v2).im⟩ :=158    XR.sound (look [ν, v1.re, v1.im, v2.re, v2.im]) (XR.mul (XR.v 3) (XR.conj (XR.v 1))) (XR.conj (XR.mul (XR.v 1) (XR.conj (XR.v 3)))) (by decide +kernel)159  -- `Q(x) = (x₀ + x₃)(x₀ − x₃) − N(v₁ conj v₂) = N v₁ N v₂ − N v₁ N v₂`160  have eq : Q ν (h * (Ext.norm v1 + Ext.norm v2)) (v1 * Ext.conj v2).re (v1 * Ext.conj v2).im (h * (Ext.norm v1 + -Ext.norm v2)) =161      (h * (Ext.norm v1 + Ext.norm v2) + h * (Ext.norm v1 + -Ext.norm v2)) * (h * (Ext.norm v1 + Ext.norm v2) + -(h * (Ext.norm v1 + -Ext.norm v2))) +162        -(Ext.norm (v1 * Ext.conj v2)) :=163    RE.sound (look [ν, h, Ext.norm v1, Ext.norm v2, (v1 * Ext.conj v2).re, (v1 * Ext.conj v2).im])164      (.add (.add (.add (.mul (.mul (.var 1) (.add (.var 2) (.var 3))) (.mul (.var 1) (.add (.var 2) (.var 3)))) (.neg (.mul (.var 4) (.var 4))))165        (.neg (.mul (.mul (.var 1) (.add (.var 2) (.neg (.var 3)))) (.mul (.var 1) (.add (.var 2) (.neg (.var 3)))))))166        (.mul (.var 0) (.mul (.var 5) (.var 5))))167      (.add (.mul (.add (.mul (.var 1) (.add (.var 2) (.var 3))) (.mul (.var 1) (.add (.var 2) (.neg (.var 3)))))168        (.add (.mul (.var 1) (.add (.var 2) (.var 3))) (.neg (.mul (.var 1) (.add (.var 2) (.neg (.var 3)))))))169        (.neg (.add (.mul (.var 4) (.var 4)) (.neg (.mul (.var 0) (.mul (.var 5) (.var 5))))))) (by decide +kernel)170  have nc : Ext.norm (Ext.conj v2) = Ext.norm v2 :=171    RE.sound (look [ν, v2.re, v2.im]) (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.neg (.var 2)) (.neg (.var 2))))))172      (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2))))) (by decide +kernel)173  refine ⟨?_, ?_⟩174  · refine M2x.ext' ?_ rfl ec ?_175    · show v1 * Ext.conj v1 = ⟨h * (Ext.norm v1 + Ext.norm v2) + h * (Ext.norm v1 + -Ext.norm v2), 0⟩176      rw [ea]; exact Ext.mul_conj v1177    · show v2 * Ext.conj v2 = ⟨h * (Ext.norm v1 + Ext.norm v2) + -(h * (Ext.norm v1 + -Ext.norm v2)), 0⟩178      rw [ed]; exact Ext.mul_conj v2179  · rw [eq, ea, ed, Ext.norm_mul, nc]; exact Shell.add_neg _180181/-- 7:C4 — a direction `[z : 1]` with `z ∉ 𝔽_p` carries a time component: the `x₂` coordinate of `v v†`, `v = (z, 1)`, is `Im z`. -/182theorem cone_time (z : Ext p ν) : (z * Ext.conj (1 : Ext p ν)).im = z.im := by183  show z.re * -(0 : Shell p) + z.im * 1 = z.im184  rw [Shell.neg_zero, Shell.mul_zero, Shell.zero_add, Shell.mul_one]185186/-! ## The two classes (7:C5) -/187188/-- 7:C5 — the determinant of a sum of two rank-one Hermitian matrices is the norm of the two-by-two determinant of the189vectors: `det(u u† + v v†) = N(u₁ v₂ − u₂ v₁)`. -/190theorem rank_two_det (u1 u2 v1 v2 : Ext p ν) :191    (⟨u1 * Ext.conj u1 + v1 * Ext.conj v1, u1 * Ext.conj u2 + v1 * Ext.conj v2,192      u2 * Ext.conj u1 + v2 * Ext.conj v1, u2 * Ext.conj u2 + v2 * Ext.conj v2⟩ : M2x p ν).det =193      Ext.ofShell (Ext.norm (u1 * v2 + -(u2 * v1))) :=194  XR.sound (look [ν, u1.re, u1.im, u2.re, u2.im, v1.re, v1.im, v2.re, v2.im])195    (MX.det ⟨XR.add (XR.mul (XR.v 1) (XR.conj (XR.v 1))) (XR.mul (XR.v 5) (XR.conj (XR.v 5))),196             XR.add (XR.mul (XR.v 1) (XR.conj (XR.v 3))) (XR.mul (XR.v 5) (XR.conj (XR.v 7))),197             XR.add (XR.mul (XR.v 3) (XR.conj (XR.v 1))) (XR.mul (XR.v 7) (XR.conj (XR.v 5))),198             XR.add (XR.mul (XR.v 3) (XR.conj (XR.v 3))) (XR.mul (XR.v 7) (XR.conj (XR.v 7)))⟩)199    (let d := XR.add (XR.mul (XR.v 1) (XR.v 7)) (XR.neg (XR.mul (XR.v 3) (XR.v 5)))200     ⟨.add (.mul d.re d.re) (.neg (.mul (.var 0) (.mul d.im d.im))), .zero⟩) (by decide +kernel)201202/-- 7:B4, 7:X1, 7:C5 — **the register square is elliptic**: on a field shell with `ν` a nonsquare, two null points `u u†`, `v v†` whose203sum is null have proportional vectors, `u₁ v₂ = u₂ v₁`: the null cone contains no totally isotropic plane. -/204theorem register_elliptic (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (u1 u2 v1 v2 : Ext p ν)205    (h : (⟨u1 * Ext.conj u1 + v1 * Ext.conj v1, u1 * Ext.conj u2 + v1 * Ext.conj v2,206           u2 * Ext.conj u1 + v2 * Ext.conj v1, u2 * Ext.conj u2 + v2 * Ext.conj v2⟩ : M2x p ν).det = 0) :207    u1 * v2 = u2 * v1 := by208  rw [rank_two_det] at h209  have hn : Ext.norm (u1 * v2 + -(u2 * v1)) = 0 := Ext.re_congr h210  have hz : u1 * v2 + -(u2 * v1) = 0 :=211    match Shell.instDecidableEq (u1 * v2 + -(u2 * v1)).re 0, Shell.instDecidableEq (u1 * v2 + -(u2 * v1)).im 0 with212    | isTrue h1, isTrue h2 => Ext.ext h1 h2213    | isTrue _, isFalse h2 => absurd hn (K.norm_ne_zero hν (Or.inr h2))214    | isFalse h1, _ => absurd hn (K.norm_ne_zero hν (Or.inl h1))215  exact ext_eq_of_add_neg_eq_zero hz216217/-- 7:B4, 7:X1, 7:C5 — **the frame quadric is hyperbolic**: the matrices `[[a, b], [0, 0]]` form a totally isotropic plane of `det` on `M₂(𝔽_p)`. -/218theorem frame_hyperbolic (a b : Shell p) : (M2.det (⟨a, b, 0, 0⟩ : M2 p)) = 0 := by219  show a * 0 + -(b * 0) = 0220  rw [Shell.mul_zero, Shell.mul_zero, Shell.neg_zero, Shell.add_zero]221222/-! ## No inertia (7:C6) -/223224/-- 7:A9, 7:X5, 7:C6 — with `a² + b² = ν`, the map `(x₀, x₁, x₂, x₃) ↦ (ν x₂, a x₁ − b x₃, x₀, b x₁ + a x₃)` multiplies the form by `ν`:225`⟨1, 1, 1, ν⟩ ≅ ⟨1, ν, ν, ν⟩`, a similitude of multiplier `ν` exchanging the two non-null classes. -/226theorem similitude (a b : Shell p) (hab : a * a + b * b = ν) (x0 x1 x2 x3 : Shell p) :227    Q ν (ν * x2) (a * x1 + -(b * x3)) x0 (b * x1 + a * x3) = ν * Q ν x0 x1 x2 x3 := by228  have e : Q ν (ν * x2) (a * x1 + -(b * x3)) x0 (b * x1 + a * x3) =229      ν * (ν * (x2 * x2)) + -((a * a + b * b) * (x1 * x1 + x3 * x3)) + ν * (x0 * x0) :=230    RE.sound (look [ν, x0, x1, x2, x3, a, b])231      (.add (.add (.add (.mul (.mul (.var 0) (.var 3)) (.mul (.var 0) (.var 3)))232          (.neg (.mul (.add (.mul (.var 5) (.var 2)) (.neg (.mul (.var 6) (.var 4)))) (.add (.mul (.var 5) (.var 2)) (.neg (.mul (.var 6) (.var 4)))))))233          (.neg (.mul (.add (.mul (.var 6) (.var 2)) (.mul (.var 5) (.var 4))) (.add (.mul (.var 6) (.var 2)) (.mul (.var 5) (.var 4))))))234        (.mul (.var 0) (.mul (.var 1) (.var 1))))235      (.add (.add (.mul (.var 0) (.mul (.var 0) (.mul (.var 3) (.var 3))))236          (.neg (.mul (.add (.mul (.var 5) (.var 5)) (.mul (.var 6) (.var 6))) (.add (.mul (.var 2) (.var 2)) (.mul (.var 4) (.var 4))))))237        (.mul (.var 0) (.mul (.var 1) (.var 1)))) (by decide +kernel)238  have e2 : ν * (ν * (x2 * x2)) + -(ν * (x1 * x1 + x3 * x3)) + ν * (x0 * x0) = ν * Q ν x0 x1 x2 x3 :=239    RE.sound (look [ν, x0, x1, x2, x3])240      (.add (.add (.mul (.var 0) (.mul (.var 0) (.mul (.var 3) (.var 3)))) (.neg (.mul (.var 0) (.add (.mul (.var 2) (.var 2)) (.mul (.var 4) (.var 4))))))241        (.mul (.var 0) (.mul (.var 1) (.var 1))))242      (.mul (.var 0) (QX 1)) (by decide +kernel)243  rw [e, hab, e2]244245/-- 7:C6 — on a shell with a quarter-turn `i² = −1` and `2h = 1`, every `ν` is a sum of two squares:246`ν = ((ν + 1)h)² + (i(ν − 1)h)²`. -/247theorem two_squares (i h : Shell p) (hi : i * i = -1) (h2 : (1 + 1) * h = 1) :248    (ν + 1) * h * ((ν + 1) * h) + i * ((ν + -1) * h) * (i * ((ν + -1) * h)) = ν := by249  have e : (ν + 1) * h * ((ν + 1) * h) + i * ((ν + -1) * h) * (i * ((ν + -1) * h)) =250      h * h * ((ν + 1) * (ν + 1) + i * i * ((ν + -1) * (ν + -1))) :=251    RE.sound (look [ν, i, h])252      (.add (.mul (.mul (.add (.var 0) .one) (.var 2)) (.mul (.add (.var 0) .one) (.var 2)))253            (.mul (.mul (.var 1) (.mul (.add (.var 0) (.neg .one)) (.var 2))) (.mul (.var 1) (.mul (.add (.var 0) (.neg .one)) (.var 2)))))254      (.mul (.mul (.var 2) (.var 2)) (.add (.mul (.add (.var 0) .one) (.add (.var 0) .one)) (.mul (.mul (.var 1) (.var 1)) (.mul (.add (.var 0) (.neg .one)) (.add (.var 0) (.neg .one))))))255      (by decide +kernel)256  have e2 : h * h * ((ν + 1) * (ν + 1) + -1 * ((ν + -1) * (ν + -1))) = (1 + 1) * h * ((1 + 1) * h) * ν :=257    RE.sound (look [ν, h])258      (.mul (.mul (.var 1) (.var 1)) (.add (.mul (.add (.var 0) .one) (.add (.var 0) .one)) (.mul (.neg .one) (.mul (.add (.var 0) (.neg .one)) (.add (.var 0) (.neg .one))))))259      (.mul (.mul (.mul (.add .one .one) (.var 1)) (.mul (.add .one .one) (.var 1))) (.var 0)) (by decide +kernel)260  rw [e, hi, e2, h2, Shell.one_mul, Shell.one_mul]261262/-! ## The fibration (7:C7, C8) -/263264/-- 7:C7 — the stabiliser of the ray `η` in the frame moves: `[[a, b], [c, d]]` fixes `η` under `z ↦ (az + b)/(cz + d)`,265i.e. `aη + b = (cη + d)η`, exactly when `a = d` and `b = νc`: the norm-one torus `[[a, νc], [c, a]]` of A10. -/266theorem ray_stabiliser (a b c d : Shell p) :267    (Ext.ofShell a * Ext.w + Ext.ofShell b : Ext p ν) = (Ext.ofShell c * Ext.w + Ext.ofShell d) * Ext.w ↔ a = d ∧ b = ν * c := by268  have l : (Ext.ofShell a * Ext.w + Ext.ofShell b : Ext p ν) = ⟨b, a⟩ :=269    XR.sound (look [ν, a, b]) (XR.add (XR.mul (sv 1) ⟨.zero, .one⟩) (sv 2)) ⟨.var 2, .var 1⟩ (by decide +kernel)270  have r : ((Ext.ofShell c * Ext.w + Ext.ofShell d) * Ext.w : Ext p ν) = ⟨ν * c, d⟩ :=271    XR.sound (look [ν, c, d]) (XR.mul (XR.add (XR.mul (sv 1) ⟨.zero, .one⟩) (sv 2)) ⟨.zero, .one⟩) ⟨.mul (.var 0) (.var 1), .var 2⟩ (by decide +kernel)272  rw [l, r]273  constructor274  · intro h; exact ⟨Ext.im_congr h, Ext.re_congr h⟩275  · intro h; exact Ext.ext h.2 h.1276277/-- 7:B1, 7:C7 — on the spin cover `−I` is both upper triangular of determinant one and a norm-one diagonal matrix278`diag(λ, λ̄)`: the Borel lift and the torus lift meet in `±I`, the obstruction to a subgroup section. -/279theorem minus_one_in_both :280    (-1 : Shell p) * -1 + -((0 : Shell p) * 0) = 1 ∧ Ext.norm (-1 : Ext p ν) = 1 ∧ Ext.conj (-1 : Ext p ν) = -1 := by281  refine ⟨?_, ?_, ?_⟩282  · rw [Shell.neg_mul_neg, Shell.one_mul, Shell.mul_zero, Shell.neg_zero, Shell.add_zero]283  · show (-1 : Shell p) * -1 + -(ν * (-0 * -0)) = 1284    rw [Shell.neg_mul_neg, Shell.one_mul, Shell.neg_zero, Shell.mul_zero, Shell.mul_zero, Shell.neg_zero, Shell.add_zero]285  · exact Ext.ext rfl (by show -(-(0 : Shell p)) = -0; rw [Shell.neg_neg, Shell.neg_zero])286287/-- 7:X2, 7:C8, 7:C10 — the axis of a ray `z`: the binary form `(t − z)(t − z̄) = t² − tr(z) t + N(z)` has discriminant288`tr(z)² − 4 N(z) = ν (2 Im z)²`, a nonsquare times a square. -/289theorem axis_discriminant (z : Ext p ν) :290    Ext.trace z * Ext.trace z + -((1 + 1) * (1 + 1) * Ext.norm z) = ν * (((1 + 1) * z.im) * ((1 + 1) * z.im)) :=291  RE.sound (look [ν, z.re, z.im])292    (.add (.mul (.add (.var 1) (.var 1)) (.add (.var 1) (.var 1)))293          (.neg (.mul (.mul (.add .one .one) (.add .one .one)) (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2))))))))294    (.mul (.var 0) (.mul (.mul (.add .one .one) (.var 2)) (.mul (.add .one .one) (.var 2)))) (by decide +kernel)295296/-! ## Time (7:D3, D4) -/297298/-- 7:D3, 7:A16 — the one-chronon move `diag(g, 1)` carries the time vector `ηJ = X(0, 0, 1, 0)` to `g·ηJ = X(0, 0, g, 0)`:299its square class flips with the chronon parity, and it carries the ray `(z, 1)` to `(gz, 1)`. -/300theorem drive_time (g : Shell p) :301    cong (diagx (Ext.ofShell g) 1) (X (ν := ν) 0 0 1 0) = X 0 0 g 0 ∧302    ∀ z : Ext p ν, (diagx (Ext.ofShell g) 1).mul ⟨z, 0, 1, 0⟩ = ⟨Ext.ofShell g * z, 0, 1, 0⟩ :=303  ⟨MX.sound (look [ν, g]) (MXcong ⟨sv 1, XR.zero, XR.zero, XR.one⟩ MXT) (MXX' .zero .zero (.var 1) .zero) (by decide +kernel),304   fun z => MX.sound (look [ν, g, z.re, z.im]) (MX.mul ⟨sv 1, XR.zero, XR.zero, XR.one⟩ ⟨XR.v 2, XR.zero, XR.one, XR.zero⟩)305     ⟨XR.mul (sv 1) (XR.v 2), XR.zero, XR.one, XR.zero⟩ (by decide +kernel)⟩306307/-- 7:D3 — the unimodular lift `D = diag(η, uη)`, `νu = 1` (so `uη = η⁻¹`), has determinant one. -/308theorem lift_det (u : Shell p) (hu : ν * u = 1) : (diagx Ext.w (Ext.ofShell u * Ext.w) : M2x p ν).det = 1 := by309  have e : (diagx Ext.w (Ext.ofShell u * Ext.w) : M2x p ν).det = Ext.ofShell (ν * u) :=310    XR.sound (look [ν, u]) (MX.det ⟨⟨.zero, .one⟩, XR.zero, XR.zero, XR.mul (sv 1) ⟨.zero, .one⟩⟩) ⟨.mul (.var 0) (.var 1), .zero⟩ (by decide +kernel)311  rw [e, hu]; rfl312313/-- 7:D3 — the lift negates the time vector: `D (ηJ) D† = −ηJ`, i.e. `X(0, 0, 1, 0) ↦ X(0, 0, −1, 0)`. -/314theorem lift_time (u : Shell p) (hu : ν * u = 1) :315    cong (diagx Ext.w (Ext.ofShell u * Ext.w)) (X (ν := ν) 0 0 1 0) = X 0 0 (-1) 0 := by316  have e : cong (diagx Ext.w (Ext.ofShell u * Ext.w)) (X (ν := ν) 0 0 1 0) = X 0 0 (-(ν * u)) 0 :=317    MX.sound (look [ν, u]) (MXcong ⟨⟨.zero, .one⟩, XR.zero, XR.zero, XR.mul (sv 1) ⟨.zero, .one⟩⟩ MXT)318      (MXX' .zero .zero (.neg (.mul (.var 0) (.var 1))) .zero) (by decide +kernel)319  rw [e, hu]320321/-- 7:D3 — the even transport `diag(g, u)`, `gu = 1`, fixes the time vector and `σ_x` and dilates `E₂₂` by `u²` and `E₁₁` by `g²`. -/322theorem even_transport (g u : Shell p) (hu : g * u = 1) :323    cong (diagx (Ext.ofShell g) (Ext.ofShell u)) (X (ν := ν) 0 0 1 0) = X 0 0 1 0 ∧324    cong (diagx (Ext.ofShell g) (Ext.ofShell u)) (X (ν := ν) 0 1 0 0) = X 0 1 0 0 ∧325    cong (diagx (Ext.ofShell g) (Ext.ofShell u)) (⟨0, 0, 0, 1⟩ : M2x p ν) = ⟨0, 0, 0, Ext.ofShell (u * u)⟩ ∧326    cong (diagx (Ext.ofShell g) (Ext.ofShell u)) (⟨1, 0, 0, 0⟩ : M2x p ν) = ⟨Ext.ofShell (g * g), 0, 0, 0⟩ := by327  have e1 : cong (diagx (Ext.ofShell g) (Ext.ofShell u)) (X (ν := ν) 0 0 1 0) = X 0 0 (g * u) 0 :=328    MX.sound (look [ν, g, u]) (MXcong ⟨sv 1, XR.zero, XR.zero, sv 2⟩ MXT) (MXX' .zero .zero (.mul (.var 1) (.var 2)) .zero) (by decide +kernel)329  have e2 : cong (diagx (Ext.ofShell g) (Ext.ofShell u)) (X (ν := ν) 0 1 0 0) = X 0 (g * u) 0 0 :=330    MX.sound (look [ν, g, u]) (MXcong ⟨sv 1, XR.zero, XR.zero, sv 2⟩ (MXX' .zero .one .zero .zero)) (MXX' .zero (.mul (.var 1) (.var 2)) .zero .zero) (by decide +kernel)331  refine ⟨by rw [e1, hu], by rw [e2, hu], ?_, ?_⟩332  · exact MX.sound (look [ν, g, u]) (MXcong ⟨sv 1, XR.zero, XR.zero, sv 2⟩ ⟨XR.zero, XR.zero, XR.zero, XR.one⟩)333      ⟨XR.zero, XR.zero, XR.zero, ⟨.mul (.var 2) (.var 2), .zero⟩⟩ (by decide +kernel)334  · exact MX.sound (look [ν, g, u]) (MXcong ⟨sv 1, XR.zero, XR.zero, sv 2⟩ ⟨XR.one, XR.zero, XR.zero, XR.zero⟩)335      ⟨⟨.mul (.var 1) (.var 1), .zero⟩, XR.zero, XR.zero, XR.zero⟩ (by decide +kernel)336337/-- 7:X4, 7:D4 — `−I` acts trivially on the register square: the spinor's two circuits are one on the square. -/338theorem neg_one_trivial (x0 x1 x2 x3 : Shell p) : cong (diagx (-1) (-1)) (X (ν := ν) x0 x1 x2 x3) = X x0 x1 x2 x3 :=339  MX.sound (envX ν x0 x1 x2 x3) (MXcong ⟨XR.neg XR.one, XR.zero, XR.zero, XR.neg XR.one⟩ (MXX 1)) (MXX 1) (by decide +kernel)340341/-- 7:D4 — `P diag(λ, λ̄) = (mult λ) P` for `P = [[η, −η], [1, 1]]` and `mult λ = [[x, νy], [y, x]]`, `λ = x + yη`: the342norm-one diagonal group `N¹` and the torus lift are conjugate in `SL₂(K)` through `P`. -/343theorem torus_conjugate (l : Ext p ν) :344    (⟨Ext.w, -Ext.w, 1, 1⟩ : M2x p ν).mul (diagx l (Ext.conj l)) =345      (⟨Ext.ofShell l.re, Ext.ofShell (ν * l.im), Ext.ofShell l.im, Ext.ofShell l.re⟩ : M2x p ν).mul ⟨Ext.w, -Ext.w, 1, 1⟩ :=346  MX.sound (look [ν, l.re, l.im])347    (MX.mul ⟨⟨.zero, .one⟩, ⟨.neg .zero, .neg .one⟩, XR.one, XR.one⟩ ⟨XR.v 1, XR.zero, XR.zero, XR.conj (XR.v 1)⟩)348    (MX.mul ⟨sv 1, ⟨.mul (.var 0) (.var 2), .zero⟩, sv 2, sv 1⟩ ⟨⟨.zero, .one⟩, ⟨.neg .zero, .neg .one⟩, XR.one, XR.one⟩) (by decide +kernel)349350/-! ## The kernel of the congruence (7:C2) and the three exclusions of the arrow (7:F3) -/351352/-- The negative of a matrix over the extension. -/353def negx (M : M2x p ν) : M2x p ν := ⟨-M.a, -M.b, -M.c, -M.d⟩354/-- `σ_x = [[0, 1], [1, 0]] = X(0, 1, 0, 0)` and `σ_z = diag(1, −1) = X(0, 0, 0, 1)`. -/355def Sx : M2x p ν := ⟨0, 1, 1, 0⟩356def Dx : M2x p ν := ⟨1, 0, 0, -1⟩357358theorem X_I : (X (ν := ν) 1 0 0 0) = Ix := MX.sound (look [ν]) (MXX' .one .zero .zero .zero) ⟨XR.one, XR.zero, XR.zero, XR.one⟩ (by decide +kernel)359theorem X_S : (X (ν := ν) 0 1 0 0) = Sx := MX.sound (look [ν]) (MXX' .zero .one .zero .zero) ⟨XR.zero, XR.one, XR.one, XR.zero⟩ (by decide +kernel)360theorem X_D : (X (ν := ν) 0 0 0 1) = Dx := MX.sound (look [ν]) (MXX' .zero .zero .zero .one) ⟨XR.one, XR.zero, XR.zero, XR.neg XR.one⟩ (by decide +kernel)361theorem X_negI : (X (ν := ν) (-1) 0 0 0) = negx Ix :=362  MX.sound (look [ν]) (MXX' (.neg .one) .zero .zero .zero) ⟨XR.neg XR.one, XR.neg XR.zero, XR.neg XR.zero, XR.neg XR.one⟩ (by decide +kernel)363theorem X_negS : (X (ν := ν) 0 (-1) 0 0) = negx Sx :=364  MX.sound (look [ν]) (MXX' .zero (.neg .one) .zero .zero) ⟨XR.neg XR.zero, XR.neg XR.one, XR.neg XR.one, XR.neg XR.zero⟩ (by decide +kernel)365theorem X_negD : (X (ν := ν) 0 0 0 (-1)) = negx Dx :=366  MX.sound (look [ν]) (MXX' .zero .zero .zero (.neg .one)) ⟨XR.neg XR.one, XR.neg XR.zero, XR.neg XR.zero, XR.neg (XR.neg XR.one)⟩ (by decide +kernel)367theorem X_negT : (X (ν := ν) 0 0 (-1) 0) = negx (X 0 0 1 0) :=368  MX.sound (look [ν]) (MXX' .zero .zero (.neg .one) .zero)369    ⟨XR.neg ⟨.add .zero .zero, .zero⟩, XR.neg ⟨.zero, .one⟩, XR.neg ⟨.zero, .neg .one⟩, XR.neg ⟨.add .zero (.neg .zero), .zero⟩⟩ (by decide +kernel)370371theorem mul_Ix (A : M2x p ν) : A.mul Ix = A := MX.sound (envAB A A) (MX.mul (MX.v 1) ⟨XR.one, XR.zero, XR.zero, XR.one⟩) (MX.v 1) (by decide +kernel)372theorem Ix_mul (A : M2x p ν) : Ix.mul A = A := MX.sound (envAB A A) (MX.mul ⟨XR.one, XR.zero, XR.zero, XR.one⟩ (MX.v 1)) (MX.v 1) (by decide +kernel)373theorem adj_mulx (A : M2x p ν) : A.adj.mul A = diagx A.det A.det :=374  MX.sound (envAB A A) (MX.mul ⟨(MX.v 1).d, XR.neg (MX.v 1).b, XR.neg (MX.v 1).c, (MX.v 1).a⟩ (MX.v 1))375    ⟨MX.det (MX.v 1), XR.zero, XR.zero, MX.det (MX.v 1)⟩ (by decide +kernel)376theorem mul_negx (A B : M2x p ν) : A.mul (negx B) = negx (A.mul B) :=377  MX.sound (envAB A B) (MX.mul (MX.v 1) ⟨XR.neg (MX.v 9).a, XR.neg (MX.v 9).b, XR.neg (MX.v 9).c, XR.neg (MX.v 9).d⟩)378    (let P := MX.mul (MX.v 1) (MX.v 9); ⟨XR.neg P.a, XR.neg P.b, XR.neg P.c, XR.neg P.d⟩) (by decide +kernel)379theorem negx_inj {A B : M2x p ν} (h : negx A = negx B) : A = B := by380  have n : ∀ x y : Ext p ν, -x = -y → x = y := fun x y e =>381    Ext.ext (by have h : -x.re = -y.re := Ext.re_congr e; rw [← Shell.neg_neg x.re, h]; exact Shell.neg_neg y.re)382            (by have h : -x.im = -y.im := Ext.im_congr e; rw [← Shell.neg_neg x.im, h]; exact Shell.neg_neg y.im)383  exact M2x.ext' (n _ _ (M2x.ext'_a h)) (n _ _ (M2x.ext'_b h)) (n _ _ (M2x.ext'_c h)) (n _ _ (M2x.ext'_d h))384385theorem diagx_one : (diagx (1 : Ext p ν) 1) = Ix := rfl386387/-- A right inverse of a matrix of determinant one is its adjugate. -/388theorem right_inverse (A N : M2x p ν) (hdet : A.det = 1) (h : A.mul N = Ix) : N = A.adj := by389  have e : A.adj.mul (A.mul N) = A.adj.mul Ix := congrArg _ h390  rw [← mul_assocx, adj_mulx, hdet, diagx_one, Ix_mul, mul_Ix] at e391  exact e392393/-- `cong A I = A A†`. -/394theorem cong_I (A : M2x p ν) : cong A Ix = A.mul A.dagger := by unfold cong; rw [mul_Ix]395396/-- A unitary matrix of determinant one (`A A† = I`) fixing `M` under the congruence commutes with `M`. -/397theorem commute_of_cong (A M : M2x p ν) (hdet : A.det = 1) (hu : A.mul A.dagger = Ix) (h : cong A M = M) : A.mul M = M.mul A := by398  have hadj := right_inverse A A.dagger hdet hu399  unfold cong at h; rw [hadj] at h400  have e : ((A.mul M).mul A.adj).mul A = M.mul A := congrArg (fun Y => Y.mul A) h401  rw [mul_assocx, adj_mulx, hdet, diagx_one, mul_Ix] at e402  exact e403404/-- The products with `σ_z` and `σ_x`, entrywise. -/405theorem mul_Dx (A : M2x p ν) : A.mul Dx = ⟨A.a, -A.b, A.c, -A.d⟩ ∧ Dx.mul A = ⟨A.a, A.b, -A.c, -A.d⟩ :=406  ⟨MX.sound (envAB A A) (MX.mul (MX.v 1) ⟨XR.one, XR.zero, XR.zero, XR.neg XR.one⟩) ⟨XR.v 1, XR.neg (XR.v 3), XR.v 5, XR.neg (XR.v 7)⟩ (by decide +kernel),407   MX.sound (envAB A A) (MX.mul ⟨XR.one, XR.zero, XR.zero, XR.neg XR.one⟩ (MX.v 1)) ⟨XR.v 1, XR.v 3, XR.neg (XR.v 5), XR.neg (XR.v 7)⟩ (by decide +kernel)⟩408theorem mul_Sx (A : M2x p ν) : A.mul Sx = ⟨A.b, A.a, A.d, A.c⟩ ∧ Sx.mul A = ⟨A.c, A.d, A.a, A.b⟩ :=409  ⟨MX.sound (envAB A A) (MX.mul (MX.v 1) ⟨XR.zero, XR.one, XR.one, XR.zero⟩) ⟨XR.v 3, XR.v 1, XR.v 7, XR.v 5⟩ (by decide +kernel),410   MX.sound (envAB A A) (MX.mul ⟨XR.zero, XR.one, XR.one, XR.zero⟩ (MX.v 1)) ⟨XR.v 5, XR.v 7, XR.v 1, XR.v 3⟩ (by decide +kernel)⟩411412theorem two_ne_zero_ext (h2 : (1 + 1 : Shell p) ≠ 0) : (1 + 1 : Ext p ν) ≠ 0 := fun h => h2 (Ext.re_congr h)413414/-- On a field shell of odd characteristic, `x + x = 0` forces `x = 0` in the extension. -/415theorem eq_zero_of_double (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (h2 : (1 + 1 : Shell p) ≠ 0) {x : Ext p ν} (h : x + x = 0) : x = 0 :=416  have e : (1 + 1 : Ext p ν) * x = x + x :=417    XR.sound (look [ν, x.re, x.im]) (XR.mul (XR.add XR.one XR.one) (XR.v 1)) (XR.add (XR.v 1) (XR.v 1)) (by decide +kernel)418  ext_eq_zero_of_mul K hν (two_ne_zero_ext h2) (by rw [e]; exact h)419420/-- A matrix commuting with `σ_z` is diagonal. -/421theorem diagonal_of_commute_D (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (h2 : (1 + 1 : Shell p) ≠ 0) (A : M2x p ν)422    (hD : A.mul Dx = Dx.mul A) : A.b = 0 ∧ A.c = 0 := by423  rw [(mul_Dx A).1, (mul_Dx A).2] at hD424  have hb : -A.b = A.b := M2x.ext'_b hD425  have hc : A.c = -A.c := M2x.ext'_c hD426  refine ⟨eq_zero_of_double K hν h2 ?_, eq_zero_of_double K hν h2 ?_⟩427  · have : A.b + A.b = -A.b + A.b := by rw [hb]428    rw [this]; exact Ext.ext (Shell.neg_add _) (Shell.neg_add _)429  · have : A.c + A.c = A.c + -A.c := by rw [← hc]430    rw [this]; exact Ext.ext (Shell.add_neg _) (Shell.add_neg _)431432/-- A matrix commuting with `σ_z` and `σ_x` is scalar. -/433theorem scalar_of_commute (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (h2 : (1 + 1 : Shell p) ≠ 0) (A : M2x p ν)434    (hD : A.mul Dx = Dx.mul A) (hS : A.mul Sx = Sx.mul A) : A = diagx A.a A.a := by435  obtain ⟨hb, hc⟩ := diagonal_of_commute_D K hν h2 A hD436  rw [(mul_Sx A).1, (mul_Sx A).2] at hS437  have had : A.a = A.d := M2x.ext'_b hS438  exact M2x.ext' rfl hb hc had.symm439440/-- `diag(a, d) (ηJ) diag(a, d)† = (a conj d) ηJ`, `diag(a, d) σ_x diag(a, d)† = [[0, a conj d], [d conj a, 0]]`, and441`diag(a, d) diag(a, d)† = diag(N a, N d)`. -/442theorem cong_diag (a d : Ext p ν) :443    cong (diagx a d) (X 0 0 1 0) = ⟨0, (a * Ext.conj d) * Ext.w, -((d * Ext.conj a) * Ext.w), 0⟩ ∧444    cong (diagx a d) Sx = ⟨0, a * Ext.conj d, d * Ext.conj a, 0⟩ ∧445    (diagx a d).mul (diagx a d).dagger = diagx (Ext.ofShell (Ext.norm a)) (Ext.ofShell (Ext.norm d)) :=446  let e := look (p := p) [ν, a.re, a.im, d.re, d.im]447  ⟨MX.sound e (MXcong ⟨XR.v 1, XR.zero, XR.zero, XR.v 3⟩ MXT)448     ⟨XR.zero, XR.mul (XR.mul (XR.v 1) (XR.conj (XR.v 3))) ⟨.zero, .one⟩, XR.neg (XR.mul (XR.mul (XR.v 3) (XR.conj (XR.v 1))) ⟨.zero, .one⟩), XR.zero⟩ (by decide +kernel),449   MX.sound e (MXcong ⟨XR.v 1, XR.zero, XR.zero, XR.v 3⟩ ⟨XR.zero, XR.one, XR.one, XR.zero⟩)450     ⟨XR.zero, XR.mul (XR.v 1) (XR.conj (XR.v 3)), XR.mul (XR.v 3) (XR.conj (XR.v 1)), XR.zero⟩ (by decide +kernel),451   MX.sound e (MX.mul ⟨XR.v 1, XR.zero, XR.zero, XR.v 3⟩ (MX.tr (MX.conj ⟨XR.v 1, XR.zero, XR.zero, XR.v 3⟩)))452     ⟨⟨.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2)))), .zero⟩, XR.zero, XR.zero,453      ⟨.add (.mul (.var 3) (.var 3)) (.neg (.mul (.var 0) (.mul (.var 4) (.var 4)))), .zero⟩⟩ (by decide +kernel)⟩454455theorem one_ne_neg_one (h2 : (1 + 1 : Shell p) ≠ 0) : (1 : Shell p) ≠ -1 := fun h => h2 (by456  have e : (1 : Shell p) + 1 = 1 + -1 := by rw [← h]457  rw [e]; exact Shell.add_neg (1 : Shell p))458459/-- On a field shell with `ν` a nonsquare, `a² = 1` in the extension forces `a = ±1`. -/460theorem sq_one (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (a : Ext p ν) (hsq : a * a = 1) : a = 1 ∨ a = -1 := by461  have fac : (a + -1) * (a + 1) = 0 := by462    have e : (a + -1) * (a + 1) = a * a + -1 :=463      XR.sound (look [ν, a.re, a.im]) (XR.mul (XR.add (XR.v 1) (XR.neg XR.one)) (XR.add (XR.v 1) XR.one)) (XR.add (XR.mul (XR.v 1) (XR.v 1)) (XR.neg XR.one)) (by decide +kernel)464    rw [e, hsq]; exact ext_add_neg_self 1465  match Ext.instDecidableEq (a + -1) 0 with466  | isTrue h => exact Or.inl (ext_eq_of_add_neg_eq_zero h)467  | isFalse h =>468    have h' : a + 1 = 0 := ext_eq_zero_of_mul K hν h fac469    have nn : -(-1 : Ext p ν) = 1 := Ext.ext (Shell.neg_neg 1) (by show -(-(0 : Shell p)) = 0; rw [Shell.neg_neg])470    exact Or.inr (ext_eq_of_add_neg_eq_zero (by rw [nn]; exact h'))471472theorem norm_one' : Ext.norm (1 : Ext p ν) = 1 :=473  RE.sound (look [ν]) (.add (.mul .one .one) (.neg (.mul (.var 0) (.mul .zero .zero)))) .one (by decide +kernel)474theorem norm_neg_one : Ext.norm (-1 : Ext p ν) = 1 :=475  RE.sound (look [ν]) (.add (.mul (.neg .one) (.neg .one)) (.neg (.mul (.var 0) (.mul (.neg .zero) (.neg .zero))))) .one (by decide +kernel)476theorem negx_negx (M : M2x p ν) : negx (negx M) = M :=477  MX.sound (envAB M M) ⟨XR.neg (XR.neg (XR.v 1)), XR.neg (XR.neg (XR.v 3)), XR.neg (XR.neg (XR.v 5)), XR.neg (XR.neg (XR.v 7))⟩ (MX.v 1) (by decide +kernel)478479/-- 7:X4, 7:C2 — **the kernel of the congruence is `±I`**: a matrix of determinant one fixing the four basis vectors of the480register square is `I` or `−I`. -/481theorem kernel_pm (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (h2 : (1 + 1 : Shell p) ≠ 0) (A : M2x p ν) (hdet : A.det = 1)482    (h0 : cong A (X 1 0 0 0) = X 1 0 0 0) (h1 : cong A (X 0 1 0 0) = X 0 1 0 0) (h3 : cong A (X 0 0 0 1) = X 0 0 0 1) :483    A = diagx 1 1 ∨ A = diagx (-1) (-1) := by484  rw [X_I] at h0; rw [X_S] at h1; rw [X_D] at h3485  have hu : A.mul A.dagger = Ix := by rw [← cong_I]; exact h0486  have hA := scalar_of_commute K hν h2 A (commute_of_cong A Dx hdet hu h3) (commute_of_cong A Sx hdet hu h1)487  have hsq : A.a * A.a = 1 := by488    have e : (diagx A.a A.a).det = A.a * A.a :=489      XR.sound (look [ν, A.a.re, A.a.im]) (MX.det ⟨XR.v 1, XR.zero, XR.zero, XR.v 1⟩) (XR.mul (XR.v 1) (XR.v 1)) (by decide +kernel)490    rw [← e, ← hA]; exact hdet491  rw [hA]492  match sq_one K hν A.a hsq with493  | Or.inl h => exact Or.inl (by rw [h])494  | Or.inr h => exact Or.inr (by rw [h])495496/-- 7:X6, 7:F3 — **the time reversal is not a Lorentz move.** No matrix of determinant one carries the four basis vectors of the497register square as the Frobenius does, `x₂ ↦ −x₂` (which negates the time vector and fixes `I`, `σ_x`, `σ_z`). -/498theorem no_time_reversal (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (h2 : (1 + 1 : Shell p) ≠ 0) (A : M2x p ν) (hdet : A.det = 1)499    (h0 : cong A (X 1 0 0 0) = X 1 0 0 0) (h1 : cong A (X 0 1 0 0) = X 0 1 0 0) (h3 : cong A (X 0 0 0 1) = X 0 0 0 1)500    (hT : cong A (X 0 0 1 0) = X 0 0 (-1) 0) : False := by501  rw [X_I] at h0; rw [X_S] at h1; rw [X_D] at h3502  have hu : A.mul A.dagger = Ix := by rw [← cong_I]; exact h0503  have hA := scalar_of_commute K hν h2 A (commute_of_cong A Dx hdet hu h3) (commute_of_cong A Sx hdet hu h1)504  obtain ⟨cT, _, cU⟩ := cong_diag A.a A.a505  rw [hA] at hu hT; rw [cU] at hu; rw [cT] at hT506  -- `N a = 1` from `A A† = I`, and `N a = −1` from the time vector507  have n1 : Ext.norm A.a = 1 := Ext.re_congr (M2x.ext'_a hu)508  have hb := M2x.ext'_b hT509  have e : (A.a * Ext.conj A.a) * Ext.w = ⟨0, Ext.norm A.a⟩ := by510    rw [Ext.mul_conj]511    exact XR.sound (look [ν, Ext.norm A.a]) (XR.mul (sv 1) ⟨.zero, .one⟩) ⟨.zero, .var 1⟩ (by decide +kernel)512  rw [e] at hb513  have n2 : Ext.norm A.a = -1 := Ext.im_congr hb514  exact one_ne_neg_one h2 (n1.symm.trans n2)515516/-- 7:X6, 7:F3 — **a spatial reflection is not a Lorentz move**: no matrix of determinant one carries the basis as `x₁ ↦ −x₁` (negating `σ_x`, fixing `I`, `σ_z`517and the time vector). -/518theorem no_reflection (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (h2 : (1 + 1 : Shell p) ≠ 0) (A : M2x p ν) (hdet : A.det = 1)519    (h0 : cong A (X 1 0 0 0) = X 1 0 0 0) (h1 : cong A (X 0 1 0 0) = X 0 (-1) 0 0) (h3 : cong A (X 0 0 0 1) = X 0 0 0 1)520    (hT : cong A (X 0 0 1 0) = X 0 0 1 0) : False := by521  rw [X_I] at h0; rw [X_S, X_negS] at h1; rw [X_D] at h3522  have hu : A.mul A.dagger = Ix := by rw [← cong_I]; exact h0523  obtain ⟨hb, hc⟩ := diagonal_of_commute_D K hν h2 A (commute_of_cong A Dx hdet hu h3)524  have hA : A = diagx A.a A.d := M2x.ext' rfl hb hc rfl525  obtain ⟨cT, cS, _⟩ := cong_diag A.a A.d526  rw [hA] at h1 hT; rw [cS] at h1; rw [cT] at hT527  -- `a conj d = −1` from `σ_x`, and `(a conj d) η = η` from the time vector528  have q1 : A.a * Ext.conj A.d = -1 := M2x.ext'_b h1529  have q2 : (A.a * Ext.conj A.d) * Ext.w = ⟨0, 1⟩ := M2x.ext'_b hT530  rw [q1] at q2531  have : (-1 : Ext p ν) * Ext.w = ⟨0, -1⟩ := XR.sound (look [ν]) (XR.mul (XR.neg XR.one) ⟨.zero, .one⟩) ⟨.zero, .neg .one⟩ (by decide +kernel)532  rw [this] at q2533  exact one_ne_neg_one h2 (Ext.im_congr q2).symm534535/-- 7:X6, 7:F3 — **the total inversion is not a Lorentz move**: no matrix of determinant one carries the basis as `X ↦ −X`. -/536theorem no_inversion (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (h2 : (1 + 1 : Shell p) ≠ 0) (A : M2x p ν) (hdet : A.det = 1)537    (h0 : cong A (X 1 0 0 0) = X (-1) 0 0 0) (h1 : cong A (X 0 1 0 0) = X 0 (-1) 0 0) (h3 : cong A (X 0 0 0 1) = X 0 0 0 (-1)) : False := by538  rw [X_I, X_negI] at h0; rw [X_S, X_negS] at h1; rw [X_D, X_negD] at h3539  have hu : A.mul (negx A.dagger) = Ix := by540    rw [mul_negx, ← cong_I, h0]541    exact MX.sound (look [ν]) ⟨XR.neg (XR.neg XR.one), XR.neg (XR.neg XR.zero), XR.neg (XR.neg XR.zero), XR.neg (XR.neg XR.one)⟩ ⟨XR.one, XR.zero, XR.zero, XR.one⟩ (by decide +kernel)542  have hadj := right_inverse A _ hdet hu543  -- the congruences with `A† = −adj A` read `A M adj A = M`544  have comm : ∀ M : M2x p ν, cong A M = negx M → A.mul M = M.mul A := fun M h => by545    unfold cong at h546    have hd : A.dagger = negx A.adj := by547      have : negx (negx A.dagger) = negx A.adj := congrArg negx hadj548      have nn : negx (negx A.dagger) = A.dagger :=549        MX.sound (envAB A.dagger A.dagger) ⟨XR.neg (XR.neg (XR.v 1)), XR.neg (XR.neg (XR.v 3)), XR.neg (XR.neg (XR.v 5)), XR.neg (XR.neg (XR.v 7))⟩ (MX.v 1) (by decide +kernel)550      rw [← nn]; exact this551    rw [hd, mul_negx] at h552    have h' := negx_inj h553    have e : ((A.mul M).mul A.adj).mul A = M.mul A := congrArg (fun Y => Y.mul A) h'554    rw [mul_assocx, adj_mulx, hdet, diagx_one, mul_Ix] at e555    exact e556  have hA := scalar_of_commute K hν h2 A (comm Dx h3) (comm Sx h1)557  obtain ⟨_, _, cU⟩ := cong_diag A.a A.a558  -- `A A† = −I` gives `N a = −1`; `det A = a² = 1` gives `a = ±1` and `N a = 1`559  have hu' : A.mul A.dagger = negx Ix := by560    have e : negx (A.mul A.dagger) = Ix := by rw [← mul_negx]; exact hu561    rw [← negx_negx (A.mul A.dagger), e]562  rw [hA, cU] at hu'563  have nm : Ext.norm A.a = -1 := Ext.re_congr (M2x.ext'_a hu')564  have hsq : A.a * A.a = 1 := by565    have e : (diagx A.a A.a).det = A.a * A.a :=566      XR.sound (look [ν, A.a.re, A.a.im]) (MX.det ⟨XR.v 1, XR.zero, XR.zero, XR.v 1⟩) (XR.mul (XR.v 1) (XR.v 1)) (by decide +kernel)567    rw [← e, ← hA]; exact hdet568  have n1 : Ext.norm A.a = 1 := match sq_one K hν A.a hsq with569    | Or.inl h => by rw [h]; exact norm_one'570    | Or.inr h => by rw [h]; exact norm_neg_one571  exact one_ne_neg_one h2 (n1.symm.trans nm)572573/-! ## The antipode (7:D6) -/574575/-- 7:D6, 7:A15 — `η` has order two modulo `𝔽_p^×`: `η² = ν ∈ 𝔽_p` while `η ∉ 𝔽_p` (its imaginary part is `1`). -/576theorem antipode_order_two : (Ext.w : Ext p ν) * Ext.w = Ext.ofShell ν ∧ (Ext.w : Ext p ν).im = 1 := ⟨Ext.w_sq, rfl⟩577578/-- 7:D6 — the half step of the cycle `C_{p+1}`, `p = 4κ + 1`: `p + 1 = 2(2κ + 1)`, and `2κ + 1` is odd. -/579theorem half_step_odd (κ : Nat) : 4 * κ + 1 + 1 = 2 * (2 * κ + 1) ∧ (2 * κ + 1) % 2 = 1 :=580  ⟨by rw [Nat.mul_add, ← FRC.Nat.mul_assoc], FRC.Nat.mod_unique (by decide) rfl⟩581582/-- 7:D6 — **the even steps never reach the antipode.** On a field shell with a quarter-turn `i² = −1` and `ν` a nonsquare,583no square `y²` of the extension lies on the line `𝔽_p^× η` of the antipode: `y² = cη`, `c ≠ 0`, would make584`ν = (i · N(y) · c⁻¹)²` a square. The unimodular torus, the even powers of a generator, misses the antipode. -/585theorem even_never_antipode (K : Fld p) (hν : ¬ ∃ y : Shell p, y * y = ν) (i : Shell p) (hi : i * i = -1)586    (c : Shell p) (hc : c ≠ 0) (y : Ext p ν) : y * y ≠ Ext.ofShell c * Ext.w := fun h => by587  have hn : Ext.norm y * Ext.norm y = c * c * -ν := by588    have e : Ext.norm (Ext.ofShell c * Ext.w : Ext p ν) = c * c * -ν :=589      RE.sound (look [ν, c]) (.add (.mul (.add (.mul (.var 1) .zero) (.mul (.var 0) (.mul .zero .one))) (.add (.mul (.var 1) .zero) (.mul (.var 0) (.mul .zero .one))))590        (.neg (.mul (.var 0) (.mul (.add (.mul (.var 1) .one) (.mul .zero .zero)) (.add (.mul (.var 1) .one) (.mul .zero .zero))))))591        (.mul (.mul (.var 1) (.var 1)) (.neg (.var 0))) (by decide +kernel)592    rw [← e, ← h]; exact (Ext.norm_mul y y).symm593  obtain ⟨s, hs⟩ := K.exists_inv hc594  apply hν595  refine ⟨i * (Ext.norm y * s), ?_⟩596  have e1 : i * (Ext.norm y * s) * (i * (Ext.norm y * s)) = i * i * (Ext.norm y * Ext.norm y * (s * s)) :=597    RE.sound (look [i, Ext.norm y, s]) (.mul (.mul (.var 0) (.mul (.var 1) (.var 2))) (.mul (.var 0) (.mul (.var 1) (.var 2))))598      (.mul (.mul (.var 0) (.var 0)) (.mul (.mul (.var 1) (.var 1)) (.mul (.var 2) (.var 2)))) (by decide +kernel)599  have e2 : (-1 : Shell p) * (c * c * -ν * (s * s)) = ν * ((c * s) * (c * s)) :=600    RE.sound (look [ν, c, s]) (.mul (.neg .one) (.mul (.mul (.mul (.var 1) (.var 1)) (.neg (.var 0))) (.mul (.var 2) (.var 2))))601      (.mul (.var 0) (.mul (.mul (.var 1) (.var 2)) (.mul (.var 1) (.var 2)))) (by decide +kernel)602  rw [e1, hi, hn, e2, hs, Shell.one_mul, Shell.mul_one]603604/-! ## The drift (7:F4, 7:A17) -/605606/-- 7:F4, 7:A25 — the joint period of a coprime pair, with its Bezout certificate `aκ = bS + 1` (at the laboratory pair607`(13, 233)`: `3 · 39 = 2 · 58 + 1`): `4κS` is a common multiple of `4κ` and `4S`, and every common multiple `L = 4κx = 4Sy` is a608multiple of `4κS` — the joint period is `lcm(4κ, 4S) = 4κS`. -/609theorem joint_period (κ S a b : Nat) (hS : 0 < S) (hbz : a * κ = b * S + 1) :610    (∃ x, 4 * κ * S = 4 * κ * x) ∧ (∃ y, 4 * κ * S = 4 * S * y) ∧611    ∀ L x y, L = 4 * κ * x → L = 4 * S * y → ∃ z, L = 4 * κ * S * z := by612  refine ⟨⟨S, rfl⟩, ⟨κ, by rw [FRC.Nat.mul_assoc, Nat.mul_comm κ S, ← FRC.Nat.mul_assoc]⟩, fun L x y hx hy => ?_⟩613  have e : κ * x = S * y := Nat.eq_of_mul_eq_mul_left (by decide : 0 < 4) (by rw [← FRC.Nat.mul_assoc, ← FRC.Nat.mul_assoc, ← hx, ← hy])614  have e2 : S * (b * x) + x = S * (a * y) :=615    calc S * (b * x) + x = (b * S + 1) * x := by rw [FRC.Nat.add_mul, Nat.one_mul, FRC.Nat.mul_assoc b S x, FRC.Nat.mul_left_comm b S x]616      _ = a * κ * x := by rw [hbz]617      _ = a * (S * y) := by rw [FRC.Nat.mul_assoc, e]618      _ = S * (a * y) := FRC.Nat.mul_left_comm a S y619  have e3 : (S * (b * x) + x) % S = (S * (a * y)) % S := by rw [e2]620  have hz : (S * (a * y)) % S = 0 := by621    have h0 := FRC.Nat.add_mul_mod_self_left 0 (a * y) S hS622    rw [Nat.add_zero, FRC.Nat.zero_mod] at h0; exact h0623  rw [FRC.Nat.add_mul_mod_self_left x (b * x) S hS, hz] at e3624  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec S hS x625  rw [e3, Nat.add_zero] at hq626  exact ⟨q, by rw [hx, hq, FRC.Nat.mul_assoc (4 * κ) S q]⟩627628/-- 7:X6, 7:F4 — **the drift distinguishes the revolutions on a hosted pair.** For a coprime pair, with its Bezout certificate `aκ = bS + 1`, the629chart count `4κn mod 4S` of the shell's origin after `n` revolutions is injective on `n < S`: two revolutions below `S` at the630same chart count are the same revolution. -/631theorem drift_injective (κ S n m a b : Nat) (hS : 0 < S) (hbz : a * κ = b * S + 1) (hn : n < S) (hm : m < S)632    (h : (4 * κ * n) % (4 * S) = (4 * κ * m) % (4 * S)) : n = m := by633  have h4 : 0 < 4 * S := Nat.mul_pos (by decide) hS634  obtain ⟨q1, e1⟩ := FRC.Nat.mod_spec (4 * S) h4 (4 * κ * n)635  obtain ⟨q2, e2⟩ := FRC.Nat.mod_spec (4 * S) h4 (4 * κ * m)636  rw [h] at e1637  generalize hr : 4 * κ * m % (4 * S) = r at e1 e2638  have e3 : 4 * (κ * n + S * q2) = 4 * (κ * m + S * q1) :=639    calc 4 * (κ * n + S * q2) = 4 * κ * n + 4 * S * q2 := by rw [Nat.mul_add, ← FRC.Nat.mul_assoc, ← FRC.Nat.mul_assoc]640      _ = 4 * S * q1 + r + 4 * S * q2 := by rw [e1]641      _ = 4 * S * q2 + r + 4 * S * q1 := by rw [Nat.add_right_comm, Nat.add_comm (4 * S * q1), ← Nat.add_right_comm]642      _ = 4 * κ * m + 4 * S * q1 := by rw [e2]643      _ = 4 * (κ * m + S * q1) := by rw [Nat.mul_add, ← FRC.Nat.mul_assoc, ← FRC.Nat.mul_assoc]644  have e4 : κ * n + S * q2 = κ * m + S * q1 := Nat.eq_of_mul_eq_mul_left (by decide : 0 < 4) e3645  have key : ∀ x q : Nat, a * (κ * x + S * q) = S * (b * x + a * q) + x := fun x q =>646    calc a * (κ * x + S * q) = a * κ * x + a * (S * q) := by rw [Nat.mul_add, ← FRC.Nat.mul_assoc]647      _ = (b * S + 1) * x + S * (a * q) := by rw [hbz, FRC.Nat.mul_left_comm a S q]648      _ = b * S * x + x + S * (a * q) := by rw [FRC.Nat.add_mul, Nat.one_mul]649      _ = S * (b * x) + x + S * (a * q) := by rw [FRC.Nat.mul_assoc b S x, FRC.Nat.mul_left_comm b S x]650      _ = S * (b * x) + S * (a * q) + x := by rw [Nat.add_right_comm]651      _ = S * (b * x + a * q) + x := by rw [Nat.mul_add]652  have e5 : S * (b * n + a * q2) + n = S * (b * m + a * q1) + m := by rw [← key n q2, ← key m q1, e4]653  have e6 : (S * (b * n + a * q2) + n) % S = (S * (b * m + a * q1) + m) % S := by rw [e5]654  rw [FRC.Nat.add_mul_mod_self_left n (b * n + a * q2) S hS, FRC.Nat.add_mul_mod_self_left m (b * m + a * q1) S hS,655      FRC.Nat.mod_eq_of_lt hn, FRC.Nat.mod_eq_of_lt hm] at e6656  exact e6657658/-- 7:F4 — the three laboratory pairs of the corpus, `(13, 233)`, `(173, 30089)` and `(1549, 2408561)`: their Bezout659certificates `aκ = bS + 1` — `39 · 3 = 2 · 58 + 1`, `5073 · 43 = 29 · 7522 + 1`, `395203 · 387 = 254 · 602140 + 1` — and the660joint periods `4κS`: `696`, `1293784`, `932112720`. -/661theorem drift_instance : (39 * 3 = 2 * 58 + 1 ∧ 4 * 3 * 58 = 696) ∧ (5073 * 43 = 29 * 7522 + 1 ∧ 4 * 43 * 7522 = 1293784) ∧662    (395203 * 387 = 254 * 602140 + 1 ∧ 4 * 387 * 602140 = 932112720) := by decide663664/-! ## The counts on the Subjects `𝔽₁₃`, `𝔽₁₇₃` and `𝔽₁₅₄₉`, decided by the kernel (7:C4, C9, B1) -/665666/-- 7:X2, 7:C9 — the class equation `1 + (p² − 1) + p(p + 1)(p − 2)/2 + p²(p − 1)/2 = (p − 1)p(p + 1)` at `p = 13`. -/667theorem class_equation_13 : 1 + (13 * 13 - 1) + 13 * 14 * 11 / 2 + 13 * 13 * 12 / 2 = 12 * 13 * 14 := by decide668/-- 7:C9, 7:X2 — the class equation at `p = 173`. -/669theorem class_equation_173 : 1 + (173 * 173 - 1) + 173 * 174 * 171 / 2 + 173 * 173 * 172 / 2 = 172 * 173 * 174 := by decide670/-- 7:C9, 7:X2 — the class equation at `p = 1549`. -/671theorem class_equation_1549 : 1 + (1549 * 1549 - 1) + 1549 * 1550 * 1547 / 2 + 1549 * 1549 * 1548 / 2 = 1548 * 1549 * 1550 := by decide672673/-- 7:C4 — the cone's `p² + 1` directions are the `p + 1` of space and the `p(p − 1)` causal rays, at `p = 13`. -/674theorem cone_count_13 : 13 + 1 + 13 * 12 = 13 * 13 + 1 := by decide675/-- 7:C4 — the cone's count at `p = 173`. -/676theorem cone_count_173 : 173 + 1 + 173 * 172 = 173 * 173 + 1 := by decide677/-- 7:C4 — the cone's count at `p = 1549`. -/678theorem cone_count_1549 : 1549 + 1 + 1549 * 1548 = 1549 * 1549 + 1 := by decide679680/-- 7:P1, 7:B1 — the three cycles have the consecutive orders `4κ`, `4κ + 1`, `4κ + 2` on the shell `p = 4κ + 1`. -/681theorem consecutive_orders (κ : Nat) : (4 * κ + 1) - 1 = 4 * κ ∧ (4 * κ + 1) + 1 = 4 * κ + 2 := ⟨FRC.Nat.add_sub_cancel (4 * κ) 1, rfl⟩682683/-! ## The general pair, and the counts on `𝔽₁₃` by elements (7:F4, C9, C4, D6; the repair of 1 November 2026) -/684685/-- `(d x) mod (d y) = d (x mod y)` for `0 < d` and `0 < y`, from the division identity. -/686theorem mul_mod_mul_left' (d x y : Nat) (hd : 0 < d) (hy : 0 < y) : (d * x) % (d * y) = d * (x % y) := by687  obtain ⟨q, hq⟩ := FRC.Nat.mod_spec y hy x688  have hr : x % y < y := FRC.Nat.mod_lt' x hy689  have hdr : d * (x % y) < d * y := by690    have h := FRC.Nat.mul_lt_mul_of_lt_of_pos hr hd691    rw [Nat.mul_comm (x % y) d, Nat.mul_comm y d] at h; exact h692  apply FRC.Nat.mod_unique hdr693  calc d * x = d * (y * q + x % y) := by rw [← hq]694    _ = d * (y * q) + d * (x % y) := Nat.mul_add d (y * q) (x % y)695    _ = d * y * q + d * (x % y) := by rw [FRC.Nat.mul_assoc]696697/-- 7:F4 — **the drift distinguishes the revolutions, general hosted pair.** With `d = gcd(κ, S)`, `κ = d κ'`, `S = d S'` and a Bezout698certificate `a κ' = b S' + 1` for the coprime parts, the chart count `4κn mod 4S` is injective on `n < S' = S/d`. -/699theorem drift_injective_gcd (κ' S' d n m a b : Nat) (hd : 0 < d) (hS : 0 < S') (hbz : a * κ' = b * S' + 1)700    (hn : n < S') (hm : m < S')701    (h : (4 * (d * κ') * n) % (4 * (d * S')) = (4 * (d * κ') * m) % (4 * (d * S'))) : n = m := by702  have h4S : 0 < 4 * S' := Nat.mul_pos (by decide) hS703  have e : ∀ x : Nat, (4 * (d * κ') * x) % (4 * (d * S')) = d * ((4 * κ' * x) % (4 * S')) := by704    intro x705    rw [FRC.Nat.mul_left_comm 4 d κ', FRC.Nat.mul_assoc d (4 * κ') x, FRC.Nat.mul_left_comm 4 d S']706    exact mul_mod_mul_left' d (4 * κ' * x) (4 * S') hd h4S707  rw [e n, e m] at h708  exact drift_injective κ' S' n m a b hS hbz hn hm (Nat.eq_of_mul_eq_mul_left hd h)709710/-- 7:F4 — an admissible pair with `gcd(κ, S) = 3`: `(13, 181)`, `κ = 3 · 1`, `S = 45 = 3 · 15`, the certificate `1 · 1 = 0 · 15 + 1`711for the coprime parts, and the joint period `lcm(12, 180) = 180 = 4κS/3`. -/712theorem drift_instance_gcd : 3 = 3 * 1 ∧ 45 = 3 * 15 ∧ 1 * 1 = 0 * 15 + 1 ∧ 4 * 3 * 45 / 3 = 180 ∧ 13 * 13 < 181 := by decide713714/-! ## The drift is one-directional (7:F4, 7:A17; the physical pair, 1 November 2026) -/715716/-- 7:F5, 7:X6, 7:F4, 7:A17 — **a count below the Carrier's cycle is its own residue**: the chart count of a duration `n < Ω − 1` is `n`. -/717theorem drift_one_directional (Om n : Nat) (h : n < Om - 1) : n % (Om - 1) = n := FRC.Nat.mod_eq_of_lt h718719/-- 7:F5, 7:B5, 7:F4, 7:A17 — **the nesting bound keeps every registrable depth below the cycle.** For an odd `p` with `p² < Ω = 4S + 1`,720`p²` is odd and `4S` even, so `p² ≤ 4S − 1`, and a registered duration `n ≤ p²` has `n < Ω − 1`: the cycle never acts. -/721theorem nesting_depth (p S n : Nat) (hp : p % 2 = 1) (hn : p * p < 4 * S + 1) (hd : n ≤ p * p) : n < 4 * S + 1 - 1 := by722  have h1 : p * p ≤ 4 * S := Nat.le_of_lt_succ hn723  have h2 : p * p % 2 = 1 := by rw [FRC.Nat.mul_mod p p 2 (by decide), hp]724  have h3 : 4 * S % 2 = 0 := by rw [FRC.Nat.mul_mod 4 S 2 (by decide)]; show 0 * (S % 2) % 2 = 0; rw [Nat.zero_mul]725  have h4 : p * p ≠ 4 * S := fun e => by rw [e] at h2; rw [h3] at h2; exact Nat.zero_ne_one h2726  have h5 : p * p < 4 * S := Nat.lt_of_le_of_ne h1 h4727  rw [Nat.add_sub_cancel]728  exact Nat.lt_of_le_of_lt hd h5729730/-- 7:F4, 7:A17 — the three laboratory pairs and `(13, 181)`: `p² < Ω − 1` on each, and the hosted joint periods all exceed `p²`. -/731theorem drift_instance_pairs : 13 * 13 < 232 ∧ 173 * 173 < 30088 ∧ 1549 * 1549 < 2408560 ∧ 13 * 13 < 180 ∧732    13 * 13 < 696 ∧ 173 * 173 < 1293784 ∧ 1549 * 1549 < 932112720 ∧ 13 * 13 < 180 := by decide733734/-- The discriminant class on `𝔽₁₃` of `[[a, b], [c, d]]`: `Δ = tr² − 4 det = (a − d)² + 4bc`, in `Nat` with `a − d` as `a + 13 − d`. -/735def disc13 (a b c d : Nat) : Nat := ((a + 13 - d) * (a + 13 - d) + 4 * b * c) % 13736/-- The nonzero squares of `𝔽₁₃`. -/737def isSquare13 (x : Nat) : Bool := [1, 3, 4, 9, 10, 12].contains x738/-- `ad − bc ≠ 0` on `𝔽₁₃`, in `Nat`. -/739def isInvertible13 (a b c d : Nat) : Bool := (a * d + 169 - b * c) % 13 != 0740/-- The elements of `GL₂(𝔽₁₃)` by discriminant class: `Δ` a nonzero square, `Δ = 0`, `Δ` a nonsquare. -/741def classCounts13 : Nat × Nat × Nat :=742  (List.range 13).foldl (fun acc a => (List.range 13).foldl (fun acc b => (List.range 13).foldl (fun acc c =>743    (List.range 13).foldl (fun acc d =>744      if isInvertible13 a b c d then745        let Δ := disc13 a b c d746        if Δ = 0 then (acc.1, acc.2.1 + 1, acc.2.2)747        else if isSquare13 Δ then (acc.1 + 1, acc.2.1, acc.2.2)748        else (acc.1, acc.2.1, acc.2.2 + 1)749      else acc) acc) acc) acc) (0, 0, 0)750/-- 7:C9, 7:X2 — **the class equation by elements at `p = 13`.** The `26208` invertible matrices fall into the three discriminant751classes with `12012`, `2028` and `12168` elements; divided by the `12` scalars these are the `1001` split classes, the identity752with the `168` unipotent classes, and the `1014` non-split classes of `PGL₂(𝔽₁₃)`: the three terms of `class_equation_13`. -/753theorem class_partition_13 : classCounts13 = (12012, 2028, 12168) ∧ 12012 = 12 * (13 * 14 * 11 / 2) ∧754    2028 = 12 * (1 + (13 * 13 - 1)) ∧ 12168 = 12 * (13 * 13 * 12 / 2) ∧ 12012 + 2028 + 12168 = 12 * (12 * 13 * 14) := by755  decide +kernel756757/-- The null vectors of the register square `Q_2 = x₀² − x₁² − x₃² + 2x₂²` on `𝔽₁₃⁴`, the zero vector included. -/758def nullCount13 : Nat :=759  (List.range 13).foldl (fun acc x0 => (List.range 13).foldl (fun acc x1 => (List.range 13).foldl (fun acc x2 =>760    (List.range 13).foldl (fun acc x3 =>761      if (x0 * x0 + 2 * x2 * x2 + 2 * 169 - x1 * x1 - x3 * x3) % 13 = 0 then acc + 1 else acc) acc) acc) acc) 0762/-- 7:C3, 7:C4 — **the cone by vectors at `p = 13`**: `2041 = p³ − p² + p` null vectors, hence `(2041 − 1)/12 = 170 = p² + 1` null763lines, the count of `cone_count_13`. -/764theorem null_count_13 : nullCount13 = 2041 ∧ 2041 = 13 * 13 * 13 - 13 * 13 + 13 ∧ (2041 - 1) / 12 = 13 * 13 + 1 := by765  decide +kernel766767/-- `K = 𝔽₁₃(η)`, `η² = 2`: the product of `a + bη` and `c + dη`. -/768def kmul13 (u v : Nat × Nat) : Nat × Nat := ((u.1 * v.1 + 2 * u.2 * v.2) % 13, (u.1 * v.2 + u.2 * v.1) % 13)769/-- The inverse of `b` in `𝔽₁₃^×` (`0` for `b = 0`). -/770def inv13 (b : Nat) : Nat := (List.range 13).foldl (fun acc c => if (b * c) % 13 = 1 then c else acc) 0771/-- The class of `a + bη` modulo `𝔽₁₃^×`: `(a/b, 1)` for `b ≠ 0`, the antipode `(1, 0)` for `b = 0`. -/772def nrm13 (u : Nat × Nat) : Nat × Nat := if u.2 = 0 then (1, 0) else ((u.1 * inv13 u.2) % 13, 1)773/-- The least `k ∈ [1, 14]` with `w^k ≡ t` modulo `𝔽₁₃^×`, or `0` when none. -/774def firstHit13 (w t : Nat × Nat) : Nat :=775  ((List.range 14).foldl (fun (acc : Nat × (Nat × Nat)) k =>776      let pw := kmul13 acc.2 w777      (if acc.1 = 0 ∧ nrm13 pw = nrm13 t then k + 1 else acc.1, pw)) (0, (1, 0))).1778/-- The `14 = p + 1` classes of `K^×/𝔽₁₃^×`, the directions `ℙ¹(𝔽₁₃)`. -/779def classes13 : List (Nat × Nat) := (1, 0) :: (List.range 13).map (fun a => (a, 1))780/-- The generators of the cycle `K^×/𝔽₁₃^×`: the classes whose first return to the identity is at `k = 14`. -/781def generators13 : List (Nat × Nat) := classes13.filter (fun w => firstHit13 w (1, 0) = 14)782/-- 7:D6 — **the antipode at the odd half step, by every generator, at `p = 13`.** `K^×/𝔽₁₃^×` is a cycle of order `14` with783`6 = φ(14)` generators, and every generator first carries the origin `η = [0 : 1]` to the antipode `1 = [1 : 0]` at the step784`7 = (p + 1)/2 = 2κ + 1`, which is odd; `η` itself has order two. -/785theorem antipode_half_step_13 : classes13.length = 14 ∧ generators13.length = 6 ∧786    generators13.all (fun w => firstHit13 w (0, 1) = 7) = true ∧ firstHit13 (0, 1) (1, 0) = 2 ∧ 7 % 2 = 1 := by787  decide +kernel788789end FRC.Lorentz790