Time contractions

noncomputable def WickContraction.staticContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : ↥(Subalgebra.center ℂ 𝓕.FieldOpAlgebra)

For a list φs of 𝓕.FieldOp and a Wick contraction φsΛ, the element of the center of 𝓕.FieldOpAlgebra, φsΛ.staticContract is defined as the product of [anPart φs[j], φs[k]]ₛ over contracted pairs {j, k} in φsΛ with j < k.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WickContraction.staticContract_insert_none {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : (insertAndContract φ φsΛ i none).staticContract = φsΛ.staticContract

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a i ≤ φs.length, then the following relation holds:

(φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract

The proof of this result ultimately is a consequence of definitions.

theorem WickContraction.staticContract_insert_some {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : (insertAndContract φ φsΛ i (some j)).staticContract = (if i < i.succAbove ↑j then ⟨(FieldSpecification.FieldOpAlgebra.superCommute (FieldSpecification.FieldOpAlgebra.anPart φ)) (FieldSpecification.FieldOpAlgebra.ofFieldOp φs[↑j]), ⋯⟩ else ⟨(FieldSpecification.FieldOpAlgebra.superCommute (FieldSpecification.FieldOpAlgebra.anPart φs[↑j])) (FieldSpecification.FieldOpAlgebra.ofFieldOp φ), ⋯⟩) * φsΛ.staticContract

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted, then (φsΛ ↩Λ φ i (some k)).staticContract is equal to the product of

• [anPart φ, φs[k]]ₛ if i ≤ k or [anPart φs[k], φ]ₛ if k < i
• φsΛ.staticContract.

The proof of this result ultimately is a consequence of definitions.

theorem WickContraction.staticContract_insert_some_of_lt {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hik : i < i.succAbove ↑k) : ↑(insertAndContract φ φsΛ i (some k)).staticContract = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => x < ↑k) φsΛ.uncontracted)) • (FieldSpecification.FieldOpAlgebra.contractStateAtIndex φ φsΛ.uncontractedListGet ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.staticContract)

theorem WickContraction.staticContract_of_not_gradingCompliant {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (h : ¬GradingCompliant φs φsΛ) : φsΛ.staticContract = 0