Static Wick's theorem

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

φs = ∑ φsΛ, φsΛ.staticWickTerm

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

The proof is via induction on φs.

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

The inductive step works as follows:

For the LHS:

The proof considers φ₀…φₙ as φ₀(φ₁…φₙ) and uses the induction hypothesis on φ₁…φₙ.

This gives terms of the form φ * φsΛ.staticWickTerm on which mul_staticWickTerm_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 1) and optional uncontracted elements of φsΛ (from 2)

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.