Theme/Lorentz.lean — FrcMathlib

1import Mathlib23/-!4# FrcMathlib.Theme.Lorentz — no definite space (7:D5), on Mathlib56The projective theme's Mathlib file for 7-spacetime (31 October 2026). The register square of the shell carries the7determinant form `Q_ν(x) = x₀² − x₁² − x₃² + ν x₂²` on `𝔽_p⁴`; every three-dimensional subspace contains a nonzero null8vector, so no form on space is definite. The restriction of `Q_ν` to the span of three vectors `u, v, w` is a quadratic9polynomial in the three coefficients, of total degree at most two in three variables, and the Chevalley–Warning theorem10(`char_dvd_card_solutions`) makes its number of zeros a multiple of `p`; the zero vector is one, so there is a second,11nonzero one (`isotropic_three`). The clause is stated for every prime `p` and every `ν`; the core proves the other clauses12of the row's theorem (`FrcCore/Theme/Lorentz.lean`). Classical, on Mathlib's hierarchy.13-/1415namespace FRC.Lorentz1617open MvPolynomial1819variable {p : ℕ} [hp : Fact p.Prime]2021/-- The determinant form of the register square on the coordinates `(x₀, x₁, x₂, x₃)`. -/22def Qf (ν : ZMod p) (x : Fin 4 → ZMod p) : ZMod p := x 0 ^ 2 - x 1 ^ 2 - x 3 ^ 2 + ν * x 2 ^ 22324/-- The linear form `a u_i + b v_i + c w_i` in the three coefficients, as a polynomial. -/25noncomputable def lin (u v w : Fin 4 → ZMod p) (i : Fin 4) : MvPolynomial (Fin 3) (ZMod p) :=26  C (u i) * X 0 + C (v i) * X 1 + C (w i) * X 22728/-- The restriction of `Q_ν` to the span of `u, v, w`, as a polynomial in the coefficients. -/29noncomputable def restr (ν : ZMod p) (u v w : Fin 4 → ZMod p) : MvPolynomial (Fin 3) (ZMod p) :=30  lin u v w 0 * lin u v w 0 - lin u v w 1 * lin u v w 1 - lin u v w 3 * lin u v w 3 +31    C ν * (lin u v w 2 * lin u v w 2)3233theorem lin_totalDegree (u v w : Fin 4 → ZMod p) (i : Fin 4) : (lin u v w i).totalDegree ≤ 1 := by34  unfold lin35  refine le_trans (totalDegree_add _ _) (max_le (le_trans (totalDegree_add _ _) (max_le ?_ ?_)) ?_) <;>36  · refine le_trans (totalDegree_mul _ _) ?_37    rw [totalDegree_C, totalDegree_X]3839theorem restr_totalDegree (ν : ZMod p) (u v w : Fin 4 → ZMod p) : (restr ν u v w).totalDegree ≤ 2 := by40  have sq : ∀ i, (lin u v w i * lin u v w i).totalDegree ≤ 2 := fun i =>41    le_trans (totalDegree_mul _ _) (by have := lin_totalDegree u v w i; omega)42  have cs : (C ν * (lin u v w 2 * lin u v w 2)).totalDegree ≤ 2 :=43    le_trans (totalDegree_mul _ _) (by rw [totalDegree_C]; have := sq 2; omega)44  unfold restr45  refine le_trans (totalDegree_add _ _) (max_le (le_trans (totalDegree_sub _ _) (max_le (le_trans (totalDegree_sub _ _) (max_le ?_ ?_)) ?_)) ?_)46  · exact sq 047  · exact sq 148  · exact sq 349  · exact cs5051theorem eval_lin (u v w : Fin 4 → ZMod p) (i : Fin 4) (a : Fin 3 → ZMod p) :52    eval a (lin u v w i) = a 0 * u i + a 1 * v i + a 2 * w i := by53  unfold lin; simp [mul_comm]5455/-- The polynomial evaluates to `Q_ν` of the combination `a₀ u + a₁ v + a₂ w`. -/56theorem eval_restr (ν : ZMod p) (u v w : Fin 4 → ZMod p) (a : Fin 3 → ZMod p) :57    eval a (restr ν u v w) = Qf ν (a 0 • u + a 1 • v + a 2 • w) := by58  unfold restr Qf59  simp only [eval_add, eval_sub, eval_mul, eval_C, eval_lin, Pi.add_apply, Pi.smul_apply, smul_eq_mul]60  ring6162/-- 7:D5 — **no definite space.** On every prime shell `p` and for every `ν`, any three vectors `u, v, w` of `𝔽_p⁴` admit63coefficients `(a₀, a₁, a₂) ≠ 0` with `Q_ν(a₀ u + a₁ v + a₂ w) = 0`: a three-dimensional subspace of the register square64contains a nonzero null vector (Chevalley–Warning: the restricted form has degree two in three variables, its zeros number a65multiple of `p`, and the zero coefficients are one of them). -/66theorem isotropic_three (ν : ZMod p) (u v w : Fin 4 → ZMod p) :67    ∃ a : Fin 3 → ZMod p, a ≠ 0 ∧ Qf ν (a 0 • u + a 1 • v + a 2 • w) = 0 := by68  classical69  have hdeg : (restr ν u v w).totalDegree < Fintype.card (Fin 3) := by70    have := restr_totalDegree ν u v w; simp; omega71  have hdvd := char_dvd_card_solutions (K := ZMod p) (σ := Fin 3) p hdeg72  let S := { x : Fin 3 → ZMod p // eval x (restr ν u v w) = 0 }73  have z0 : eval (0 : Fin 3 → ZMod p) (restr ν u v w) = 0 := by74    rw [eval_restr]; simp [Qf]75  have hpos : 0 < Fintype.card S := Fintype.card_pos_iff.mpr ⟨⟨0, z0⟩⟩76  have hle : p ≤ Fintype.card S := Nat.le_of_dvd hpos hdvd77  have h1 : 1 < Fintype.card S := lt_of_lt_of_le hp.out.one_lt hle78  obtain ⟨b, hb⟩ := Fintype.exists_ne_of_one_lt_card h1 (⟨0, z0⟩ : S)79  refine ⟨b.1, fun h0 => hb (Subtype.ext h0), ?_⟩80  rw [← eval_restr]; exact b.28182end FRC.Lorentz83