Physlib.QFT.PerturbationTheory.WickAlgebra.WicksTheorem

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.WickTerm

Wick's theorem

This file constrains the time-dependent version of Wick's theorem for lists of fields containing both fermions and bosons.

Wick's theorem is related to Isserlis' theorem in mathematics.

@[expose] public section

Wick terms

Wick's theorem

lemma wicks_theorem_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
    ∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm
    = ∑ (φs'Λ : WickContraction φs'.length), φs'Λ.wickTerm := h ▸ rfl

For a list φs of 𝓕.FieldOp, Wick's theorem states that

𝓣(φs) = ∑ φsΛ, φsΛ.wickTerm

where the sum is over all Wick contraction φsΛ.

The proof is via induction on φs.

The base case φs = [] is handled by wickTerm_empty_nil.

The inductive step works as follows:

For the LHS:

timeOrder_eq_maxTimeField_mul_finset is used to write 𝓣(φ₀…φₙ) as 𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ) where φᵢ is the maximal time field in φ₀…φₙ

The induction hypothesis is then used on 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ) to expand it as a sum over Wick contractions of φ₀…φᵢ₋₁φᵢ₊₁φₙ.

This gives terms of the form φᵢ * φsΛ.wickTerm on which mul_wickTerm_eq_sum is used where φsΛ is a Wick contraction of φ₀…φᵢ₋₁φᵢ₊₁φ, to rewrite terms as a sum over optional uncontracted elements of φsΛ

On the LHS we now have a sum over Wick contractions φsΛ of φ₀…φᵢ₋₁φᵢ₊₁φ (from 2) and optional uncontracted elements of φsΛ (from 3)

For the RHS:

The sum over Wick contractions of φ₀…φₙ on the RHS is split via insertLift_sum into a sum over Wick contractions φsΛ of φ₀…φᵢ₋₁φᵢ₊₁φ and sum over optional uncontracted elements of φsΛ.

Both sides are now sums over the same thing and their terms equate by the nature of the lemmas used.


theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
    ∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm
  | [] =>𝓕:FieldSpecification⊢ timeOrder (ofFieldOpList []) = ∑ φsΛ, φsΛ.wickTerm by𝓕:FieldSpecification⊢ timeOrder (ofFieldOpList []) = ∑ φsΛ, φsΛ.wickTerm
    simp only [timeOrder_ofFieldOpList_nil, List.length_nil, sum_WickContraction_nil,
      wickTerm_empty_nil]All goals completed! 🐙
  | φ :: φs =>𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrder (ofFieldOpList (φ :: φs)) = ∑ φsΛ, φsΛ.wickTerm by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrder (ofFieldOpList (φ :: φs)) = ∑ φsΛ, φsΛ.wickTerm
    have ih := wicks_theorem (eraseMaxTimeField φ φs)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTerm⊢ timeOrder (ofFieldOpList (φ :: φs)) = ∑ φsΛ, φsΛ.wickTerm
    conv_lhs => rw [timeOrder_eq_maxTimeField_mul_finset, ih, Finset.mul_sum]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTerm| ∑ i,
  (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
      ofFieldOp (maxTimeField φ φs) *
    i.wickTerm
    have h1 : φ :: φs =
        (eraseMaxTimeField φ φs).insertIdx (maxTimeFieldPosFin φ φs) (maxTimeField φ φs) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrder (ofFieldOpList (φ :: φs)) = ∑ φsΛ, φsΛ.wickTerm𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)⊢ ∑ i,
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
          (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
            {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
        ofFieldOp (maxTimeField φ φs) *
      i.wickTerm =
  ∑ φsΛ, φsΛ.wickTerm
      simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one,
        maxTimeField, insertionSortMin, List.get_eq_getElem]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTerm⊢ φ :: φs =
  ((φ :: φs).eraseIdx ↑(insertionSortMinPos timeOrderRel φ φs)).insertIdx (↑(maxTimeFieldPosFin φ φs))
    (φ :: φs)[↑(insertionSortMinPos timeOrderRel φ φs)]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)⊢ ∑ i,
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
          (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
            {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
        ofFieldOp (maxTimeField φ φs) *
      i.wickTerm =
  ∑ φsΛ, φsΛ.wickTerm
      erw [insertIdx_eraseIdx_fin𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTerm⊢ φ :: φs = φ :: φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)⊢ ∑ i,
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
          (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
            {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
        ofFieldOp (maxTimeField φ φs) *
      i.wickTerm =
  ∑ φsΛ, φsΛ.wickTerm]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)⊢ ∑ i,
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
          (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
            {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
        ofFieldOp (maxTimeField φ φs) *
      i.wickTerm =
  ∑ φsΛ, φsΛ.wickTerm𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)⊢ ∑ i,
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
          (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
            {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
        ofFieldOp (maxTimeField φ φs) *
      i.wickTerm =
  ∑ φsΛ, φsΛ.wickTerm
    conv_rhs => rw [wicks_theorem_congr h1, insertLift_sum]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)| ∑ φsΛ, ∑ k, (φsΛ↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm
    refine Finset.sum_congr rfl fun c _ => ?_𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
      ofFieldOp (maxTimeField φ φs) *
    c.wickTerm =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm
    rw [Algebra.smul_mul_assoc,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
      (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
        {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
    (ofFieldOp (maxTimeField φ φs) * c.wickTerm) =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ((exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs})) •
    ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTermhlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k]hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs) mul_wickTerm_eq_sum
      (maxTimeField φ φs) (eraseMaxTimeField φ φs) (maxTimeFieldPosFin φ φs) c,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
      (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
        {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
    (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) •
      ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTermhlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k]hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ((exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs})) •
    ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTermhlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k]hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs) smul_smul𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ((exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs})) •
    ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTermhlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k]hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ((exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs})) •
    ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTermhlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k]hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs)]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ((exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) *
      (exchangeSign (𝓕|>ₛmaxTimeField φ φs))
        (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get
          {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs})) •
    ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTerm =
  ∑ k, (c↩Λ(maxTimeField φ φs)(maxTimeFieldPosFin φ φs)k).wickTermhlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k]hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs)
    simp only [exchangeSign_mul_self, Nat.succ_eq_add_one, Fintype.sum_option,
      Finset.univ_eq_attach, smul_add, one_smul]hlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k]hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs)
    ·hlt𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length), timeOrderRel (maxTimeField φ φs) (eraseMaxTimeField φ φs)[k] exact fun k => timeOrder_maxTimeField _ _ kAll goals completed! 🐙
    ·hn𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpih:timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) = ∑ φsΛ, φsΛ.wickTermh1:φ :: φs = (eraseMaxTimeField φ φs).insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs)c:WickContraction (eraseMaxTimeField φ φs).lengthx✝:c ∈ Finset.univ⊢ ∀ (k : Fin (eraseMaxTimeField φ φs).length),
  (maxTimeFieldPosFin φ φs).succAbove k < maxTimeFieldPosFin φ φs →
    ¬timeOrderRel (eraseMaxTimeField φ φs)[k] (maxTimeField φ φs) exact fun k => lt_maxTimeFieldPosFin_not_timeOrder _ _ kAll goals completed! 🐙
termination_by φs => φs.length