Physlib.QFT.PerturbationTheory.WickAlgebra.TimeContraction

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas
public import Physlib.QFT.PerturbationTheory.WickAlgebra.TimeOrder

Time contractions

We define the state algebra of a field structure to be the free algebra generated by the states.

@[expose] public section

For a field specification 𝓕, and φ and ψ elements of 𝓕.FieldOp, the element of 𝓕.WickAlgebra, timeContract φ ψ is defined to be 𝓣(φψ) - 𝓝(φψ).

def timeContract (φ ψ : 𝓕.FieldOp) : 𝓕.WickAlgebra :=
    𝓣(ofFieldOp φ * ofFieldOp ψ) - 𝓝(ofFieldOp φ * ofFieldOp ψ)

lemma timeContract_eq_smul (φ ψ : 𝓕.FieldOp) : timeContract φ ψ =
    𝓣(ofFieldOp φ * ofFieldOp ψ) + (-1 : ℂ) • 𝓝(ofFieldOp φ * ofFieldOp ψ) := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOp⊢ timeContract φ ψ = timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • normalOrder (ofFieldOp φ * ofFieldOp ψ) rflAll goals completed! 🐙

For a field specification 𝓕, and φ and ψ elements of 𝓕.FieldOp, if φ and ψ are time-ordered then

timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ.


lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.FieldOp) (h : timeOrderRel φ ψ) :
    timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeContract φ ψ = (superCommute (anPart φ)) (ofFieldOp ψ)
  conv_rhs =>
    rw [ofFieldOp_eq_crPart_add_anPart]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ| (superCommute (anPart φ)) (crPart ψ + anPart ψ)
    rw [map_add, superCommute_anPart_anPart, superCommute_anPart_crPart]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ| anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • crPart ψ * anPart φ + 0
  simp only [timeContract, Algebra.smul_mul_assoc, add_zero]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrder (ofFieldOp φ * ofFieldOp ψ) - normalOrder (ofFieldOp φ * ofFieldOp ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)
  rw [timeOrder_ofFieldOp_ofFieldOp_ordered h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ ofFieldOp φ * ofFieldOp ψ - normalOrder (ofFieldOp φ * ofFieldOp ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ ofFieldOp φ * ofFieldOp ψ - normalOrder (ofFieldOp φ * ofFieldOp ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ ofFieldOp φ * ofFieldOp ψ - normalOrder (ofFieldOp φ * ofFieldOp ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)
  rw [normalOrder_ofFieldOp_mul_ofFieldOp𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ ofFieldOp φ * ofFieldOp ψ -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ ofFieldOp φ * ofFieldOp ψ -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ ofFieldOp φ * ofFieldOp ψ -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)
  rw [ofFieldOp_eq_crPart_add_anPart,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (crPart φ + anPart φ) * ofFieldOp ψ -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (crPart φ + anPart φ) * (crPart ψ + anPart ψ) -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) ofFieldOp_eq_crPart_add_anPart𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (crPart φ + anPart φ) * (crPart ψ + anPart ψ) -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (crPart φ + anPart φ) * (crPart ψ + anPart ψ) -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (crPart φ + anPart φ) * (crPart ψ + anPart ψ) -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)
  simp only [mul_add, add_mul]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ crPart φ * crPart ψ + anPart φ * crPart ψ + (crPart φ * anPart ψ + anPart φ * anPart ψ) -
    (crPart φ * crPart ψ + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ) + crPart φ * anPart ψ +
      anPart φ * anPart ψ) =
  anPart φ * crPart ψ - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (crPart ψ * anPart φ)
  abel_nfAll goals completed! 🐙



lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.FieldOp) (h : ¬ timeOrderRel φ ψ) :
    timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • timeContract ψ φ := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeContract φ ψ = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ
  rw [timeContract_eq_smul𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • normalOrder (ofFieldOp φ * ofFieldOp ψ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • normalOrder (ofFieldOp φ * ofFieldOp ψ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • normalOrder (ofFieldOp φ * ofFieldOp ψ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ
  rw [normalOrder_ofFieldOp_ofFieldOp_swap𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ
  rw [timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ
  rw [timeContract_eq_smul𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) •
    (timeOrder (ofFieldOp ψ * ofFieldOp φ) + -1 • normalOrder (ofFieldOp ψ * ofFieldOp φ))𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) •
    (timeOrder (ofFieldOp ψ * ofFieldOp φ) + -1 • normalOrder (ofFieldOp ψ * ofFieldOp φ))]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) •
    (timeOrder (ofFieldOp ψ * ofFieldOp φ) + -1 • normalOrder (ofFieldOp ψ * ofFieldOp φ))
  simp only [smul_add]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    -1 • (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • -1 • normalOrder (ofFieldOp ψ * ofFieldOp φ)
  rw [smul_smul,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    (-1 * (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ)) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • -1 • normalOrder (ofFieldOp ψ * ofFieldOp φ)All goals completed! 🐙 smul_smul,𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    (-1 * (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ)) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) * -1) • normalOrder (ofFieldOp ψ * ofFieldOp φ)All goals completed! 🐙 mul_comm𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) * -1) • normalOrder (ofFieldOp ψ * ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ofFieldOp ψ * ofFieldOp φ) +
    ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) * -1) • normalOrder (ofFieldOp ψ * ofFieldOp φ)All goals completed! 🐙]All goals completed! 🐙

