Theme/Plane.lean — FrcCore

1import FrcCore.Theme.Dirac23/-!4# The Lorentzian plane of 8-dirac — the class datum, the boosts and the Cayley map, no axioms56The second file of the dirac theme (5 November 2026, the core-proof programme of7`8-dirac-20260709/reports/core-proofs-20261105/`): what the Lorentzian plane of the shell gives on every frame8`(τ; 0, 1, g)` with its drive `g` and every nonsquare `ν`, by the frame theme's parity and the ring normaliser9(`RE.sound`, a kernel decision of a polynomial identity on the shell). The class is the datum: the product of two10nonsquares is a square, since both are odd powers of the drive, and the Lorentzian form depends on its coefficient11through the class alone (B2). The boost `Λ(x, y)` of a pair with `δ = x² − νy² ≠ 0` has the entries12`A = (x² + νy²)/δ`, `B = −2xy/δ` with `A² − νB² = 1`, so the extension theme's `boost_preserves` applies (D14); the13boosts compose as the extension multiplies, `Λ(z)Λ(z') = Λ(zz')`, with `Λ(1) = 1` and `Λ(z̄) = Λ(z)⁻¹` (D15). The14scalar Cayley map `φ(λ) = (1 + λw)/(1 − λw)` and its gauge flip `φ⁻(λ) = (1 − λw)/(1 + λw)` are inverse to each15other, with the inverse of the common norm `1 − νλ²` supplied (C16). Every statement is general in the shell; the16inverses enter as hypotheses `d · u = 1`, which Fermat's theorem (`Field.fermat`, `u = d^{p−2}`) discharges on a prime17shell. No axioms.18-/1920namespace FRC.Dirac.Plane2122open FRC FRC.Shell FRC.Shell.Frame FRC.Extension2324variable {p : Nat} [Pos p]2526/-! ## 8:B2 — the class is the datum -/27section classdatum28variable {κ : Nat} {g : Shell p}2930/-- A nonzero residue is a power of the drive below `p − 1`: the frame generates. -/31theorem exists_pow_eq (F : Frame p κ g) {a : Shell p} (ha : a ≠ 0) : ∃ m, m < p - 1 ∧ g ^ m = a := by32  have hv : 0 < a.val := by33    rcases Nat.eq_zero_or_pos a.val with h0 | h034    · exact absurd (Shell.ext (by rw [h0]; rfl)) ha35    · exact h036  obtain ⟨m, hm, he⟩ := F.generates a.val a.lt hv37  exact ⟨m, hm, Shell.ext he⟩3839/-- A nonsquare residue is an odd power of the drive. -/40theorem odd_of_nonsquare (F : Frame p κ g) {a : Shell p} (ha : ¬IsSquare a) {m : Nat} (hm : g ^ m = a) :41    m % 2 = 1 := by42  rcases mod_two_cases m with h | h43  · obtain ⟨r, hr⟩ := (parity_iff F m).2 h44    exact absurd ⟨r, by rw [hr, hm]⟩ ha45  · exact h4647/-- 8:B2 — the nonsquares form one square class: the product of two nonsquares is a square, on every frame. Each48is an odd power of the drive, so the product is an even power. -/49theorem class_datum (F : Frame p κ g) {a b : Shell p} (ha0 : a ≠ 0) (hb0 : b ≠ 0) (ha : ¬IsSquare a)50    (hb : ¬IsSquare b) : IsSquare (a * b) := by51  obtain ⟨m, -, hm⟩ := exists_pow_eq F ha052  obtain ⟨n, -, hn⟩ := exists_pow_eq F hb053  have hmo := odd_of_nonsquare F ha hm54  have hno := odd_of_nonsquare F hb hn55  have he : (m + n) % 2 = 0 := by56    rw [FRC.Nat.add_mod m n 2 (by decide), hmo, hno]57  rw [← hm, ← hn, ← Shell.pow_add]58  exact (parity_iff F (m + n)).2 he5960/-- 8:B2 — the Lorentzian form depends on its coefficient through the class alone: for every `m`,61`−(m²ν) x₀² + x₁² + x₂² + x₃² = −ν (m x₀)² + x₁² + x₂² + x₃²`, so the forms of `ν` and `m²ν` are equivalent by62the rescaling `x₀ ↦ m x₀` (a polynomial identity, decided by the normaliser). -/63theorem form_class (ν m x₀ x₁ x₂ x₃ : Shell p) :64    -(m * m * ν) * (x₀ * x₀) + x₁ * x₁ + x₂ * x₂ + x₃ * x₃ =65      -ν * ((m * x₀) * (m * x₀)) + x₁ * x₁ + x₂ * x₂ + x₃ * x₃ :=66  RE.sound (look [ν, m, x₀, x₁, x₂, x₃])67    (.add (.add (.add (.mul (.neg (.mul (.mul (.var 1) (.var 1)) (.var 0))) (.mul (.var 2) (.var 2)))68      (.mul (.var 3) (.var 3))) (.mul (.var 4) (.var 4))) (.mul (.var 5) (.var 5)))69    (.add (.add (.add (.mul (.neg (.var 0)) (.mul (.mul (.var 1) (.var 2)) (.mul (.var 1) (.var 2))))70      (.mul (.var 3) (.var 3))) (.mul (.var 4) (.var 4))) (.mul (.var 5) (.var 5)))71    (by decide +kernel)7273end classdatum7475/-! ## 8:D14, 8:D15 — the boosts -/76section boosts7778/-- The boost of the pair `(x, y)`, with `u` the inverse of `δ = x² − νy²`: the extension element `A + Bw`,79`A = (x² + νy²)u`, `B = −2xy·u`. -/80def boostOf (ν x y u : Shell p) : Ext p ν := ⟨(x * x + ν * (y * y)) * u, -((x + x) * y) * u⟩8182/-- 8:D14 — the boost entries have `A² − νB² = 1`: `A² − νB² = (δu)²` as polynomials, and `δu = 1`. -/83theorem boost_entries_norm (ν x y u : Shell p) (hu : (x * x + -(ν * (y * y))) * u = 1) :84    (boostOf ν x y u).re * (boostOf ν x y u).re + -(ν * ((boostOf ν x y u).im * (boostOf ν x y u).im)) = 1 := by85  show (x * x + ν * (y * y)) * u * ((x * x + ν * (y * y)) * u) +86      -(ν * (-((x + x) * y) * u * (-((x + x) * y) * u))) = 187  have e : (x * x + ν * (y * y)) * u * ((x * x + ν * (y * y)) * u) +88      -(ν * (-((x + x) * y) * u * (-((x + x) * y) * u))) =89      ((x * x + -(ν * (y * y))) * u) * ((x * x + -(ν * (y * y))) * u) :=90    RE.sound (look [ν, x, y, u])91      (.add (.mul (.mul (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.var 3))92                  (.mul (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.var 3)))93            (.neg (.mul (.var 0) (.mul (.mul (.neg (.mul (.add (.var 1) (.var 1)) (.var 2))) (.var 3))94                                       (.mul (.neg (.mul (.add (.var 1) (.var 1)) (.var 2))) (.var 3))))))95      (.mul (.mul (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2))))) (.var 3))96            (.mul (.add (.mul (.var 1) (.var 1)) (.neg (.mul (.var 0) (.mul (.var 2) (.var 2))))) (.var 3)))97      (by decide +kernel)98  rw [e, hu]; exact Shell.one_mul 199100/-- 8:D14 — the boost is orthogonal: `Λ(x, y)` preserves the coordinate form `x² − νt²` (the extension theme's101`boost_preserves` with `γ = A`, `b = B`). -/102theorem boost_orthogonal (ν x y u : Shell p) (hu : (x * x + -(ν * (y * y))) * u = 1) (t s : Shell p) :103    Q2 ν (boostT ν (boostOf ν x y u).re (boostOf ν x y u).im t s)104         (boostX ν (boostOf ν x y u).re (boostOf ν x y u).im t s) = Q2 ν t s :=105  boost_preserves (boost_entries_norm ν x y u hu) t s106107/-- 8:D15 — the boost of the product is the product of the boosts: with `zz' = (xx' + νyy') + (xy' + yx')w` and108the inverse `uu'` of `δ(zz') = δ(z)δ(z')`, `Λ(zz') = Λ(z)Λ(z')` in the extension (two polynomial identities). -/109theorem boost_of_mul (ν x y u x' y' u' : Shell p) :110    boostOf ν (x * x' + ν * (y * y')) (x * y' + y * x') (u * u') = boostOf ν x y u * boostOf ν x' y' u' := by111  apply Ext.ext112  · show (((x * x' + ν * (y * y')) * (x * x' + ν * (y * y')) + ν * ((x * y' + y * x') * (x * y' + y * x'))) * (u * u')) =113      (x * x + ν * (y * y)) * u * ((x' * x' + ν * (y' * y')) * u') + ν * (-((x + x) * y) * u * (-((x' + x') * y') * u'))114    exact RE.sound (look [ν, x, y, u, x', y', u'])115      (.mul (.add (.mul (.add (.mul (.var 1) (.var 4)) (.mul (.var 0) (.mul (.var 2) (.var 5))))116                        (.add (.mul (.var 1) (.var 4)) (.mul (.var 0) (.mul (.var 2) (.var 5)))))117                  (.mul (.var 0) (.mul (.add (.mul (.var 1) (.var 5)) (.mul (.var 2) (.var 4)))118                                       (.add (.mul (.var 1) (.var 5)) (.mul (.var 2) (.var 4))))))119            (.mul (.var 3) (.var 6)))120      (.add (.mul (.mul (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.var 3))121                  (.mul (.add (.mul (.var 4) (.var 4)) (.mul (.var 0) (.mul (.var 5) (.var 5)))) (.var 6)))122            (.mul (.var 0) (.mul (.mul (.neg (.mul (.add (.var 1) (.var 1)) (.var 2))) (.var 3))123                                 (.mul (.neg (.mul (.add (.var 4) (.var 4)) (.var 5))) (.var 6)))))124      (by decide +kernel)125  · show -(((x * x' + ν * (y * y')) + (x * x' + ν * (y * y'))) * (x * y' + y * x')) * (u * u') =126      (x * x + ν * (y * y)) * u * (-((x' + x') * y') * u') + -((x + x) * y) * u * ((x' * x' + ν * (y' * y')) * u')127    exact RE.sound (look [ν, x, y, u, x', y', u'])128      (.mul (.neg (.mul (.add (.add (.mul (.var 1) (.var 4)) (.mul (.var 0) (.mul (.var 2) (.var 5))))129                              (.add (.mul (.var 1) (.var 4)) (.mul (.var 0) (.mul (.var 2) (.var 5)))))130                        (.add (.mul (.var 1) (.var 5)) (.mul (.var 2) (.var 4)))))131            (.mul (.var 3) (.var 6)))132      (.add (.mul (.mul (.add (.mul (.var 1) (.var 1)) (.mul (.var 0) (.mul (.var 2) (.var 2)))) (.var 3))133                  (.mul (.neg (.mul (.add (.var 4) (.var 4)) (.var 5))) (.var 6)))134            (.mul (.mul (.neg (.mul (.add (.var 1) (.var 1)) (.var 2))) (.var 3))135                  (.mul (.add (.mul (.var 4) (.var 4)) (.mul (.var 0) (.mul (.var 5) (.var 5)))) (.var 6))))136      (by decide +kernel)137138/-- 8:D15 — the identity: `Λ(1, 0) = 1` (with the inverse `1` of `δ = 1`). -/139theorem boost_one (ν : Shell p) : boostOf ν 1 0 1 = 1 := by140  apply Ext.ext141  · show (1 * 1 + ν * (0 * 0)) * 1 = 1142    rw [Shell.mul_one, Shell.mul_zero, Shell.mul_zero, Shell.add_zero]; exact Shell.one_mul 1143  · show -((1 + 1) * 0) * 1 = 0144    rw [Shell.mul_zero, Shell.neg_zero]; exact Shell.zero_mul 1145146/-- 8:D15 — the inverse: `Λ(x, −y)` is the conjugate of `Λ(x, y)`, and a norm-one element times its conjugate is147`1` (`conj_inv_of_norm_one`), so `Λ(x, −y) = Λ(x, y)⁻¹`. -/148theorem boost_conj (ν x y u : Shell p) : boostOf ν x (-y) u = Ext.conj (boostOf ν x y u) := by149  apply Ext.ext150  · show (x * x + ν * (-y * -y)) * u = (x * x + ν * (y * y)) * u151    rw [Shell.neg_mul_neg]152  · show -((x + x) * -y) * u = -(-((x + x) * y) * u)153    rw [← Shell.mul_neg, Shell.neg_neg, ← Shell.neg_mul, Shell.neg_neg]154155/-- 8:D15 — `Λ(x, y) Λ(x, −y) = 1`: the boosts form a group under the product of the extension, with the conjugate156as the inverse. -/157theorem boost_inv (ν x y u : Shell p) (hu : (x * x + -(ν * (y * y))) * u = 1) :158    boostOf ν x y u * boostOf ν x (-y) u = 1 := by159  rw [boost_conj]160  exact Ext.conj_inv_of_norm_one _ (boost_entries_norm ν x y u hu)161162end boosts163164/-! ## 8:F7 — the dispersion relation on the characters -/165section dispersion166variable {κ : Nat} {g : Shell p}167168/-- 8:F7 — the dispersion relation: on the drive cycle, `χ_k(j) = g^{jk}` and the cycle Laplacian169`(Δχ)(j) = χ(j+1) + χ(j−1) − 2χ(j)` acts on `χ_k` as the scalar `g^k + g^{−k} − 2`: at the site `j + 1`,170`χ_k(j+2) = g^k χ_k(j+1)` and `χ_k(j) = y^k χ_k(j+1)` with `y = g⁻¹` (`drive_eigen`). -/171theorem dispersion {y : Shell p} (hy : g * y = 1) (j k : Nat) :172    g ^ ((j + 2) * k) + g ^ (j * k) + -(2 * g ^ ((j + 1) * k)) = (g ^ k + y ^ k + -2) * g ^ ((j + 1) * k) := by173  have h1 : g ^ ((j + 2) * k) = g ^ k * g ^ ((j + 1) * k) := by174    have e : (j + 2) * k = k + (j + 1) * k := by175      rw [show j + 2 = j + 1 + 1 from rfl, Nat.add_mul (j + 1) 1 k, Nat.one_mul, Nat.add_comm]176    rw [e, Shell.pow_add]177  rw [h1, ← drive_eigen hy j k, Shell.right_distrib, Shell.right_distrib, ← Shell.neg_mul]178179end dispersion180181/-! ## 8:C16 — the gauge `α ↦ −α` inverts the Cayley map -/182section gauge183184/-- The scalar Cayley map `φ(λ) = (1 + λw)/(1 − λw)` with the inverse `u` of the norm `1 − νλ²` supplied:185`(1 + λw) · conj(1 − λw) · u`. The theme's `phi` is this with the searched inverse. -/186def phiU (ν lam u : Shell p) : Ext p ν := (⟨1, lam⟩ : Ext p ν) * Ext.conj ⟨1, -lam⟩ * Ext.ofShell u187188/-- The gauge-flipped map `φ⁻(λ) = (1 − λw)/(1 + λw)` (the parameter `−α`), the same inverse: the norms of189`1 ± λw` agree. -/190def phiNegU (ν lam u : Shell p) : Ext p ν := (⟨1, -lam⟩ : Ext p ν) * Ext.conj ⟨1, lam⟩ * Ext.ofShell u191192/-- 8:C16 — the orientation gauge inverts every value of the Cayley map: `φ⁻(λ) φ(λ) = 1` when `(1 − νλ²) u = 1`193(the product is `(N u)²` on the real line and `0` on the imaginary one, two polynomial identities). -/194theorem cayley_gauge (ν lam u : Shell p) (hu : (1 + -(ν * (lam * lam))) * u = 1) :195    phiNegU ν lam u * phiU ν lam u = 1 := by196  have h1 : phiU ν lam u = ⟨(1 * 1 + ν * (lam * lam)) * u + ν * ((1 * lam + lam * 1) * 0), (1 * 1 + ν * (lam * lam)) * 0 + (1 * lam + lam * 1) * u⟩ := by197    unfold phiU198    rw [show Ext.conj (⟨1, -lam⟩ : Ext p ν) = ⟨1, lam⟩ from Ext.ext rfl (Shell.neg_neg lam)]199    rfl200  have h2 : phiNegU ν lam u = ⟨(1 * 1 + ν * (-lam * -lam)) * u + ν * ((1 * -lam + -lam * 1) * 0), (1 * 1 + ν * (-lam * -lam)) * 0 + (1 * -lam + -lam * 1) * u⟩ := by201    unfold phiNegU; rfl202  rw [h2, h1]203  apply Ext.ext204  · show ((1 * 1 + ν * (-lam * -lam)) * u + ν * ((1 * -lam + -lam * 1) * 0)) * ((1 * 1 + ν * (lam * lam)) * u + ν * ((1 * lam + lam * 1) * 0)) + ν * (((1 * 1 + ν * (-lam * -lam)) * 0 + (1 * -lam + -lam * 1) * u) * ((1 * 1 + ν * (lam * lam)) * 0 + (1 * lam + lam * 1) * u)) = 1205    have e : ((1 * 1 + ν * (-lam * -lam)) * u + ν * ((1 * -lam + -lam * 1) * 0)) * ((1 * 1 + ν * (lam * lam)) * u + ν * ((1 * lam + lam * 1) * 0)) + ν * (((1 * 1 + ν * (-lam * -lam)) * 0 + (1 * -lam + -lam * 1) * u) * ((1 * 1 + ν * (lam * lam)) * 0 + (1 * lam + lam * 1) * u)) = ((1 + -(ν * (lam * lam))) * u) * ((1 + -(ν * (lam * lam))) * u) :=206      RE.sound (look [ν, lam, u])207        (.add (.mul (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.var 2)) (.mul (.var 0) (.mul (.add (.mul .one (.neg (.var 1))) (.mul (.neg (.var 1)) .one)) .zero))) (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.var 1) (.var 1)))) (.var 2)) (.mul (.var 0) (.mul (.add (.mul .one (.var 1)) (.mul (.var 1) .one)) .zero)))) (.mul (.var 0) (.mul (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1))))) .zero) (.mul (.add (.mul .one (.neg (.var 1))) (.mul (.neg (.var 1)) .one)) (.var 2))) (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.var 1) (.var 1)))) .zero) (.mul (.add (.mul .one (.var 1)) (.mul (.var 1) .one)) (.var 2))))))208        (.mul (.mul (.add .one (.neg (.mul (.var 0) (.mul (.var 1) (.var 1))))) (.var 2)) (.mul (.add .one (.neg (.mul (.var 0) (.mul (.var 1) (.var 1))))) (.var 2)))209        (by decide +kernel)210    rw [e, hu]; exact Shell.one_mul 1211  · show ((1 * 1 + ν * (-lam * -lam)) * u + ν * ((1 * -lam + -lam * 1) * 0)) * ((1 * 1 + ν * (lam * lam)) * 0 + (1 * lam + lam * 1) * u) + ((1 * 1 + ν * (-lam * -lam)) * 0 + (1 * -lam + -lam * 1) * u) * ((1 * 1 + ν * (lam * lam)) * u + ν * ((1 * lam + lam * 1) * 0)) = 0212    exact RE.sound (look [ν, lam, u])213      (.add (.mul (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1))))) (.var 2)) (.mul (.var 0) (.mul (.add (.mul .one (.neg (.var 1))) (.mul (.neg (.var 1)) .one)) .zero))) (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.var 1) (.var 1)))) .zero) (.mul (.add (.mul .one (.var 1)) (.mul (.var 1) .one)) (.var 2)))) (.mul (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.neg (.var 1)) (.neg (.var 1))))) .zero) (.mul (.add (.mul .one (.neg (.var 1))) (.mul (.neg (.var 1)) .one)) (.var 2))) (.add (.mul (.add (.mul .one .one) (.mul (.var 0) (.mul (.var 1) (.var 1)))) (.var 2)) (.mul (.var 0) (.mul (.add (.mul .one (.var 1)) (.mul (.var 1) .one)) .zero)))))214      .zero215      (by decide +kernel)216217end gauge218219end FRC.Dirac.Plane220