Merge pull request #269 from HEPLean/WickContract

refactor: Move contractions

HepLean.lean

@@ -114,12 +114,13 @@ import HepLean.Meta.Notes.HTMLNote
 import HepLean.Meta.Notes.NoteFile
 import HepLean.Meta.Notes.ToHTML
 import HepLean.Meta.TransverseTactics
+import HepLean.PerturbationTheory.Contractions.Basic
+import HepLean.PerturbationTheory.Contractions.Involutions
 import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
 import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
 import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.Phi4
 import HepLean.PerturbationTheory.FeynmanDiagrams.Momentum
 import HepLean.PerturbationTheory.FieldStatistics
-import HepLean.PerturbationTheory.Wick.Contractions
 import HepLean.PerturbationTheory.Wick.CreateAnnihilateSection
 import HepLean.PerturbationTheory.Wick.KoszulOrder
 import HepLean.PerturbationTheory.Wick.OfList

HepLean/PerturbationTheory/Wick/Contractions.lean → HepLean/PerturbationTheory/Contractions/Basic.lean

@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 import HepLean.PerturbationTheory.Wick.OperatorMap
 /-!
 
-# Koszul signs and ordering for lists and algebras
+# Contractions of a list of fields
 
 -/
 
@@ -40,6 +40,8 @@ lemma contractions_nil (a : Contractions ([] : List 𝓕)) : a = ⟨[], Contract
   cases c
   rfl
 
+/-- Establishes uniqueness of contractions for a single field, showing that any contraction
+  of a single field must be equivalent to the trivial contraction with no pairing. -/
 lemma contractions_single {i : 𝓕} (a : Contractions [i]) : a =
     ⟨[i], ContractionsAux.cons none ContractionsAux.nil⟩ := by
   cases a
@@ -52,7 +54,10 @@ lemma contractions_single {i : 𝓕} (a : Contractions [i]) : a =
   rename_i x
   exact Fin.elim0 x
 
-/-- For the nil list of fields there is only one contraction. -/
+/--
+  This function provides an equivalence between the type of contractions for an empty list of fields
+  and the unit type, indicating that there is only one possible contraction for an empty list.
+-/
 def nilEquiv : Contractions ([] : List 𝓕) ≃ Unit where
   toFun _ := ()
   invFun _ := ⟨[], ContractionsAux.nil⟩
@@ -105,6 +110,16 @@ instance fintype : (l : List 𝓕) → Fintype (Contractions l)
       Sigma.instFintype
     Fintype.ofEquiv _ consEquiv.symm
 
+/-- A contraction is a full contraction if there normalizing list of fields is empty. -/
+def IsFull : Prop := c.normalize = []
+
+/-- Provides a decidable instance for determining if a contraction is full
+  (i.e., all fields are paired). -/
+instance isFull_decidable : Decidable c.IsFull := by
+  have hn : c.IsFull ↔ c.normalize.length = 0 := by
+    simp [IsFull]
+  apply decidable_of_decidable_of_iff hn.symm
+
 /-- A structure specifying when a type `I` and a map `f :I → Type` corresponds to
   the splitting of a fields `φ` into a creation `n` and annihlation part `p`. -/
 structure Splitting (f : 𝓕 → Type) [∀ i, Fintype (f i)]
@@ -137,6 +152,11 @@ noncomputable def toCenterTerm (f : 𝓕 → Type) [∀ i, Fintype (f i)]
     superCommuteCoef q [aux'.get n] (List.take (↑n) aux') •
       F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a))) (ofListLift f [aux'.get n] 1))
 
+/-- Shows that adding a field with no contractions (none) to an existing set of contractions
+  results in the same center term as the original contractions.
+
+  Physically, this represents that an uncontracted (free) field does not affect
+  the contraction structure of other fields in Wick's theorem. -/
 lemma toCenterTerm_none (f : 𝓕 → Type) [∀ i, Fintype (f i)]
     (q : 𝓕 → FieldStatistic) {r : List 𝓕}
     (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
@@ -150,6 +170,8 @@ lemma toCenterTerm_none (f : 𝓕 → Type) [∀ i, Fintype (f i)]
   dsimp [toCenterTerm]
   rfl
 
+/-- Proves that the part of the term gained from Wick contractions is in
+  the center of the algebra. -/
 lemma toCenterTerm_center (f : 𝓕 → Type) [∀ i, Fintype (f i)]
     (q : 𝓕 → FieldStatistic)
     (le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]

HepLean/PerturbationTheory/Contractions/Involutions.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.Contractions.Basic
+import HepLean.Meta.Informal.Basic
+/-!
+
+# Involutions
+
+There is an isomorphism between the type of contractions of a list `l` and
+the type of involutions from `Fin l.length` to `Fin l.length`.
+
+Likewise, there is an isomorphism from the type of full contractions of a list `l`
+and the type of fixed-point free involutions from `Fin l.length` to `Fin l.length`.
+
+Given this, the number of full contractions of a list `l` is
+is given by the OEIS sequence A000085.
+
+-/
+
+namespace Wick
+
+open HepLean.List
+open FieldStatistic
+
+variable {𝓕 : Type}
+namespace Contractions
+
+variable {l : List 𝓕}
+
+informal_definition equivInvolution where
+  math :≈ "There is an isomorphism between the type of contractions of a list `l` and
+    the type of involutions from `Fin l.length` to `Fin l.length."
+
+informal_definition equivFullInvolution where
+  math :≈ "There is an isomorphism from the type of full contractions of a list `l`
+    and the type of fixed-point free involutions from `Fin l.length` to `Fin l.length."
+
+end Contractions
+
+end Wick

HepLean/PerturbationTheory/Wick/CreateAnnihilateSection.lean

@@ -203,9 +203,7 @@ lemma eraseIdx_succ_head {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
     RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply, Equiv.prodCongr_apply,
     Equiv.coe_refl, Prod.map_snd]
   conv_lhs =>
-    rhs
-    rhs
-    rhs
+    enter [1, 2, 1]
     erw [Fin.insertNthEquiv_symm_apply]
   simp only [head, Equiv.piCongr, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.piCongrRight,
     Equiv.cast_symm, Equiv.piCongrLeft, OrderIso.toEquiv_symm, OrderIso.symm_symm,
@@ -229,9 +227,7 @@ lemma eraseIdx_succ_tail {i : 𝓕} (n : ℕ) (hn : n + 1 < (i :: l).length)
     List.getElem_cons_succ, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply,
     Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd, Nat.succ_eq_add_one]
   conv_lhs =>
-    rhs
-    rhs
-    rhs
+    enter [1, 2, 1]
     erw [Fin.insertNthEquiv_symm_apply]
   rw [eraseIdx]
   conv_rhs =>

HepLean/PerturbationTheory/Wick/OperatorMap.lean

@@ -9,7 +9,6 @@ import HepLean.PerturbationTheory.Wick.SuperCommute
 # Operator map
 
 -/
-
 namespace Wick
 
 noncomputable section

HepLean/PerturbationTheory/Wick/StaticTheorem.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.PerturbationTheory.Wick.Contractions
+import HepLean.PerturbationTheory.Contractions.Basic
 /-!
 
 # Static Wick's theorem