For a field specification 𝓕, and φ and ψ elements of 𝓕.FieldOp, if φ and ψ are not time-ordered then

timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ.


lemma timeContract_of_not_timeOrderRel_expand (φ ψ : 𝓕.FieldOp) (h : ¬ timeOrderRel φ ψ) :
    timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeContract φ ψ = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)
  rw [timeContract_of_not_timeOrderRel _ _ h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)
  rw [timeContract_of_timeOrderRel _ _ _𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
  have h1 := Std.Total.total (r := 𝓕.timeOrderRel) φ ψ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel φ ψ ∨ timeOrderRel ψ φ⊢ timeOrderRel ψ φ
  simp_allAll goals completed! 🐙



lemma timeContract_eq_superCommute (φ ψ : 𝓕.FieldOp) :
    timeContract φ ψ = if timeOrderRel φ ψ then [anPart φ, ofFieldOp ψ]ₛ
    else 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOp⊢ timeContract φ ψ =
  if timeOrderRel φ ψ then (superCommute (anPart φ)) (ofFieldOp ψ)
  else (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)
  split_ifspos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph✝:timeOrderRel φ ψ⊢ timeContract φ ψ = (superCommute (anPart φ)) (ofFieldOp ψ)neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph✝:¬timeOrderRel φ ψ⊢ timeContract φ ψ = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)
  ·pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph✝:timeOrderRel φ ψ⊢ timeContract φ ψ = (superCommute (anPart φ)) (ofFieldOp ψ) rename_i hpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeContract φ ψ = (superCommute (anPart φ)) (ofFieldOp ψ)
    rw [timeContract_of_timeOrderRel _ _ hpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) = (superCommute (anPart φ)) (ofFieldOp ψ)All goals completed! 🐙]All goals completed! 🐙
  ·neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph✝:¬timeOrderRel φ ψ⊢ timeContract φ ψ = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ) rename_i hneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeContract φ ψ = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)
    rw [timeContract_of_not_timeOrderRel_expand _ _ hneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)All goals completed! 🐙]All goals completed! 🐙

For a field specification 𝓕, and φ and ψ elements of 𝓕.FieldOp, then timeContract φ ψ is in the center of 𝓕.WickAlgebra.


