feat: Finish proof of anti-symm symm tensor contract

HepLean/Tensors/ComplexLorentz/Lemmas.lean

@@ -73,36 +73,37 @@ lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ :
     | (1 : Fin 2) => rfl
 
 set_option maxRecDepth 20000 in
+/-- Contracting a rank-2 anti-symmetric tensor with a rank-2 symmetric tensor gives zero. -/
 lemma symm_contract_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V)
     (S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V)
-    (hA : (twoNodeE complexLorentzTensor Color.up Color.up A).tensor =
-      (TensorTree.neg (perm
-      (OverColor.equivToHomEq (Equality.finMapToEquiv ![1, 0] ![1, 0]) (by decide))
-      (twoNodeE complexLorentzTensor Color.up Color.up A))).tensor)
-    (hs : {S | μ ν = S | ν μ}ᵀ) : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = 0 := by
-  have h1 : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = - {A | μ ν ⊗ S | μ ν}ᵀ.tensor := by
-    nth_rewrite 1 [contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_fst hA))]
-    nth_rewrite 1 [(contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_snd hs)))]
-    rw [contr_tensor_eq (contr_tensor_eq (neg_fst_prod _ _))]
-    rw [contr_tensor_eq (neg_contr _)]
-    rw [neg_contr]
-    rw [neg_tensor]
-    apply congrArg
-    rw [contr_tensor_eq (contr_tensor_eq (prod_perm_left _ _ _ _))]
-    rw [contr_tensor_eq (perm_contr _ _)]
-    rw [perm_contr]
-    rw [perm_tensor_eq (contr_tensor_eq (contr_tensor_eq (prod_perm_right _ _ _ _)))]
-    rw [perm_tensor_eq (contr_tensor_eq (perm_contr _ _))]
-    rw [perm_tensor_eq (perm_contr _  _)]
-    rw [perm_perm]
-    nth_rewrite 1 [perm_tensor_eq (contr_contr _ _ _)]
-    rw [perm_perm]
-    rw [perm_eq_id]
-    · rfl
-    · apply OverColor.Hom.ext
-      rfl
-
-
+    (hA : {A | μ ν = - (A | ν μ)}ᵀ) (hs : {S | μ ν = S | ν μ}ᵀ) :
+    {A | μ ν ⊗ S | μ ν}ᵀ.tensor = 0 := by
+  have hn {M : Type} [AddCommGroup M] [Module ℂ M] {x : M} (h : x = - x) : x = 0 := by
+    rw [eq_neg_iff_add_eq_zero, ← two_smul ℂ x] at h
+    simpa using h
+  refine hn ?_
+  rw [← neg_tensor]
+  rw [neg_perm] at hA
+  nth_rewrite 1 [contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_fst hA))]
+  nth_rewrite 1 [(contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_snd hs)))]
+  rw [contr_tensor_eq (contr_tensor_eq (neg_fst_prod _ _))]
+  rw [contr_tensor_eq (neg_contr _)]
+  rw [neg_contr]
+  rw [neg_tensor]
+  apply congrArg
+  rw [contr_tensor_eq (contr_tensor_eq (prod_perm_left _ _ _ _))]
+  rw [contr_tensor_eq (perm_contr _ _)]
+  rw [perm_contr]
+  rw [perm_tensor_eq (contr_tensor_eq (contr_tensor_eq (prod_perm_right _ _ _ _)))]
+  rw [perm_tensor_eq (contr_tensor_eq (perm_contr _ _))]
+  rw [perm_tensor_eq (perm_contr _  _)]
+  rw [perm_perm]
+  nth_rewrite 1 [perm_tensor_eq (contr_contr _ _ _)]
+  rw [perm_perm]
+  rw [perm_eq_id]
+  · rfl
+  · apply OverColor.Hom.ext
+    rfl
 
 end Fermion
 

HepLean/Tensors/Tree/Elab.lean

@@ -108,6 +108,9 @@ syntax "(" tensorExpr ")" : tensorExpr
 /-- Scalar multiplication for tensors. -/
 syntax term "•" tensorExpr : tensorExpr
 
+/-- Negation of a tensor tree. -/
+syntax "-" tensorExpr : tensorExpr
+
 /-- Equality. -/
 syntax tensorExpr "=" tensorExpr : tensorExpr
 
@@ -372,6 +375,15 @@ partial def syntaxFull (stx : Syntax) : TermElabM Term := do
 
 end ProdNode
 
+namespace negNode
+
+/-- The syntax associated with a product of tensors. -/
+def negSyntax (T1 : Term) : Term :=
+  Syntax.mkApp (mkIdent ``TensorTree.neg) #[T1]
+
+end negNode
+
+
 /-- Returns the full list of indices after contraction. TODO: Include evaluation. -/
 partial def getIndicesFull (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
   match stx with
@@ -381,6 +393,8 @@ partial def getIndicesFull (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)
       return (← ProdNode.withoutContr stx)
   | `(tensorExpr| ($a:tensorExpr)) => do
       return (← getIndicesFull a)
+  | `(tensorExpr| -$a:tensorExpr) => do
+      return (← getIndicesFull a)
   | _ =>
     throwError "Unsupported tensor expression syntax in getIndicesProd: {stx}"
 
@@ -448,10 +462,13 @@ def equalSyntax (permSyntax : Term) (T1 T2 : Term) : TermElabM Term := do
 /-- Creates the syntax associated with a tensor node. -/
 partial def syntaxFull (stx : Syntax) : TermElabM Term := do
   match stx with
-  | `(tensorExpr| $_:term | $[$args]*) => ProdNode.syntaxFull stx
+  | `(tensorExpr| $_:term | $[$args]*) =>
+    ProdNode.syntaxFull stx
   | `(tensorExpr| $_:tensorExpr ⊗ $_:tensorExpr) => ProdNode.syntaxFull stx
   | `(tensorExpr| ($a:tensorExpr)) => do
       return (← syntaxFull a)
+  | `(tensorExpr| -$a:tensorExpr) => do
+      return negNode.negSyntax (← syntaxFull a)
   | `(tensorExpr| $a:tensorExpr = $b:tensorExpr) => do
       let indicesLeft ← getIndicesLeft stx
       let indicesRight ← getIndicesRight stx

HepLean/Tensors/Tree/NodeIdentities/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.Tree.Basic
+import LLMLean
 /-!
 
 ## Basic node identities