Theme/Symbol.lean — FrcCore

1import FrcCore.Ring2import FrcCore.Series34/-!5# FrcCore.Theme.Symbol — the symbol lemmas of the curvature-square uniqueness (the gravity theme, task LM40)67The first step of the master's E1 (p00052): at a fixed symbol `k`, the gauge-invariant quadratic forms of the8relevant (two-derivative) order form one line, for the vector field and for the symmetric tensor field. The symbol9`k`, the fields and the gauge parameters are vectors `Nat → Shell p` in `n` dimensions. The metric is diagonal,10`η : Nat → Shell p`, so `u·v = Σ_{μ<n} η_μ u_μ v_μ` (`dot`) covers the Euclidean and the Lorentzian signature.11Nothing is assumed of the modulus `p` beyond `Pos p`, so the identities hold on every shell.1213* Spin 1. The form `a₁ k² A·A + a₂ (k·A)²` (`vecForm`) changes under the gauge shift `A ↦ A + z k` (`shift`) by14  `(a₁ + a₂) k² (2z (k·A) + z² k²)`, a polynomial identity in `z` (`vec_shift`). So `a₁ + a₂ = 0`, the symbol of15  `F²`, is invariant at every symbol (`vec_invariant`). When `k²` is a unit the converse holds at that symbol16  (`vec_iff_unit`). A null symbol, `k² = 0`, leaves every form invariant (`vec_null`). Over all symbols the invariant17  forms are exactly the line `a₁ + a₂ = 0` once one metric entry is a unit (`maxwell_unique`).18* Spin 2. The four scalars of a symmetric `h` are `k² ⟨h, h⟩`, `(k·h)·(k·h)`, `(k·h·k) tr h` and `k² (tr h)²`, the19  symbols of `∂h ∂h`, `∂·h ∂·h`, `∂·h ∂ tr h` and `∂ tr h ∂ tr h` (`tensForm`). Under `h_μν ↦ h_μν + k_μ ξ_ν + k_ν ξ_μ`20  (`gauge`) the combination changes by three gauge structures with coefficients `2a₁ + a₂`, `a₂ + a₃` and21  `a₃ + 2a₄` (`tens_shift`). The Fierz–Pauli line `(−1, 2, −2, 1)` is invariant on every shell22  (`fierz_pauli_invariant`). When `2` and two metric entries are units and `n ≥ 2`, it is the only invariant line23  (`fierz_pauli_unique`). In characteristic 2 the uniqueness fails: `k² ⟨h, h⟩` alone is invariant there24  (`char_two_not_unique`).2526The ring identities are decided by the core's normaliser (`RE.sound`, a kernel computation). The sums are handled by27`sumRange` and its linearity. No axioms.28-/2930namespace FRC.Symbol3132open FRC.Shell FRC.Shell.Frame3334variable {p : Nat} [Pos p]3536/-! ## Sums -/3738/-- Double sums commute: `Σ_{i<n} Σ_{j<m} f i j = Σ_{j<m} Σ_{i<n} f i j`. -/39theorem sum_swap (f : Nat → Nat → Shell p) (m : Nat) : ∀ n,40    sumRange (fun i => sumRange (fun j => f i j) m) n = sumRange (fun j => sumRange (fun i => f i j) n) m41  | 0 => (sum_zero m (fun _ _ => rfl)).symm42  | n + 1 => by43    rw [sumRange_succ, sum_swap f m n, ← sum_add]44    rfl4546theorem lin2_zero (c : Shell p) : 0 = 0 + 0 * c :=47  RE.sound (look [c])48    .zero49    (.add .zero (.mul .zero (.var 0))) (by decide +kernel)5051theorem lin2_step (S T a b c : Shell p) : S + T * c + (a + b * c) = S + a + (T + b) * c :=52  RE.sound (look [S, T, a, b, c])53    (.add (.add (.var 0) (.mul (.var 1) (.var 4))) (.add (.var 2) (.mul (.var 3) (.var 4))))54    (.add (.add (.var 0) (.var 2)) (.mul (.add (.var 1) (.var 3)) (.var 4))) (by decide +kernel)5556/-- A sum of two terms with constant coefficients. -/57theorem sum_lin2 (f g : Nat → Shell p) (c : Shell p) : ∀ n,58    sumRange (fun μ => f μ + g μ * c) n = sumRange f n + sumRange g n * c59  | 0 => lin2_zero c60  | n + 1 => by61    show sumRange (fun μ => f μ + g μ * c) n + (f n + g n * c) = sumRange f n + f n + (sumRange g n + g n) * c62    rw [sum_lin2 f g c n]; exact lin2_step _ _ _ _ _6364theorem lin3_zero (c d : Shell p) : 0 = 0 + 0 * c + 0 * d :=65  RE.sound (look [c, d])66    .zero67    (.add (.add .zero (.mul .zero (.var 0))) (.mul .zero (.var 1))) (by decide +kernel)6869theorem lin3_step (S T U a b e c d : Shell p) :70    S + T * c + U * d + (a + b * c + e * d) = S + a + (T + b) * c + (U + e) * d :=71  RE.sound (look [S, T, U, a, b, e, c, d])72    (.add (.add (.add (.var 0) (.mul (.var 1) (.var 6))) (.mul (.var 2) (.var 7))) (.add (.add (.var 3) (.mul (.var 4) (.var 6))) (.mul (.var 5) (.var 7))))73    (.add (.add (.add (.var 0) (.var 3)) (.mul (.add (.var 1) (.var 4)) (.var 6))) (.mul (.add (.var 2) (.var 5)) (.var 7))) (by decide +kernel)7475/-- A sum of three terms with constant coefficients. -/76theorem sum_lin3 (f g h : Nat → Shell p) (c d : Shell p) : ∀ n,77    sumRange (fun μ => f μ + g μ * c + h μ * d) n = sumRange f n + sumRange g n * c + sumRange h n * d78  | 0 => lin3_zero c d79  | n + 1 => by80    show sumRange (fun μ => f μ + g μ * c + h μ * d) n + (f n + g n * c + h n * d) =81      sumRange f n + f n + (sumRange g n + g n) * c + (sumRange h n + h n) * d82    rw [sum_lin3 f g h c d n]; exact lin3_step _ _ _ _ _ _ _ _8384theorem lin6_zero (c₁ c₂ c₃ c₄ c₅ : Shell p) : 0 = 0 + 0 * c₁ + 0 * c₂ + 0 * c₃ + 0 * c₄ + 0 * c₅ :=85  RE.sound (look [c₁, c₂, c₃, c₄, c₅])86    .zero87    (.add (.add (.add (.add (.add .zero (.mul .zero (.var 0))) (.mul .zero (.var 1))) (.mul .zero (.var 2))) (.mul .zero (.var 3))) (.mul .zero (.var 4))) (by decide +kernel)8889theorem lin6_step (S₀ S₁ S₂ S₃ S₄ S₅ b₀ b₁ b₂ b₃ b₄ b₅ c₁ c₂ c₃ c₄ c₅ : Shell p) :90    S₀ + S₁ * c₁ + S₂ * c₂ + S₃ * c₃ + S₄ * c₄ + S₅ * c₅ + (b₀ + b₁ * c₁ + b₂ * c₂ + b₃ * c₃ + b₄ * c₄ + b₅ * c₅) =91      S₀ + b₀ + (S₁ + b₁) * c₁ + (S₂ + b₂) * c₂ + (S₃ + b₃) * c₃ + (S₄ + b₄) * c₄ + (S₅ + b₅) * c₅ :=92  RE.sound (look [S₀, S₁, S₂, S₃, S₄, S₅, b₀, b₁, b₂, b₃, b₄, b₅, c₁, c₂, c₃, c₄, c₅])93    (.add (.add (.add (.add (.add (.add (.var 0) (.mul (.var 1) (.var 12))) (.mul (.var 2) (.var 13))) (.mul (.var 3) (.var 14))) (.mul (.var 4) (.var 15))) (.mul (.var 5) (.var 16))) (.add (.add (.add (.add (.add (.var 6) (.mul (.var 7) (.var 12))) (.mul (.var 8) (.var 13))) (.mul (.var 9) (.var 14))) (.mul (.var 10) (.var 15))) (.mul (.var 11) (.var 16))))94    (.add (.add (.add (.add (.add (.add (.var 0) (.var 6)) (.mul (.add (.var 1) (.var 7)) (.var 12))) (.mul (.add (.var 2) (.var 8)) (.var 13))) (.mul (.add (.var 3) (.var 9)) (.var 14))) (.mul (.add (.var 4) (.var 10)) (.var 15))) (.mul (.add (.var 5) (.var 11)) (.var 16))) (by decide +kernel)9596/-- A sum of six terms with constant coefficients. -/97theorem sum_lin6 (f₀ f₁ f₂ f₃ f₄ f₅ : Nat → Shell p) (c₁ c₂ c₃ c₄ c₅ : Shell p) : ∀ n,98    sumRange (fun μ => f₀ μ + f₁ μ * c₁ + f₂ μ * c₂ + f₃ μ * c₃ + f₄ μ * c₄ + f₅ μ * c₅) n =99      sumRange f₀ n + sumRange f₁ n * c₁ + sumRange f₂ n * c₂ + sumRange f₃ n * c₃ + sumRange f₄ n * c₄ +100        sumRange f₅ n * c₅101  | 0 => lin6_zero c₁ c₂ c₃ c₄ c₅102  | n + 1 => by103    show sumRange (fun μ => f₀ μ + f₁ μ * c₁ + f₂ μ * c₂ + f₃ μ * c₃ + f₄ μ * c₄ + f₅ μ * c₅) n +104        (f₀ n + f₁ n * c₁ + f₂ n * c₂ + f₃ n * c₃ + f₄ n * c₄ + f₅ n * c₅) =105      sumRange f₀ n + f₀ n + (sumRange f₁ n + f₁ n) * c₁ + (sumRange f₂ n + f₂ n) * c₂ +106        (sumRange f₃ n + f₃ n) * c₃ + (sumRange f₄ n + f₄ n) * c₄ + (sumRange f₅ n + f₅ n) * c₅107    rw [sum_lin6 f₀ f₁ f₂ f₃ f₄ f₅ c₁ c₂ c₃ c₄ c₅ n]; exact lin6_step _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _108109/-! ## The metric pairing -/110111/-- The metric pairing `u·v = Σ_{μ<n} η_μ u_μ v_μ` for a diagonal metric `η`. -/112def dot (η : Nat → Shell p) (n : Nat) (u v : Nat → Shell p) : Shell p := sumRange (fun μ => η μ * u μ * v μ) n113114theorem comm_pt (e u v : Shell p) : e * u * v = e * v * u :=115  RE.sound (look [e, u, v])116    (.mul (.mul (.var 0) (.var 1)) (.var 2))117    (.mul (.mul (.var 0) (.var 2)) (.var 1)) (by decide +kernel)118119theorem dot_comm (η : Nat → Shell p) (n : Nat) (u v : Nat → Shell p) : dot η n u v = dot η n v u :=120  sum_congr n (fun _ _ => comm_pt _ _ _)121122theorem dot_zero_left (η : Nat → Shell p) (n : Nat) {u : Nat → Shell p} (v : Nat → Shell p) (hu : ∀ μ, u μ = 0) :123    dot η n u v = 0 :=124  sum_zero n (fun μ _ => by show η μ * u μ * v μ = 0; rw [hu μ, mul_zero, zero_mul])125126theorem lin2_pt (e w u x c : Shell p) : e * (w + c * u) * x = e * w * x + e * u * x * c :=127  RE.sound (look [e, w, u, x, c])128    (.mul (.mul (.var 0) (.add (.var 1) (.mul (.var 4) (.var 2)))) (.var 3))129    (.add (.mul (.mul (.var 0) (.var 1)) (.var 3)) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 3)) (.var 4))) (by decide +kernel)130131/-- The pairing is linear in its first slot (two terms). -/132theorem dot_lin2 (η : Nat → Shell p) (n : Nat) {W w u : Nat → Shell p} {c : Shell p}133    (hW : ∀ μ, W μ = w μ + c * u μ) (x : Nat → Shell p) :134    dot η n W x = dot η n w x + dot η n u x * c :=135  (sum_congr n (fun μ _ => by rw [hW μ]; exact lin2_pt _ _ _ _ _)).trans (sum_lin2 _ _ c n)136137theorem lin3_pt (e w u v c d x : Shell p) :138    e * (w + c * u + d * v) * x = e * w * x + e * u * x * c + e * v * x * d :=139  RE.sound (look [e, w, u, v, c, d, x])140    (.mul (.mul (.var 0) (.add (.add (.var 1) (.mul (.var 4) (.var 2))) (.mul (.var 5) (.var 3)))) (.var 6))141    (.add (.add (.mul (.mul (.var 0) (.var 1)) (.var 6)) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 6)) (.var 4))) (.mul (.mul (.mul (.var 0) (.var 3)) (.var 6)) (.var 5))) (by decide +kernel)142143/-- The pairing is linear in its first slot (three terms). -/144theorem dot_lin3 (η : Nat → Shell p) (n : Nat) {W w u v : Nat → Shell p} {c d : Shell p}145    (hW : ∀ μ, W μ = w μ + c * u μ + d * v μ) (x : Nat → Shell p) :146    dot η n W x = dot η n w x + dot η n u x * c + dot η n v x * d :=147  (sum_congr n (fun μ _ => by rw [hW μ]; exact lin3_pt _ _ _ _ _ _ _)).trans (sum_lin3 _ _ _ c d n)148149theorem quad2_pt (e w u c : Shell p) :150    e * (w + c * u) * (w + c * u) = e * w * w + e * w * u * ((1 + 1) * c) + e * u * u * (c * c) :=151  RE.sound (look [e, w, u, c])152    (.mul (.mul (.var 0) (.add (.var 1) (.mul (.var 3) (.var 2)))) (.add (.var 1) (.mul (.var 3) (.var 2))))153    (.add (.add (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.mul (.add .one .one) (.var 3)))) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.mul (.var 3) (.var 3)))) (by decide +kernel)154155/-- The square of a two-term combination. -/156theorem dot_quad2 (η : Nat → Shell p) (n : Nat) {W w u : Nat → Shell p} {c : Shell p}157    (hW : ∀ μ, W μ = w μ + c * u μ) :158    dot η n W W = dot η n w w + dot η n w u * ((1 + 1) * c) + dot η n u u * (c * c) :=159  (sum_congr n (fun μ _ => by rw [hW μ]; exact quad2_pt _ _ _ _)).trans (sum_lin3 _ _ _ _ _ n)160161theorem quad3_pt (e w u v c d : Shell p) :162    e * (w + c * u + d * v) * (w + c * u + d * v) = e * w * w + e * u * u * (c * c) + e * v * v * (d * d) +163      e * w * u * ((1 + 1) * c) + e * w * v * ((1 + 1) * d) + e * u * v * ((1 + 1) * c * d) :=164  RE.sound (look [e, w, u, v, c, d])165    (.mul (.mul (.var 0) (.add (.add (.var 1) (.mul (.var 4) (.var 2))) (.mul (.var 5) (.var 3)))) (.add (.add (.var 1) (.mul (.var 4) (.var 2))) (.mul (.var 5) (.var 3))))166    (.add (.add (.add (.add (.add (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 2)) (.mul (.var 4) (.var 4)))) (.mul (.mul (.mul (.var 0) (.var 3)) (.var 3)) (.mul (.var 5) (.var 5)))) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.mul (.add .one .one) (.var 4)))) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 3)) (.mul (.add .one .one) (.var 5)))) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 3)) (.mul (.mul (.add .one .one) (.var 4)) (.var 5)))) (by decide +kernel)167168/-- The square of a three-term combination. -/169theorem dot_quad3 (η : Nat → Shell p) (n : Nat) {W w u v : Nat → Shell p} {c d : Shell p}170    (hW : ∀ μ, W μ = w μ + c * u μ + d * v μ) :171    dot η n W W = dot η n w w + dot η n u u * (c * c) + dot η n v v * (d * d) + dot η n w u * ((1 + 1) * c) +172      dot η n w v * ((1 + 1) * d) + dot η n u v * ((1 + 1) * c * d) :=173  (sum_congr n (fun μ _ => by rw [hW μ]; exact quad3_pt _ _ _ _ _ _)).trans (sum_lin6 _ _ _ _ _ _ _ _ _ _ _ n)174175/-! ## Spin 1: the vector field -/176177/-- The gauge shift `A ↦ A + z k`. -/178def shift (A k : Nat → Shell p) (z : Shell p) : Nat → Shell p := fun μ => A μ + z * k μ179180/-- The two relevant quadratic scalars of a vector field at the symbol `k`: `a₁ k² A·A + a₂ (k·A)²`. -/181def vecForm (η : Nat → Shell p) (n : Nat) (a₁ a₂ : Shell p) (k A : Nat → Shell p) : Shell p :=182  a₁ * dot η n k k * dot η n A A + a₂ * (dot η n k A * dot η n k A)183184theorem vec_ring (a₁ a₂ K B C z : Shell p) :185    a₁ * K * (C + B * ((1 + 1) * z) + K * (z * z)) + a₂ * ((B + K * z) * (B + K * z)) =186      a₁ * K * C + a₂ * (B * B) + (a₁ + a₂) * K * (z * ((1 + 1) * B) + z * z * K) :=187  RE.sound (look [a₁, a₂, K, B, C, z])188    (.add (.mul (.mul (.var 0) (.var 2)) (.add (.add (.var 4) (.mul (.var 3) (.mul (.add .one .one) (.var 5)))) (.mul (.var 2) (.mul (.var 5) (.var 5))))) (.mul (.var 1) (.mul (.add (.var 3) (.mul (.var 2) (.var 5))) (.add (.var 3) (.mul (.var 2) (.var 5))))))189    (.add (.add (.mul (.mul (.var 0) (.var 2)) (.var 4)) (.mul (.var 1) (.mul (.var 3) (.var 3)))) (.mul (.mul (.add (.var 0) (.var 1)) (.var 2)) (.add (.mul (.var 5) (.mul (.add .one .one) (.var 3))) (.mul (.mul (.var 5) (.var 5)) (.var 2))))) (by decide +kernel)190191/-- Spin 1, the gauge variation as a polynomial identity in `z`, on every shell, in every dimension and metric:192`a₁ k² (A + zk)² + a₂ (k·(A + zk))² = a₁ k² A² + a₂ (k·A)² + (a₁ + a₂) k² (2z (k·A) + z² k²)`. -/193theorem vec_shift (η : Nat → Shell p) (n : Nat) (a₁ a₂ : Shell p) (k A : Nat → Shell p) (z : Shell p) :194    vecForm η n a₁ a₂ k (shift A k z) = vecForm η n a₁ a₂ k A +195      (a₁ + a₂) * dot η n k k * (z * ((1 + 1) * dot η n k A) + z * z * dot η n k k) := by196  have e₁ : dot η n k (shift A k z) = dot η n k A + dot η n k k * z := by197    rw [dot_comm η n k (shift A k z), dot_lin2 η n (W := shift A k z) (w := A) (u := k) (c := z) (fun _ => rfl) k, dot_comm η n A k]198  have e₂ : dot η n (shift A k z) (shift A k z) =199      dot η n A A + dot η n k A * ((1 + 1) * z) + dot η n k k * (z * z) := by200    rw [dot_quad2 η n (W := shift A k z) (w := A) (u := k) (c := z) (fun _ => rfl), dot_comm η n A k]201  unfold vecForm202  rw [e₁, e₂]203  exact vec_ring _ _ _ _ _ _204205/-- 00:E1 — spin 1: the line `a₁ + a₂ = 0`, the symbol of `F²`, is gauge invariant at every symbol. -/206theorem vec_invariant (η : Nat → Shell p) (n : Nat) {a₁ a₂ : Shell p} (h : a₁ + a₂ = 0) (k A : Nat → Shell p)207    (z : Shell p) : vecForm η n a₁ a₂ k (shift A k z) = vecForm η n a₁ a₂ k A := by208  rw [vec_shift, h, zero_mul, zero_mul, add_zero]209210/-- Spin 1 at a null symbol, `k² = 0`: every form is gauge invariant, so the symbol decides nothing there. -/211theorem vec_null (η : Nat → Shell p) (n : Nat) (a₁ a₂ : Shell p) {k : Nat → Shell p} (hk : dot η n k k = 0)212    (A : Nat → Shell p) (z : Shell p) : vecForm η n a₁ a₂ k (shift A k z) = vecForm η n a₁ a₂ k A := by213  rw [vec_shift, hk, mul_zero, zero_mul, add_zero]214215/-! ## Cancellation helpers -/216217theorem eq_zero_of_add_left {a b : Shell p} (h : a + b = a) : b = 0 :=218  add_right_cancel (c := a) (by rw [add_comm, h, zero_add])219220theorem sub_one_zero {a : Shell p} (h : a = 1) : a + -1 = 0 := by rw [h]; exact add_neg 1221222theorem lc2 {L R x y e f : Shell p} (h : L = R + x * e + y * f) (he : e = 0) (hf : f = 0) : L = R := by223  rw [h, he, hf, mul_zero, mul_zero, add_zero, add_zero]224225theorem lc4 {L R x y z w e f g u : Shell p} (h : L = R + x * e + y * f + z * g + w * u) (he : e = 0) (hf : f = 0)226    (hg : g = 0) (hu : u = 0) : L = R := by227  rw [h, he, hf, hg, hu, mul_zero, mul_zero, mul_zero, mul_zero, add_zero, add_zero, add_zero, add_zero]228229theorem cancel3_ring (c x y z x' y' z' : Shell p) :230    c * (x * x' * (y * y') * (z * z')) = c * (x * y * z) * (x' * y' * z') :=231  RE.sound (look [c, x, y, z, x', y', z'])232    (.mul (.var 0) (.mul (.mul (.mul (.var 1) (.var 4)) (.mul (.var 2) (.var 5))) (.mul (.var 3) (.var 6))))233    (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 2)) (.var 3))) (.mul (.mul (.var 4) (.var 5)) (.var 6))) (by decide +kernel)234235/-- A product with three unit factors vanishes only if the cofactor does. -/236theorem cancel3 {c x y z x' y' z' : Shell p} (h : c * (x * y * z) = 0) (hx : x * x' = 1) (hy : y * y' = 1)237    (hz : z * z' = 1) : c = 0 := by238  have e := cancel3_ring c x y z x' y' z'239  rw [hx, hy, hz, h, zero_mul, one_mul, one_mul, mul_one] at e240  exact e241242theorem cancel4_ring (c x y z w x' y' z' w' : Shell p) :243    c * (x * x' * (y * y') * (z * z') * (w * w')) = c * (x * y * z * w) * (x' * y' * z' * w') :=244  RE.sound (look [c, x, y, z, w, x', y', z', w'])245    (.mul (.var 0) (.mul (.mul (.mul (.mul (.var 1) (.var 5)) (.mul (.var 2) (.var 6))) (.mul (.var 3) (.var 7))) (.mul (.var 4) (.var 8))))246    (.mul (.mul (.var 0) (.mul (.mul (.mul (.var 1) (.var 2)) (.var 3)) (.var 4))) (.mul (.mul (.mul (.var 5) (.var 6)) (.var 7)) (.var 8))) (by decide +kernel)247248/-- A product with four unit factors vanishes only if the cofactor does. -/249theorem cancel4 {c x y z w x' y' z' w' : Shell p} (h : c * (x * y * z * w) = 0) (hx : x * x' = 1)250    (hy : y * y' = 1) (hz : z * z' = 1) (hw : w * w' = 1) : c = 0 := by251  have e := cancel4_ring c x y z w x' y' z' w'252  rw [hx, hy, hz, hw, h, zero_mul, one_mul, one_mul, one_mul, mul_one] at e253  exact e254255theorem unit_ring (s K w : Shell p) :256    s = 0 + (w * w) * (s * K * (1 * ((1 + 1) * 0) + 1 * 1 * K)) + (-(s * (K * w + 1))) * (K * w + -1) :=257  RE.sound (look [s, K, w])258    (.var 0)259    (.add (.add .zero (.mul (.mul (.var 2) (.var 2)) (.mul (.mul (.var 0) (.var 1)) (.add (.mul .one (.mul (.add .one .one) .zero)) (.mul (.mul .one .one) (.var 1)))))) (.mul (.neg (.mul (.var 0) (.add (.mul (.var 1) (.var 2)) .one))) (.add (.mul (.var 1) (.var 2)) (.neg .one)))) (by decide +kernel)260261/-- Spin 1 at a symbol whose square `k²` is a unit: the form is gauge invariant exactly on the line `a₁ + a₂ = 0`. -/262theorem vec_iff_unit (η : Nat → Shell p) (n : Nat) (a₁ a₂ : Shell p) (k : Nat → Shell p) {w : Shell p}263    (hk : dot η n k k * w = 1) :264    (∀ (A : Nat → Shell p) (z : Shell p), vecForm η n a₁ a₂ k (shift A k z) = vecForm η n a₁ a₂ k A) ↔265      a₁ + a₂ = 0 := by266  constructor267  · intro h268    have h₀ := (vec_shift η n a₁ a₂ k (fun _ => 0) 1).symm.trans (h (fun _ => 0) 1)269    rw [dot_comm η n k (fun _ => 0), dot_zero_left η n (u := fun _ => 0) k (fun _ => rfl)] at h₀270    exact lc2 (unit_ring (a₁ + a₂) (dot η n k k) w) (eq_zero_of_add_left h₀) (sub_one_zero hk)271  · intro h A z272    exact vec_invariant η n h k A z273274/-! ## Coordinate vectors -/275276/-- The coordinate vector `e_i`. -/277def basis (i : Nat) : Nat → Shell p := fun μ => if μ = i then 1 else 0278279theorem basis_self (i : Nat) : basis (p := p) i i = 1 := ite_eq_left rfl280281theorem basis_ne {i μ : Nat} (h : μ ≠ i) : basis (p := p) i μ = 0 := ite_eq_right h282283theorem basis_mul_ne {i j : Nat} (hij : i ≠ j) (μ : Nat) : basis (p := p) i μ * basis j μ = 0 :=284  match Nat.decEq μ i with285  | isTrue e => by rw [basis_ne (fun e' => hij (e.symm.trans e')), mul_zero]286  | isFalse e => by rw [basis_ne e, zero_mul]287288theorem dot_basis_self (η : Nat → Shell p) {n i : Nat} (hi : i < n) : dot η n (basis i) (basis i) = η i :=289  (sum_eq_single hi (fun l _ hl => by290    show η l * basis i l * basis i l = 0291    rw [basis_ne hl, mul_zero])).trans (by292    show η i * basis i i * basis i i = η i293    rw [basis_self, mul_one, mul_one])294295theorem dot_basis_ne (η : Nat → Shell p) (n : Nat) {i j : Nat} (hij : i ≠ j) : dot η n (basis i) (basis j) = 0 :=296  sum_zero n (fun l _ => by297    show η l * basis i l * basis j l = 0298    rw [mul_assoc, basis_mul_ne hij, mul_zero])299300/-- 00:E1 — spin 1 over all symbols: when the metric entry `η₀` is a unit (`n ≥ 1`), the forms gauge invariant at every301symbol are exactly the line `a₁ + a₂ = 0`, Maxwell's `F²`. -/302theorem maxwell_unique (η : Nat → Shell p) {n : Nat} {w : Shell p} (hn : 0 < n) (h₀ : η 0 * w = 1)303    (a₁ a₂ : Shell p) :304    (∀ (k A : Nat → Shell p) (z : Shell p), vecForm η n a₁ a₂ k (shift A k z) = vecForm η n a₁ a₂ k A) ↔305      a₁ + a₂ = 0 :=306  ⟨fun h => (vec_iff_unit η n a₁ a₂ (basis 0) (w := w) (by rw [dot_basis_self η hn]; exact h₀)).mp (h (basis 0)),307   fun h k A z => vec_invariant η n h k A z⟩308309/-! ## Spin 2: the symmetric tensor field -/310311/-- The trace `tr h = Σ_μ η_μ h_μμ`. -/312def tr (η : Nat → Shell p) (n : Nat) (h : Nat → Nat → Shell p) : Shell p := sumRange (fun μ => η μ * h μ μ) n313314/-- The contraction `(u·h)_ν = Σ_μ η_μ u_μ h_μν`. -/315def ctr (η : Nat → Shell p) (n : Nat) (u : Nat → Shell p) (h : Nat → Nat → Shell p) : Nat → Shell p :=316  fun ν => sumRange (fun μ => η μ * u μ * h μ ν) n317318/-- The pairing `⟨h, h'⟩ = Σ_μ η_μ (h_μ · h'_μ)`, row by row. -/319def pair (η : Nat → Shell p) (n : Nat) (h h' : Nat → Nat → Shell p) : Shell p :=320  sumRange (fun μ => η μ * dot η n (h μ) (h' μ)) n321322/-- The gauge shift `h_μν ↦ h_μν + k_μ ξ_ν + k_ν ξ_μ`. -/323def gauge (h : Nat → Nat → Shell p) (k ξ : Nat → Shell p) : Nat → Nat → Shell p :=324  fun μ ν => h μ ν + (k μ * ξ ν + k ν * ξ μ)325326/-- The four two-derivative quadratic scalars of a symmetric field at the symbol `k`, combined:327`a₁ k² ⟨h, h⟩ + a₂ (k·h)·(k·h) + a₃ (k·h·k) tr h + a₄ k² (tr h)²`. -/328def tensForm (η : Nat → Shell p) (n : Nat) (a₁ a₂ a₃ a₄ : Shell p) (k : Nat → Shell p) (h : Nat → Nat → Shell p) :329    Shell p :=330  a₁ * (dot η n k k * pair η n h h) + a₂ * dot η n (ctr η n k h) (ctr η n k h) +331    a₃ * (dot η n (ctr η n k h) k * tr η n h) + a₄ * (dot η n k k * (tr η n h * tr η n h))332333theorem tr_pt (e h a b : Shell p) : e * (h + (a * b + a * b)) = e * h + e * a * b * (1 + 1) :=334  RE.sound (look [e, h, a, b])335    (.mul (.var 0) (.add (.var 1) (.add (.mul (.var 2) (.var 3)) (.mul (.var 2) (.var 3)))))336    (.add (.mul (.var 0) (.var 1)) (.mul (.mul (.mul (.var 0) (.var 2)) (.var 3)) (.add .one .one))) (by decide +kernel)337338theorem tr_gauge (η : Nat → Shell p) (n : Nat) (h : Nat → Nat → Shell p) (k ξ : Nat → Shell p) :339    tr η n (gauge h k ξ) = tr η n h + dot η n k ξ * (1 + 1) :=340  (sum_congr n (fun _ _ => tr_pt _ _ _ _)).trans (sum_lin2 _ _ _ n)341342theorem ctr_pt (e a h b c d : Shell p) :343    e * a * (h + (a * b + c * d)) = e * a * h + e * a * a * b + e * a * d * c :=344  RE.sound (look [e, a, h, b, c, d])345    (.mul (.mul (.var 0) (.var 1)) (.add (.var 2) (.add (.mul (.var 1) (.var 3)) (.mul (.var 4) (.var 5)))))346    (.add (.add (.mul (.mul (.var 0) (.var 1)) (.var 2)) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 1)) (.var 3))) (.mul (.mul (.mul (.var 0) (.var 1)) (.var 5)) (.var 4))) (by decide +kernel)347348theorem ctr_gauge (η : Nat → Shell p) (n : Nat) (k ξ : Nat → Shell p) (h : Nat → Nat → Shell p) (ν : Nat) :349    ctr η n k (gauge h k ξ) ν = ctr η n k h ν + dot η n k k * ξ ν + dot η n k ξ * k ν :=350  (sum_congr n (fun _ _ => ctr_pt _ _ _ _ _ _)).trans (sum_lin3 _ _ _ _ _ n)351352theorem rows_pt (a b c d e : Shell p) : a * (b * c * d) * e = b * c * (a * d * e) :=353  RE.sound (look [a, b, c, d, e])354    (.mul (.mul (.var 0) (.mul (.mul (.var 1) (.var 2)) (.var 3))) (.var 4))355    (.mul (.mul (.var 1) (.var 2)) (.mul (.mul (.var 0) (.var 3)) (.var 4))) (by decide +kernel)356357/-- `(u·h)·v` as a double sum. -/358theorem ctr_dot (η : Nat → Shell p) (n : Nat) (u v : Nat → Shell p) (h : Nat → Nat → Shell p) :359    dot η n (ctr η n u h) v = sumRange (fun ν => sumRange (fun μ => η μ * u μ * (η ν * h μ ν * v ν)) n) n :=360  sum_congr n (fun ν _ => by361    show η ν * sumRange (fun μ => η μ * u μ * h μ ν) n * v ν = _362    rw [← sum_mul_left, ← sum_mul_right]363    exact sum_congr n (fun μ _ => rows_pt _ _ _ _ _))364365/-- `(u·h)·v` row by row: `Σ_μ η_μ u_μ (h_μ · v)`. -/366theorem rows (η : Nat → Shell p) (n : Nat) (u v : Nat → Shell p) (h : Nat → Nat → Shell p) :367    sumRange (fun μ => η μ * u μ * dot η n (h μ) v) n = dot η n (ctr η n u h) v := by368  rw [ctr_dot, ← sum_swap]369  exact sum_congr n (fun μ _ => (sum_mul_left _ _ n).symm)370371theorem sym_pt (a u b h v : Shell p) : a * u * (b * h * v) = b * v * (a * h * u) :=372  RE.sound (look [a, u, b, h, v])373    (.mul (.mul (.var 0) (.var 1)) (.mul (.mul (.var 2) (.var 3)) (.var 4)))374    (.mul (.mul (.var 2) (.var 4)) (.mul (.mul (.var 0) (.var 3)) (.var 1))) (by decide +kernel)375376/-- For a symmetric `h`, `(u·h)·v = (v·h)·u`. -/377theorem ctr_symm (η : Nat → Shell p) (n : Nat) (u v : Nat → Shell p) {h : Nat → Nat → Shell p}378    (hs : ∀ μ ν, h μ ν = h ν μ) : dot η n (ctr η n u h) v = dot η n (ctr η n v h) u := by379  rw [ctr_dot η n u v h, ctr_dot η n v u h, sum_swap]380  exact sum_congr n (fun a _ => sum_congr n (fun b _ => by rw [hs a b]; exact sym_pt _ _ _ _ _))381382theorem row_pt (h a x b c : Shell p) : h + (a * x + b * c) = h + a * x + c * b :=383  RE.sound (look [h, a, x, b, c])384    (.add (.var 0) (.add (.mul (.var 1) (.var 2)) (.mul (.var 3) (.var 4))))385    (.add (.add (.var 0) (.mul (.var 1) (.var 2))) (.mul (.var 4) (.var 3))) (by decide +kernel)386387theorem pair_pt (e P X K a b B C Y : Shell p) :388    e * (P + X * (a * a) + K * (b * b) + B * ((1 + 1) * a) + C * ((1 + 1) * b) + Y * ((1 + 1) * a * b)) =389      e * P + e * a * a * X + e * b * b * K + e * a * B * (1 + 1) + e * b * C * (1 + 1) + e * a * b * ((1 + 1) * Y) :=390  RE.sound (look [e, P, X, K, a, b, B, C, Y])391    (.mul (.var 0) (.add (.add (.add (.add (.add (.var 1) (.mul (.var 2) (.mul (.var 4) (.var 4)))) (.mul (.var 3) (.mul (.var 5) (.var 5)))) (.mul (.var 6) (.mul (.add .one .one) (.var 4)))) (.mul (.var 7) (.mul (.add .one .one) (.var 5)))) (.mul (.var 8) (.mul (.mul (.add .one .one) (.var 4)) (.var 5)))))392    (.add (.add (.add (.add (.add (.mul (.var 0) (.var 1)) (.mul (.mul (.mul (.var 0) (.var 4)) (.var 4)) (.var 2))) (.mul (.mul (.mul (.var 0) (.var 5)) (.var 5)) (.var 3))) (.mul (.mul (.mul (.var 0) (.var 4)) (.var 6)) (.add .one .one))) (.mul (.mul (.mul (.var 0) (.var 5)) (.var 7)) (.add .one .one))) (.mul (.mul (.mul (.var 0) (.var 4)) (.var 5)) (.mul (.add .one .one) (.var 8)))) (by decide +kernel)393394theorem pair_gauge (η : Nat → Shell p) (n : Nat) (k ξ : Nat → Shell p) {h : Nat → Nat → Shell p}395    (hs : ∀ μ ν, h μ ν = h ν μ) :396    pair η n (gauge h k ξ) (gauge h k ξ) = pair η n h h + dot η n k k * dot η n ξ ξ + dot η n ξ ξ * dot η n k k +397      dot η n (ctr η n k h) ξ * (1 + 1) + dot η n (ctr η n k h) ξ * (1 + 1) + dot η n k ξ * ((1 + 1) * dot η n k ξ) := by398  have row : ∀ μ, dot η n (gauge h k ξ μ) (gauge h k ξ μ) = dot η n (h μ) (h μ) + dot η n ξ ξ * (k μ * k μ) +399      dot η n k k * (ξ μ * ξ μ) + dot η n (h μ) ξ * ((1 + 1) * k μ) + dot η n (h μ) k * ((1 + 1) * ξ μ) +400      dot η n ξ k * ((1 + 1) * k μ * ξ μ) := fun μ =>401    dot_quad3 η n (W := gauge h k ξ μ) (w := h μ) (u := ξ) (v := k) (c := k μ) (d := ξ μ)402      (fun ν => row_pt _ _ _ _ _)403  have e := sum_lin6 (fun μ => η μ * dot η n (h μ) (h μ)) (fun μ => η μ * k μ * k μ) (fun μ => η μ * ξ μ * ξ μ)404    (fun μ => η μ * k μ * dot η n (h μ) ξ) (fun μ => η μ * ξ μ * dot η n (h μ) k) (fun μ => η μ * k μ * ξ μ)405    (dot η n ξ ξ) (dot η n k k) (1 + 1) (1 + 1) ((1 + 1) * dot η n ξ k) n406  rw [rows η n k ξ h, rows η n ξ k h, ctr_symm η n ξ k hs, dot_comm η n ξ k] at e407  exact (sum_congr n (fun μ _ => by rw [row μ, dot_comm η n ξ k]; exact pair_pt _ _ _ _ _ _ _ _ _)).trans e408409theorem tens_ring (a₁ a₂ a₃ a₄ K P X B Y D C T : Shell p) :410    a₁ * (K * (P + K * X + X * K + B * (1 + 1) + B * (1 + 1) + Y * ((1 + 1) * Y))) +411        a₂ * (D + X * (K * K) + K * (Y * Y) + B * ((1 + 1) * K) + C * ((1 + 1) * Y) + Y * ((1 + 1) * K * Y)) +412        a₃ * ((C + Y * K + K * Y) * (T + Y * (1 + 1))) + a₄ * (K * ((T + Y * (1 + 1)) * (T + Y * (1 + 1)))) =413      a₁ * (K * P) + a₂ * D + a₃ * (C * T) + a₄ * (K * (T * T)) +414        ((1 + 1) * a₁ + a₂) * ((1 + 1) * K * B + K * K * X + K * (Y * Y)) +415        (a₂ + a₃) * ((1 + 1) * Y * C + (1 + 1) * K * (Y * Y)) +416        (a₃ + (1 + 1) * a₄) * ((1 + 1) * K * Y * T + (1 + 1) * K * (Y * Y)) :=417  RE.sound (look [a₁, a₂, a₃, a₄, K, P, X, B, Y, D, C, T])418    (.add (.add (.add (.mul (.var 0) (.mul (.var 4) (.add (.add (.add (.add (.add (.var 5) (.mul (.var 4) (.var 6))) (.mul (.var 6) (.var 4))) (.mul (.var 7) (.add .one .one))) (.mul (.var 7) (.add .one .one))) (.mul (.var 8) (.mul (.add .one .one) (.var 8)))))) (.mul (.var 1) (.add (.add (.add (.add (.add (.var 9) (.mul (.var 6) (.mul (.var 4) (.var 4)))) (.mul (.var 4) (.mul (.var 8) (.var 8)))) (.mul (.var 7) (.mul (.add .one .one) (.var 4)))) (.mul (.var 10) (.mul (.add .one .one) (.var 8)))) (.mul (.var 8) (.mul (.mul (.add .one .one) (.var 4)) (.var 8)))))) (.mul (.var 2) (.mul (.add (.add (.var 10) (.mul (.var 8) (.var 4))) (.mul (.var 4) (.var 8))) (.add (.var 11) (.mul (.var 8) (.add .one .one)))))) (.mul (.var 3) (.mul (.var 4) (.mul (.add (.var 11) (.mul (.var 8) (.add .one .one))) (.add (.var 11) (.mul (.var 8) (.add .one .one)))))))419    (.add (.add (.add (.add (.add (.add (.mul (.var 0) (.mul (.var 4) (.var 5))) (.mul (.var 1) (.var 9))) (.mul (.var 2) (.mul (.var 10) (.var 11)))) (.mul (.var 3) (.mul (.var 4) (.mul (.var 11) (.var 11))))) (.mul (.add (.mul (.add .one .one) (.var 0)) (.var 1)) (.add (.add (.mul (.mul (.add .one .one) (.var 4)) (.var 7)) (.mul (.mul (.var 4) (.var 4)) (.var 6))) (.mul (.var 4) (.mul (.var 8) (.var 8)))))) (.mul (.add (.var 1) (.var 2)) (.add (.mul (.mul (.add .one .one) (.var 8)) (.var 10)) (.mul (.mul (.add .one .one) (.var 4)) (.mul (.var 8) (.var 8)))))) (.mul (.add (.var 2) (.mul (.add .one .one) (.var 3))) (.add (.mul (.mul (.mul (.add .one .one) (.var 4)) (.var 8)) (.var 11)) (.mul (.mul (.add .one .one) (.var 4)) (.mul (.var 8) (.var 8)))))) (by decide +kernel)420421/-- Spin 2, the gauge variation, on every shell, in every dimension and metric: for a symmetric `h`, the shift422`h ↦ h + kξ + ξk` changes the combination by `(2a₁ + a₂) X₁ + (a₂ + a₃) X₂ + (a₃ + 2a₄) X₃`, with423`X₁ = 2k² (k·h·ξ) + k⁴ ξ² + k² (k·ξ)²`, `X₂ = 2(k·ξ)(k·h·k) + 2k² (k·ξ)²` and `X₃ = 2k² (k·ξ) tr h + 2k² (k·ξ)²`. -/424theorem tens_shift (η : Nat → Shell p) (n : Nat) (a₁ a₂ a₃ a₄ : Shell p) (k ξ : Nat → Shell p)425    {h : Nat → Nat → Shell p} (hs : ∀ μ ν, h μ ν = h ν μ) :426    tensForm η n a₁ a₂ a₃ a₄ k (gauge h k ξ) = tensForm η n a₁ a₂ a₃ a₄ k h +427      ((1 + 1) * a₁ + a₂) * ((1 + 1) * dot η n k k * dot η n (ctr η n k h) ξ +428        dot η n k k * dot η n k k * dot η n ξ ξ + dot η n k k * (dot η n k ξ * dot η n k ξ)) +429      (a₂ + a₃) * ((1 + 1) * dot η n k ξ * dot η n (ctr η n k h) k +430        (1 + 1) * dot η n k k * (dot η n k ξ * dot η n k ξ)) +431      (a₃ + (1 + 1) * a₄) * ((1 + 1) * dot η n k k * dot η n k ξ * tr η n h +432        (1 + 1) * dot η n k k * (dot η n k ξ * dot η n k ξ)) := by433  have hc : ∀ ν, ctr η n k (gauge h k ξ) ν = ctr η n k h ν + dot η n k k * ξ ν + dot η n k ξ * k ν :=434    ctr_gauge η n k ξ h435  unfold tensForm436  rw [pair_gauge η n k ξ hs, dot_quad3 η n hc, dot_lin3 η n hc k, tr_gauge, dot_comm η n ξ k]437  exact tens_ring _ _ _ _ _ _ _ _ _ _ _ _438439theorem fp_ring (S X₁ X₂ X₃ c : Shell p) :440    S + ((1 + 1) * (-c) + (1 + 1) * c) * X₁ + ((1 + 1) * c + (-((1 + 1) * c))) * X₂ +441      ((-((1 + 1) * c)) + (1 + 1) * c) * X₃ = S :=442  RE.sound (look [S, X₁, X₂, X₃, c])443    (.add (.add (.add (.var 0) (.mul (.add (.mul (.add .one .one) (.neg (.var 4))) (.mul (.add .one .one) (.var 4))) (.var 1))) (.mul (.add (.mul (.add .one .one) (.var 4)) (.neg (.mul (.add .one .one) (.var 4)))) (.var 2))) (.mul (.add (.neg (.mul (.add .one .one) (.var 4))) (.mul (.add .one .one) (.var 4))) (.var 3)))444    (.var 0) (by decide +kernel)445446/-- 00:E1, 21:C9 — spin 2: the Fierz–Pauli line `(−1, 2, −2, 1)` is gauge invariant on every shell, at every symbol. -/447theorem fierz_pauli_invariant (η : Nat → Shell p) (n : Nat) (c : Shell p) (k ξ : Nat → Shell p)448    {h : Nat → Nat → Shell p} (hs : ∀ μ ν, h μ ν = h ν μ) :449    tensForm η n (-c) ((1 + 1) * c) (-((1 + 1) * c)) c k (gauge h k ξ) =450      tensForm η n (-c) ((1 + 1) * c) (-((1 + 1) * c)) c k h := by451  rw [tens_shift η n _ _ _ _ k ξ hs]452  exact fp_ring _ _ _ _ _453454/-! ## Spin 2: uniqueness of the Fierz–Pauli line -/455456/-- The zero field. -/457def zero2 : Nat → Nat → Shell p := fun _ _ => 0458459/-- The field `e₁ ⊗ e₁`. -/460def unit11 : Nat → Nat → Shell p := fun μ ν => basis 1 μ * basis 1 ν461462theorem var_ring (S A B C : Shell p) : A + B + C = S + A + B + C + -S :=463  RE.sound (look [S, A, B, C])464    (.add (.add (.var 1) (.var 2)) (.var 3))465    (.add (.add (.add (.add (.var 0) (.var 1)) (.var 2)) (.var 3)) (.neg (.var 0))) (by decide +kernel)466467theorem var_zero {S A B C : Shell p} (h : S + A + B + C = S) : A + B + C = 0 := by468  rw [var_ring S A B C, h, add_neg]469470theorem ctr_zero2 (η : Nat → Shell p) (n : Nat) (u v : Nat → Shell p) : dot η n (ctr η n u zero2) v = 0 :=471  dot_zero_left η n v (fun _ => sum_zero n (fun _ _ => mul_zero _))472473theorem tr_zero2 (η : Nat → Shell p) (n : Nat) : tr η n zero2 = 0 := sum_zero n (fun _ _ => mul_zero _)474475theorem u11_pt (e a b c : Shell p) : e * a * (b * c) = e * (a * b) * c :=476  RE.sound (look [e, a, b, c])477    (.mul (.mul (.var 0) (.var 1)) (.mul (.var 2) (.var 3)))478    (.mul (.mul (.var 0) (.mul (.var 1) (.var 2))) (.var 3)) (by decide +kernel)479480theorem ctr_unit11 (η : Nat → Shell p) (n : Nat) (v : Nat → Shell p) : dot η n (ctr η n (basis 0) unit11) v = 0 :=481  dot_zero_left η n v (fun ν => sum_zero n (fun μ _ => by482    show η μ * basis 0 μ * (basis 1 μ * basis 1 ν) = 0483    rw [u11_pt, basis_mul_ne (i := 0) (j := 1) (by decide) μ, mul_zero, zero_mul]))484485theorem tr_unit11 (η : Nat → Shell p) {n : Nat} (hn : 1 < n) : tr η n unit11 = η 1 :=486  (sum_congr n (fun _ _ => (mul_assoc _ _ _).symm)).trans (dot_basis_self η hn)487488theorem t1_ring (A B C e₀ e₁ : Shell p) :489    A * ((1 + 1) * e₀ * 0 + e₀ * e₀ * e₁ + e₀ * (0 * 0)) + B * ((1 + 1) * 0 * 0 + (1 + 1) * e₀ * (0 * 0)) +490      C * ((1 + 1) * e₀ * 0 * 0 + (1 + 1) * e₀ * (0 * 0)) = A * (e₀ * e₀ * e₁) :=491  RE.sound (look [A, B, C, e₀, e₁])492    (.add (.add (.mul (.var 0) (.add (.add (.mul (.mul (.add .one .one) (.var 3)) .zero) (.mul (.mul (.var 3) (.var 3)) (.var 4))) (.mul (.var 3) (.mul .zero .zero)))) (.mul (.var 1) (.add (.mul (.mul (.add .one .one) .zero) .zero) (.mul (.mul (.add .one .one) (.var 3)) (.mul .zero .zero))))) (.mul (.var 2) (.add (.mul (.mul (.mul (.add .one .one) (.var 3)) .zero) .zero) (.mul (.mul (.add .one .one) (.var 3)) (.mul .zero .zero)))))493    (.mul (.var 0) (.mul (.mul (.var 3) (.var 3)) (.var 4))) (by decide +kernel)494495theorem t2_ring (A B C e₀ : Shell p) :496    A * ((1 + 1) * e₀ * 0 + e₀ * e₀ * e₀ + e₀ * (e₀ * e₀)) + B * ((1 + 1) * e₀ * 0 + (1 + 1) * e₀ * (e₀ * e₀)) +497      C * ((1 + 1) * e₀ * e₀ * 0 + (1 + 1) * e₀ * (e₀ * e₀)) = (A + B + C) * ((1 + 1) * e₀ * e₀ * e₀) :=498  RE.sound (look [A, B, C, e₀])499    (.add (.add (.mul (.var 0) (.add (.add (.mul (.mul (.add .one .one) (.var 3)) .zero) (.mul (.mul (.var 3) (.var 3)) (.var 3))) (.mul (.var 3) (.mul (.var 3) (.var 3))))) (.mul (.var 1) (.add (.mul (.mul (.add .one .one) (.var 3)) .zero) (.mul (.mul (.add .one .one) (.var 3)) (.mul (.var 3) (.var 3)))))) (.mul (.var 2) (.add (.mul (.mul (.mul (.add .one .one) (.var 3)) (.var 3)) .zero) (.mul (.mul (.add .one .one) (.var 3)) (.mul (.var 3) (.var 3))))))500    (.mul (.add (.add (.var 0) (.var 1)) (.var 2)) (.mul (.mul (.mul (.add .one .one) (.var 3)) (.var 3)) (.var 3))) (by decide +kernel)501502theorem t3_ring (A B C e₀ e₁ : Shell p) :503    A * ((1 + 1) * e₀ * 0 + e₀ * e₀ * e₀ + e₀ * (e₀ * e₀)) + B * ((1 + 1) * e₀ * 0 + (1 + 1) * e₀ * (e₀ * e₀)) +504      C * ((1 + 1) * e₀ * e₀ * e₁ + (1 + 1) * e₀ * (e₀ * e₀)) =505    (A + B + C) * ((1 + 1) * e₀ * e₀ * e₀) + C * ((1 + 1) * e₀ * e₀ * e₁) :=506  RE.sound (look [A, B, C, e₀, e₁])507    (.add (.add (.mul (.var 0) (.add (.add (.mul (.mul (.add .one .one) (.var 3)) .zero) (.mul (.mul (.var 3) (.var 3)) (.var 3))) (.mul (.var 3) (.mul (.var 3) (.var 3))))) (.mul (.var 1) (.add (.mul (.mul (.add .one .one) (.var 3)) .zero) (.mul (.mul (.add .one .one) (.var 3)) (.mul (.var 3) (.var 3)))))) (.mul (.var 2) (.add (.mul (.mul (.mul (.add .one .one) (.var 3)) (.var 3)) (.var 4)) (.mul (.mul (.add .one .one) (.var 3)) (.mul (.var 3) (.var 3))))))508    (.add (.mul (.add (.add (.var 0) (.var 1)) (.var 2)) (.mul (.mul (.mul (.add .one .one) (.var 3)) (.var 3)) (.var 3))) (.mul (.var 2) (.mul (.mul (.mul (.add .one .one) (.var 3)) (.var 3)) (.var 4)))) (by decide +kernel)509510theorem line_a1 (a₁ a₂ a₃ a₄ t : Shell p) :511    a₁ + a₄ = 0 + (t * (1 + 1)) * ((1 + 1) * a₁ + a₂) +512      (-t) * ((1 + 1) * a₁ + a₂ + (a₂ + a₃) + (a₃ + (1 + 1) * a₄)) + (t * (1 + 1)) * (a₃ + (1 + 1) * a₄) +513      (-(a₁ + a₄)) * ((1 + 1) * t + -1) :=514  RE.sound (look [a₁, a₂, a₃, a₄, t])515    (.add (.var 0) (.var 3))516    (.add (.add (.add (.add .zero (.mul (.mul (.var 4) (.add .one .one)) (.add (.mul (.add .one .one) (.var 0)) (.var 1)))) (.mul (.neg (.var 4)) (.add (.add (.add (.mul (.add .one .one) (.var 0)) (.var 1)) (.add (.var 1) (.var 2))) (.add (.var 2) (.mul (.add .one .one) (.var 3)))))) (.mul (.mul (.var 4) (.add .one .one)) (.add (.var 2) (.mul (.add .one .one) (.var 3))))) (.mul (.neg (.add (.var 0) (.var 3))) (.add (.mul (.add .one .one) (.var 4)) (.neg .one)))) (by decide +kernel)517518theorem line_a2 (a₁ a₂ a₄ : Shell p) :519    a₂ = (1 + 1) * a₄ + 1 * ((1 + 1) * a₁ + a₂) + (-(1 + 1)) * (a₁ + a₄) :=520  RE.sound (look [a₁, a₂, a₄])521    (.var 1)522    (.add (.add (.mul (.add .one .one) (.var 2)) (.mul .one (.add (.mul (.add .one .one) (.var 0)) (.var 1)))) (.mul (.neg (.add .one .one)) (.add (.var 0) (.var 2)))) (by decide +kernel)523524/-- 00:E1, 00:E3, 21:C9 — spin 2 over all symbols: when `2` and the metric entries `η₀`, `η₁` are units (`n ≥ 2`), the525combinations gauge invariant at every symbol, for every symmetric field and every gauge vector, are exactly the526Fierz–Pauli line `(a₁, a₂, a₃, a₄) = c (−1, 2, −2, 1)`. -/527theorem fierz_pauli_unique (η : Nat → Shell p) {n : Nat} {w₀ w₁ t : Shell p} (hn : 1 < n) (h₀ : η 0 * w₀ = 1)528    (h₁ : η 1 * w₁ = 1) (h₂ : (1 + 1) * t = 1) (a₁ a₂ a₃ a₄ : Shell p) :529    (∀ (k ξ : Nat → Shell p) (h : Nat → Nat → Shell p), (∀ μ ν, h μ ν = h ν μ) →530        tensForm η n a₁ a₂ a₃ a₄ k (gauge h k ξ) = tensForm η n a₁ a₂ a₃ a₄ k h) ↔531      ∃ c : Shell p, a₁ = -c ∧ a₂ = (1 + 1) * c ∧ a₃ = -((1 + 1) * c) ∧ a₄ = c := by532  constructor533  · intro hinv534    have v := fun (k ξ : Nat → Shell p) (h : Nat → Nat → Shell p) (hs : ∀ μ ν, h μ ν = h ν μ) =>535      var_zero ((tens_shift η n a₁ a₂ a₃ a₄ k ξ hs).symm.trans (hinv k ξ h hs))536    have hn0 : 0 < n := Nat.lt_trans (Nat.zero_lt_succ 0) hn537    have v1 := v (basis 0) (basis 1) zero2 (fun _ _ => rfl)538    rw [dot_basis_self η hn0, dot_basis_self η hn, dot_basis_ne η n (i := 0) (j := 1) (by decide), ctr_zero2,539      ctr_zero2, tr_zero2] at v1540    have c₁ := cancel3 ((t1_ring _ _ _ _ _).symm.trans v1) h₀ h₀ h₁541    have v2 := v (basis 0) (basis 0) zero2 (fun _ _ => rfl)542    rw [dot_basis_self η hn0, ctr_zero2, tr_zero2] at v2543    have s := cancel4 ((t2_ring _ _ _ _).symm.trans v2) h₂ h₀ h₀ h₀544    have v3 := v (basis 0) (basis 0) unit11 (fun μ ν => mul_comm _ _)545    rw [dot_basis_self η hn0, ctr_unit11, tr_unit11 η hn] at v3546    have v3' := (t3_ring _ _ _ _ _).symm.trans v3547    rw [s, zero_mul, zero_add] at v3'548    have c₃ := cancel4 v3' h₂ h₀ h₀ h₁549    have h14 : a₁ + a₄ = 0 := lc4 (line_a1 a₁ a₂ a₃ a₄ t) c₁ s c₃ (sub_one_zero h₂)550    exact ⟨a₄, eq_neg_of_add_eq_zero h14, lc2 (line_a2 a₁ a₂ a₄) c₁ h14, eq_neg_of_add_eq_zero c₃, rfl⟩551  · intro ⟨c, e₁, e₂, e₃, e₄⟩ k ξ h hs552    rw [e₁, e₂, e₃, e₄]553    exact fierz_pauli_invariant η n c k ξ hs554555/-- The hypothesis on `2` cannot be dropped: on the shell of two residues, `k² ⟨h, h⟩` alone is gauge invariant, and556it is not on the Fierz–Pauli line. -/557theorem char_two_not_unique (η : Nat → Shell 2) (n : Nat) :558    (∀ (k ξ : Nat → Shell 2) (h : Nat → Nat → Shell 2), (∀ μ ν, h μ ν = h ν μ) →559        tensForm η n 1 0 0 0 k (gauge h k ξ) = tensForm η n 1 0 0 0 k h) ∧560      ¬ ∃ c : Shell 2, (1 : Shell 2) = -c ∧ (0 : Shell 2) = (1 + 1) * c ∧ (0 : Shell 2) = -((1 + 1) * c) ∧561        (0 : Shell 2) = c := by562  constructor563  · intro k ξ h hs564    rw [tens_shift η n 1 0 0 0 k ξ hs]565    have e₁ : (1 + 1) * (1 : Shell 2) + 0 = 0 := by decide566    have e₂ : (0 : Shell 2) + 0 = 0 := by decide567    have e₃ : (0 : Shell 2) + (1 + 1) * 0 = 0 := by decide568    rw [e₁, e₂, e₃, zero_mul, zero_mul, zero_mul, add_zero, add_zero, add_zero]569  · intro ⟨c, e₁, _, _, e₄⟩570    rw [← e₄] at e₁571    exact absurd e₁ (by decide)572573end FRC.Symbol574