lemma timeContract_mem_center (φ ψ : 𝓕.FieldOp) :
    timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOp⊢ timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
  by_cases h : timeOrderRel φ ψpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebraneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
  ·pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra rw [timeContract_of_timeOrderRel _ _ hpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) ∈ Subalgebra.center ℂ 𝓕.WickAlgebrapos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) ∈ Subalgebra.center ℂ 𝓕.WickAlgebra]pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
    exact superCommute_anPart_ofFieldOp_mem_center φ ψAll goals completed! 🐙
  ·neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra rw [timeContract_of_not_timeOrderRel _ _ hneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ ∈ Subalgebra.center ℂ 𝓕.WickAlgebraneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
    refine Subalgebra.smul_mem (Subalgebra.center ℂ _) ?_ 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ)neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeContract ψ φ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra
    rw [timeContract_of_timeOrderRelneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (superCommute (anPart ψ)) (ofFieldOp φ) ∈ Subalgebra.center ℂ 𝓕.WickAlgebraneg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (superCommute (anPart ψ)) (ofFieldOp φ) ∈ Subalgebra.center ℂ 𝓕.WickAlgebraneg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (superCommute (anPart ψ)) (ofFieldOp φ) ∈ Subalgebra.center ℂ 𝓕.WickAlgebraneg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
    exact superCommute_anPart_ofFieldOp_mem_center _ _neg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
    have h1 := Std.Total.total (r := 𝓕.timeOrderRel) φ ψneg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel φ ψ ∨ timeOrderRel ψ φ⊢ timeOrderRel ψ φ
    simp_allAll goals completed! 🐙

              

lemma timeContract_zero_of_diff_grade (φ ψ : 𝓕.FieldOp) (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) :
    timeContract φ ψ = 0 := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψ⊢ timeContract φ ψ = 0
  by_cases h1 : timeOrderRel φ ψpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ timeContract φ ψ = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeContract φ ψ = 0
  ·pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ timeContract φ ψ = 0 rw [timeContract_of_timeOrderRel _ _ h1pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) = 0pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) = 0]pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ (superCommute (anPart φ)) (ofFieldOp ψ) = 0
    rw [superCommute_anPart_ofFieldOpF_diff_grade_zeropos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ 0 = 0pos.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ (𝓕|>ₛφ) ≠ 𝓕|>ₛψpos.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ (𝓕|>ₛφ) ≠ 𝓕|>ₛψ]pos.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:timeOrderRel φ ψ⊢ (𝓕|>ₛφ) ≠ 𝓕|>ₛψ
    exact hAll goals completed! 🐙
  ·neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeContract φ ψ = 0 rw [timeContract_of_not_timeOrderRel _ _ h1neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ = 0]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ = 0
    rw [timeContract_of_timeOrderRel _ _ _neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
    rw [superCommute_anPart_ofFieldOpF_diff_grade_zeroneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • 0 = 0neg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (𝓕|>ₛψ) ≠ 𝓕|>ₛφ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • 0 = 0neg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (𝓕|>ₛψ) ≠ 𝓕|>ₛφ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • 0 = 0neg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (𝓕|>ₛψ) ≠ 𝓕|>ₛφ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
    simp only [smul_zero]neg.h𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ (𝓕|>ₛψ) ≠ 𝓕|>ₛφ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
    exact h.symm𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψ⊢ timeOrderRel ψ φ
    have ht := Std.Total.total (r := 𝓕.timeOrderRel) φ ψ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:(𝓕|>ₛφ) ≠ 𝓕|>ₛψh1:¬timeOrderRel φ ψht:timeOrderRel φ ψ ∨ timeOrderRel ψ φ⊢ timeOrderRel ψ φ
    simp_allAll goals completed! 🐙

lemma normalOrder_timeContract (φ ψ : 𝓕.FieldOp) :
    𝓝(timeContract φ ψ) = 0 := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOp⊢ normalOrder (timeContract φ ψ) = 0
  by_cases h : timeOrderRel φ ψpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ normalOrder (timeContract φ ψ) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ normalOrder (timeContract φ ψ) = 0
  ·pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ normalOrder (timeContract φ ψ) = 0 rw [timeContract_of_timeOrderRel _ _ hpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ normalOrder ((superCommute (anPart φ)) (ofFieldOp ψ)) = 0pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ normalOrder ((superCommute (anPart φ)) (ofFieldOp ψ)) = 0]pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ normalOrder ((superCommute (anPart φ)) (ofFieldOp ψ)) = 0
    simpAll goals completed! 🐙
  ·neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ normalOrder (timeContract φ ψ) = 0 rw [timeContract_of_not_timeOrderRel _ _ hneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ normalOrder ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ normalOrder ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ) = 0]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ normalOrder ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeContract ψ φ) = 0
    simp only [map_smul, smul_eq_zero]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder (timeContract ψ φ) = 0
    have h1 : timeOrderRel ψ φ := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOp⊢ normalOrder (timeContract φ ψ) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel ψ φ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder (timeContract ψ φ) = 0
      have ht : timeOrderRel φ ψ ∨ timeOrderRel ψ φ := Std.Total.total (r := 𝓕.timeOrderRel) φ ψ𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψht:timeOrderRel φ ψ ∨ timeOrderRel ψ φ⊢ timeOrderRel ψ φneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel ψ φ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder (timeContract ψ φ) = 0
      simp_allneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel ψ φ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder (timeContract ψ φ) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel ψ φ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder (timeContract ψ φ) = 0
    rw [timeContract_of_timeOrderRel _ _ h1neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel ψ φ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder ((superCommute (anPart ψ)) (ofFieldOp φ)) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel ψ φ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder ((superCommute (anPart ψ)) (ofFieldOp φ)) = 0]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψh1:timeOrderRel ψ φ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ normalOrder ((superCommute (anPart ψ)) (ofFieldOp φ)) = 0
    simpAll goals completed! 🐙

lemma timeOrder_timeContract_eq_time_mid {φ ψ : 𝓕.FieldOp}
    (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (a b : 𝓕.WickAlgebra) :
    𝓣(a * timeContract φ ψ * b) = timeContract φ ψ * 𝓣(a * b) := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * timeContract φ ψ * b) = timeContract φ ψ * timeOrder (a * b)
  rw [timeContract_of_timeOrderRel _ _ h1𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * (superCommute (anPart φ)) (ofFieldOp ψ) * b) =
  (superCommute (anPart φ)) (ofFieldOp ψ) * timeOrder (a * b)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * (superCommute (anPart φ)) (ofFieldOp ψ) * b) =
  (superCommute (anPart φ)) (ofFieldOp ψ) * timeOrder (a * b)]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * (superCommute (anPart φ)) (ofFieldOp ψ) * b) =
  (superCommute (anPart φ)) (ofFieldOp ψ) * timeOrder (a * b)
  rw [ofFieldOp_eq_sum𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * (superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩) * b) =
  (superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩) * timeOrder (a * b)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * (superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩) * b) =
  (superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩) * timeOrder (a * b)]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * (superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩) * b) =
  (superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩) * timeOrder (a * b)
  simp only [map_sum, Finset.mul_sum, Finset.sum_mul]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ ∑ x, timeOrder (a * (superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩) * b) =
  ∑ i, (superCommute (anPart φ)) (ofCrAnOp ⟨ψ, i⟩) * timeOrder (a * b)
  congre_f𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ (fun x => timeOrder (a * (superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩) * b)) = fun i =>
  (superCommute (anPart φ)) (ofCrAnOp ⟨ψ, i⟩) * timeOrder (a * b)
  funext xe_f𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψ⊢ timeOrder (a * (superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩) * b) =
  (superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩) * timeOrder (a * b)
  match φ with
  | .inAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:timeOrderRel (FieldOp.inAsymp φ) ψh2:timeOrderRel ψ (FieldOp.inAsymp φ)⊢ timeOrder (a * (superCommute (anPart (FieldOp.inAsymp φ))) (ofCrAnOp ⟨ψ, x⟩) * b) =
  (superCommute (anPart (FieldOp.inAsymp φ))) (ofCrAnOp ⟨ψ, x⟩) * timeOrder (a * b)
    simpAll goals completed! 🐙
  | .position φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:timeOrderRel (FieldOp.position φ) ψh2:timeOrderRel ψ (FieldOp.position φ)⊢ timeOrder (a * (superCommute (anPart (FieldOp.position φ))) (ofCrAnOp ⟨ψ, x⟩) * b) =
  (superCommute (anPart (FieldOp.position φ))) (ofCrAnOp ⟨ψ, x⟩) * timeOrder (a * b)
    simp only [anPart_position,]𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:timeOrderRel (FieldOp.position φ) ψh2:timeOrderRel ψ (FieldOp.position φ)⊢ timeOrder (a * (superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofCrAnOp ⟨ψ, x⟩) * b) =
  (superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofCrAnOp ⟨ψ, x⟩) * timeOrder (a * b)
    apply timeOrder_superCommute_eq_time_mid _ _𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:timeOrderRel (FieldOp.position φ) ψh2:timeOrderRel ψ (FieldOp.position φ)⊢ crAnTimeOrderRel ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ ⟨ψ, x⟩𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:timeOrderRel (FieldOp.position φ) ψh2:timeOrderRel ψ (FieldOp.position φ)⊢ crAnTimeOrderRel ⟨ψ, x⟩ ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩
    simp only [crAnTimeOrderRel, h1]𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:timeOrderRel (FieldOp.position φ) ψh2:timeOrderRel ψ (FieldOp.position φ)⊢ crAnTimeOrderRel ⟨ψ, x⟩ ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩
    simp [crAnTimeOrderRel, h2]All goals completed! 🐙
  | .outAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:timeOrderRel (FieldOp.outAsymp φ) ψh2:timeOrderRel ψ (FieldOp.outAsymp φ)⊢ timeOrder (a * (superCommute (anPart (FieldOp.outAsymp φ))) (ofCrAnOp ⟨ψ, x⟩) * b) =
  (superCommute (anPart (FieldOp.outAsymp φ))) (ofCrAnOp ⟨ψ, x⟩) * timeOrder (a * b)
    simp only [anPart_outAsymp]𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:timeOrderRel (FieldOp.outAsymp φ) ψh2:timeOrderRel ψ (FieldOp.outAsymp φ)⊢ timeOrder (a * (superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofCrAnOp ⟨ψ, x⟩) * b) =
  (superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofCrAnOp ⟨ψ, x⟩) * timeOrder (a * b)
    apply timeOrder_superCommute_eq_time_mid _ _𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:timeOrderRel (FieldOp.outAsymp φ) ψh2:timeOrderRel ψ (FieldOp.outAsymp φ)⊢ crAnTimeOrderRel ⟨FieldOp.outAsymp φ, ()⟩ ⟨ψ, x⟩𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:timeOrderRel (FieldOp.outAsymp φ) ψh2:timeOrderRel ψ (FieldOp.outAsymp φ)⊢ crAnTimeOrderRel ⟨ψ, x⟩ ⟨FieldOp.outAsymp φ, ()⟩
    simp only [crAnTimeOrderRel, h1]𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebrax:𝓕.fieldOpToCrAnType ψφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:timeOrderRel (FieldOp.outAsymp φ) ψh2:timeOrderRel ψ (FieldOp.outAsymp φ)⊢ crAnTimeOrderRel ⟨ψ, x⟩ ⟨FieldOp.outAsymp φ, ()⟩
    simp [crAnTimeOrderRel, h2]All goals completed! 🐙

lemma timeOrder_timeContract_eq_time_left {φ ψ : 𝓕.FieldOp}
    (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (b : 𝓕.WickAlgebra) :
    𝓣(timeContract φ ψ * b) = timeContract φ ψ * 𝓣(b) := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeOrder (timeContract φ ψ * b) = timeContract φ ψ * timeOrder b
  trans 𝓣(1 * timeContract φ ψ * b)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeOrder (timeContract φ ψ * b) = timeOrder (1 * timeContract φ ψ * b)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeOrder (1 * timeContract φ ψ * b) = timeContract φ ψ * timeOrder b
  simp only [one_mul]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeOrder (1 * timeContract φ ψ * b) = timeContract φ ψ * timeOrder b
  rw [timeOrder_timeContract_eq_time_mid h1 h2𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeContract φ ψ * timeOrder (1 * b) = timeContract φ ψ * timeOrder b𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeContract φ ψ * timeOrder (1 * b) = timeContract φ ψ * timeOrder b]𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:timeOrderRel φ ψh2:timeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeContract φ ψ * timeOrder (1 * b) = timeContract φ ψ * timeOrder b
  simpAll goals completed! 🐙

lemma timeOrder_timeContract_ne_time {φ ψ : 𝓕.FieldOp}
    (h1 : ¬ (timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) :
    𝓣(timeContract φ ψ) = 0 := by𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)⊢ timeOrder (timeContract φ ψ) = 0
  by_cases h2 : timeOrderRel φ ψpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:timeOrderRel φ ψ⊢ timeOrder (timeContract φ ψ) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder (timeContract φ ψ) = 0
  ·pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:timeOrderRel φ ψ⊢ timeOrder (timeContract φ ψ) = 0 simp_all only [true_and]pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ timeOrder (timeContract φ ψ) = 0
    rw [timeContract_of_timeOrderRel _ _ h2pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart φ)) (ofFieldOp ψ)) = 0pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart φ)) (ofFieldOp ψ)) = 0]pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart φ)) (ofFieldOp ψ)) = 0
    rw [ofFieldOp_eq_sumpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩)) = 0pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩)) = 0]pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩)) = 0
    simp only [map_sum]pos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ ∑ x, timeOrder ((superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩)) = 0
    apply Finset.sum_eq_zeropos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψ⊢ ∀ x ∈ Finset.univ, timeOrder ((superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩)) = 0
    intro x hxpos𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬timeOrderRel ψ φh2:timeOrderRel φ ψx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univ⊢ timeOrder ((superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩)) = 0
    match φ with
    | .inAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬timeOrderRel ψ (FieldOp.inAsymp φ)h2:timeOrderRel (FieldOp.inAsymp φ) ψ⊢ timeOrder ((superCommute (anPart (FieldOp.inAsymp φ))) (ofCrAnOp ⟨ψ, x⟩)) = 0
      simpAll goals completed! 🐙
    | .position φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:¬timeOrderRel ψ (FieldOp.position φ)h2:timeOrderRel (FieldOp.position φ) ψ⊢ timeOrder ((superCommute (anPart (FieldOp.position φ))) (ofCrAnOp ⟨ψ, x⟩)) = 0
      simp only [anPart_position]𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:¬timeOrderRel ψ (FieldOp.position φ)h2:timeOrderRel (FieldOp.position φ) ψ⊢ timeOrder ((superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofCrAnOp ⟨ψ, x⟩)) = 0
      apply timeOrder_superCommute_ne_time𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:¬timeOrderRel ψ (FieldOp.position φ)h2:timeOrderRel (FieldOp.position φ) ψ⊢ ¬(crAnTimeOrderRel ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ ⟨ψ, x⟩ ∧
    crAnTimeOrderRel ⟨ψ, x⟩ ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)
      simp_all [crAnTimeOrderRel]All goals completed! 🐙
    | .outAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬timeOrderRel ψ (FieldOp.outAsymp φ)h2:timeOrderRel (FieldOp.outAsymp φ) ψ⊢ timeOrder ((superCommute (anPart (FieldOp.outAsymp φ))) (ofCrAnOp ⟨ψ, x⟩)) = 0
      simp only [anPart_outAsymp]𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬timeOrderRel ψ (FieldOp.outAsymp φ)h2:timeOrderRel (FieldOp.outAsymp φ) ψ⊢ timeOrder ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofCrAnOp ⟨ψ, x⟩)) = 0
      apply timeOrder_superCommute_ne_time𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpx:𝓕.fieldOpToCrAnType ψhx:x ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬timeOrderRel ψ (FieldOp.outAsymp φ)h2:timeOrderRel (FieldOp.outAsymp φ) ψ⊢ ¬(crAnTimeOrderRel ⟨FieldOp.outAsymp φ, ()⟩ ⟨ψ, x⟩ ∧ crAnTimeOrderRel ⟨ψ, x⟩ ⟨FieldOp.outAsymp φ, ()⟩)
      simp_all [crAnTimeOrderRel]All goals completed! 🐙
  ·neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder (timeContract φ ψ) = 0 rw [timeContract_of_not_timeOrderRel_expand _ _ h2neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)) = 0]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • (superCommute (anPart ψ)) (ofFieldOp φ)) = 0
    simp only [map_smul, smul_eq_zero]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) = 0 ∨ timeOrder ((superCommute (anPart ψ)) (ofFieldOp φ)) = 0
    rightneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart ψ)) (ofFieldOp φ)) = 0
    rw [ofFieldOp_eq_sumneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart ψ)) (∑ i, ofCrAnOp ⟨φ, i⟩)) = 0neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart ψ)) (∑ i, ofCrAnOp ⟨φ, i⟩)) = 0]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ timeOrder ((superCommute (anPart ψ)) (∑ i, ofCrAnOp ⟨φ, i⟩)) = 0
    simp only [map_sum]neg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ ∑ x, timeOrder ((superCommute (anPart ψ)) (ofCrAnOp ⟨φ, x⟩)) = 0
    apply Finset.sum_eq_zeroneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψ⊢ ∀ x ∈ Finset.univ, timeOrder ((superCommute (anPart ψ)) (ofCrAnOp ⟨φ, x⟩)) = 0
    intro x hxneg𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph1:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)h2:¬timeOrderRel φ ψx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univ⊢ timeOrder ((superCommute (anPart ψ)) (ofCrAnOp ⟨φ, x⟩)) = 0
    match ψ with
    | .inAsymp ψ =>𝓕:FieldSpecificationφ:𝓕.FieldOpψ✝:𝓕.FieldOpx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬(timeOrderRel φ (FieldOp.inAsymp ψ) ∧ timeOrderRel (FieldOp.inAsymp ψ) φ)h2:¬timeOrderRel φ (FieldOp.inAsymp ψ)⊢ timeOrder ((superCommute (anPart (FieldOp.inAsymp ψ))) (ofCrAnOp ⟨φ, x⟩)) = 0
      simpAll goals completed! 🐙
    | .position ψ =>𝓕:FieldSpecificationφ:𝓕.FieldOpψ✝:𝓕.FieldOpx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univψ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:¬(timeOrderRel φ (FieldOp.position ψ) ∧ timeOrderRel (FieldOp.position ψ) φ)h2:¬timeOrderRel φ (FieldOp.position ψ)⊢ timeOrder ((superCommute (anPart (FieldOp.position ψ))) (ofCrAnOp ⟨φ, x⟩)) = 0
      simp only [anPart_position]𝓕:FieldSpecificationφ:𝓕.FieldOpψ✝:𝓕.FieldOpx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univψ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:¬(timeOrderRel φ (FieldOp.position ψ) ∧ timeOrderRel (FieldOp.position ψ) φ)h2:¬timeOrderRel φ (FieldOp.position ψ)⊢ timeOrder ((superCommute (ofCrAnOp ⟨FieldOp.position ψ, CreateAnnihilate.annihilate⟩)) (ofCrAnOp ⟨φ, x⟩)) = 0
      apply timeOrder_superCommute_ne_time𝓕:FieldSpecificationφ:𝓕.FieldOpψ✝:𝓕.FieldOpx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univψ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeh1:¬(timeOrderRel φ (FieldOp.position ψ) ∧ timeOrderRel (FieldOp.position ψ) φ)h2:¬timeOrderRel φ (FieldOp.position ψ)⊢ ¬(crAnTimeOrderRel ⟨FieldOp.position ψ, CreateAnnihilate.annihilate⟩ ⟨φ, x⟩ ∧
    crAnTimeOrderRel ⟨φ, x⟩ ⟨FieldOp.position ψ, CreateAnnihilate.annihilate⟩)
      simp_all [crAnTimeOrderRel]All goals completed! 🐙
    | .outAsymp ψ =>𝓕:FieldSpecificationφ:𝓕.FieldOpψ✝:𝓕.FieldOpx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬(timeOrderRel φ (FieldOp.outAsymp ψ) ∧ timeOrderRel (FieldOp.outAsymp ψ) φ)h2:¬timeOrderRel φ (FieldOp.outAsymp ψ)⊢ timeOrder ((superCommute (anPart (FieldOp.outAsymp ψ))) (ofCrAnOp ⟨φ, x⟩)) = 0
      simp only [anPart_outAsymp]𝓕:FieldSpecificationφ:𝓕.FieldOpψ✝:𝓕.FieldOpx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬(timeOrderRel φ (FieldOp.outAsymp ψ) ∧ timeOrderRel (FieldOp.outAsymp ψ) φ)h2:¬timeOrderRel φ (FieldOp.outAsymp ψ)⊢ timeOrder ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp ψ, ()⟩)) (ofCrAnOp ⟨φ, x⟩)) = 0
      apply timeOrder_superCommute_ne_time𝓕:FieldSpecificationφ:𝓕.FieldOpψ✝:𝓕.FieldOpx:𝓕.fieldOpToCrAnType φhx:x ∈ Finset.univψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumh1:¬(timeOrderRel φ (FieldOp.outAsymp ψ) ∧ timeOrderRel (FieldOp.outAsymp ψ) φ)h2:¬timeOrderRel φ (FieldOp.outAsymp ψ)⊢ ¬(crAnTimeOrderRel ⟨FieldOp.outAsymp ψ, ()⟩ ⟨φ, x⟩ ∧ crAnTimeOrderRel ⟨φ, x⟩ ⟨FieldOp.outAsymp ψ, ()⟩)
      simp_all [crAnTimeOrderRel]All goals completed! 🐙

The time contraction of an incoming asymptotic field with another incoming asymptotic field is zero.

This prevents Feynman diagrams where incoming vertices are connected to incoming vertices.


lemma timeContract_inAsymp_inAsymp (φ ψ : ((f : Field 𝓕) × AsymptoticLabel 𝓕 f) × Momentum) :
    timeContract (.inAsymp φ) (.inAsymp ψ) = 0 := by𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeContract (FieldOp.inAsymp φ) (FieldOp.inAsymp ψ) = 0
  rw [timeContract_eq_superCommute𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.inAsymp φ) (FieldOp.inAsymp ψ) then
    (superCommute (anPart (FieldOp.inAsymp φ))) (ofFieldOp (FieldOp.inAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛFieldOp.inAsymp ψ) •
      (superCommute (anPart (FieldOp.inAsymp ψ))) (ofFieldOp (FieldOp.inAsymp φ))) =
  0𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.inAsymp φ) (FieldOp.inAsymp ψ) then
    (superCommute (anPart (FieldOp.inAsymp φ))) (ofFieldOp (FieldOp.inAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛFieldOp.inAsymp ψ) •
      (superCommute (anPart (FieldOp.inAsymp ψ))) (ofFieldOp (FieldOp.inAsymp φ))) =
  0]𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.inAsymp φ) (FieldOp.inAsymp ψ) then
    (superCommute (anPart (FieldOp.inAsymp φ))) (ofFieldOp (FieldOp.inAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛFieldOp.inAsymp ψ) •
      (superCommute (anPart (FieldOp.inAsymp ψ))) (ofFieldOp (FieldOp.inAsymp φ))) =
  0
  simpAll goals completed! 🐙

The time contraction of an outgoing asymptotic field with another outgoing asymptotic field is zero.

This prevents Feynman diagrams where outgoing vertices are connected to outgoing vertices.


lemma timeContract_outAsymp_outAsymp (φ ψ : ((f : Field 𝓕) × AsymptoticLabel 𝓕 f) × Momentum) :
    timeContract (.outAsymp φ) (.outAsymp ψ) = 0 := by𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeContract (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) = 0
  rw [timeContract_eq_superCommute,𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) then
    (superCommute (anPart (FieldOp.outAsymp φ))) (ofFieldOp (FieldOp.outAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp ψ) •
      (superCommute (anPart (FieldOp.outAsymp ψ))) (ofFieldOp (FieldOp.outAsymp φ))) =
  0𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) then
    (superCommute (anPart (FieldOp.outAsymp φ))) (anPart (FieldOp.outAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp ψ) •
      (superCommute (anPart (FieldOp.outAsymp ψ))) (anPart (FieldOp.outAsymp φ))) =
  0 ← anPart_outAsymp_eq_ofFieldOp,𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) then
    (superCommute (anPart (FieldOp.outAsymp φ))) (anPart (FieldOp.outAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp ψ) •
      (superCommute (anPart (FieldOp.outAsymp ψ))) (ofFieldOp (FieldOp.outAsymp φ))) =
  0𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) then
    (superCommute (anPart (FieldOp.outAsymp φ))) (anPart (FieldOp.outAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp ψ) •
      (superCommute (anPart (FieldOp.outAsymp ψ))) (anPart (FieldOp.outAsymp φ))) =
  0 ← anPart_outAsymp_eq_ofFieldOp𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) then
    (superCommute (anPart (FieldOp.outAsymp φ))) (anPart (FieldOp.outAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp ψ) •
      (superCommute (anPart (FieldOp.outAsymp ψ))) (anPart (FieldOp.outAsymp φ))) =
  0𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) then
    (superCommute (anPart (FieldOp.outAsymp φ))) (anPart (FieldOp.outAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp ψ) •
      (superCommute (anPart (FieldOp.outAsymp ψ))) (anPart (FieldOp.outAsymp φ))) =
  0]𝓕:FieldSpecificationφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumψ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (if timeOrderRel (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) then
    (superCommute (anPart (FieldOp.outAsymp φ))) (anPart (FieldOp.outAsymp ψ))
  else
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp ψ) •
      (superCommute (anPart (FieldOp.outAsymp ψ))) (anPart (FieldOp.outAsymp φ))) =
  0
  simp [- anPart_outAsymp]All goals completed! 🐙