The type FieldStatistic is the type containing two elements bosonic and fermionic. This type is used to specify if a field or operator obeys bosonic or fermionic statistics.

Constructors

bosonic : FieldStatistic

fermionic : FieldStatistic

The type FieldStatistic carries an instance of a commutative group in which

• bosonic * bosonic = bosonic

• bosonic * fermionic = fermionic

• fermionic * bosonic = fermionic

• fermionic * fermionic = bosonic

This group is isomorphic to ℤ₂.

The exchange sign, exchangeSign, is defined as the group homomorphism

FieldStatistic →* FieldStatistic →* ℂ,

for which exchangeSign a b is -1 if both a and b are fermionic and 1 otherwise. The exchange sign is the sign one picks up on exchanging an operator or field φ₁ of statistic a with an operator or field φ₂ of statistic b, i.e. φ₁φ₂ → φ₂φ₁.

The notation 𝓢(a, b) is used for the exchange sign of a and b.

The structure FieldSpecification is defined to have the following content:

• A type Field whose elements are the constituent fields of the theory.

• For every field f in Field, a type PositionLabel f whose elements label the different position operators associated with the field f. For example,

  • For f a real-scalar field, PositionLabel f will have a unique element.

  • For f a complex-scalar field, PositionLabel f will have two elements, one for the field operator and one for its conjugate.

  • For f a Dirac fermion, PositionLabel f will have eight elements, one for each Lorentz index of the field and its conjugate.

  • For f a Weyl fermion, PositionLabel f will have four elements, one for each Lorentz index of the field and its conjugate.

• For every field f in Field, a type AsymptoticLabel f whose elements label the different types of incoming asymptotic field operators associated with the field f (this also matches the types of outgoing asymptotic field operators). For example,

  • For f a real-scalar field, AsymptoticLabel f will have a unique element.

  • For f a complex-scalar field, AsymptoticLabel f will have two elements, one for the field operator and one for its conjugate.

  • For f a Dirac fermion, AsymptoticLabel f will have four elements, two for each spin.

  • For f a Weyl fermion, AsymptoticLabel f will have two elements, one for each spin.

• For each field f in Field, a field statistic statistic f which classifies f as either bosonic or fermionic.

For a field specification 𝓕, the inductive type 𝓕.FieldOp is defined to contain the following elements:

• For every f in 𝓕.Field, element of e of AsymptoticLabel f and 3-momentum p, an element labelled inAsymp f e p corresponding to an incoming asymptotic field operator of the field f, of label e (e.g. specifying the spin), and momentum p.

• For every f in 𝓕.Field, element of e of PositionLabel f and space-time position x, an element labelled position f e x corresponding to a position field operator of the field f, of label e (e.g. specifying the Lorentz index), and position x.

• For every f in 𝓕.Field, element of e of AsymptoticLabel f and 3-momentum p, an element labelled outAsymp f e p corresponding to an outgoing asymptotic field operator of the field f, of label e (e.g. specifying the spin), and momentum p.

As an example, if f corresponds to a Weyl-fermion field, then

• For inAsymp f e p, e would correspond to a spin s, and inAsymp f e p would, once represented in the operator algebra, be proportional to the creation operator a(p, s).

• position f e x, e would correspond to a Lorentz index a, and position f e x would, once represented in the operator algebra, be proportional to the operator

  ∑ s, ∫ d³p/(…) (xₐ(p,s) a(p, s) e ^ (-i p x) + yₐ(p,s) a†(p, s) e ^ (-i p x)).

• outAsymp f e p, e would correspond to a spin s, and outAsymp f e p would, once represented in the operator algebra, be proportional to the annihilation operator a†(p, s).

Constructors

inAsymp {𝓕 : _root_.FieldSpecification}
    : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) →
      𝓕.FieldOp

position {𝓕 : _root_.FieldSpecification}
    : ((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime →
      𝓕.FieldOp

outAsymp {𝓕 : _root_.FieldSpecification}
    : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) →
      𝓕.FieldOp

For a field specification 𝓕, and an element φ of 𝓕.FieldOp. The field statistic fieldOpStatistic φ is defined to be the statistic associated with the field underlying φ.

The following notation is used in relation to fieldOpStatistic:

• For φ an element of 𝓕.FieldOp, 𝓕 |>s φ is fieldOpStatistic φ.

• For φs a list of 𝓕.FieldOp, 𝓕 |>s φs is the product of fieldOpStatistic φ over the list φs.

• For a function f : Fin n → 𝓕.FieldOp and a finite set a of Fin n, 𝓕 |>s ⟨f, a⟩ is the product of fieldOpStatistic (f i) for all i ∈ a.

The type CreateAnnihilate is the type containing two elements create and annihilate. This type is used to specify if an operator is a creation, or annihilation, operator or the sum thereof or integral thereof etc.

Constructors

create : CreateAnnihilate

annihilate : CreateAnnihilate

For a field specification 𝓕, the (sigma) type 𝓕.CrAnFieldOp corresponds to the type of creation and annihilation parts of field operators. It formally defined to consist of the following elements:

• For each incoming asymptotic field operator φ in 𝓕.FieldOp an element written as ⟨φ, ()⟩ in 𝓕.CrAnFieldOp, corresponding to the creation part of φ. Here φ has no annihilation part. (Here () is the unique element of Unit.)

• For each position field operator φ in 𝓕.FieldOp an element of 𝓕.CrAnFieldOp written as ⟨φ, .create⟩, corresponding to the creation part of φ.

• For each position field operator φ in 𝓕.FieldOp an element of 𝓕.CrAnFieldOp written as ⟨φ, .annihilate⟩, corresponding to the annihilation part of φ.

• For each outgoing asymptotic field operator φ in 𝓕.FieldOp an element written as ⟨φ, ()⟩ in 𝓕.CrAnFieldOp, corresponding to the annihilation part of φ. Here φ has no creation part. (Here () is the unique element of Unit.)

As an example, if f corresponds to a Weyl-fermion field, it would contribute the following elements to 𝓕.CrAnFieldOp

• For each spin s, an element corresponding to an incoming asymptotic operator: a(p, s).

• For each each Lorentz index a, an element corresponding to the creation part of a position operator:

  ∑ s, ∫ d³p/(…) (xₐ (p,s) a(p, s) e ^ (-i p x)).

• For each each Lorentz index a,an element corresponding to annihilation part of a position operator:

  ∑ s, ∫ d³p/(…) (yₐ(p,s) a†(p, s) e ^ (-i p x)).

• For each spin s, element corresponding to an outgoing asymptotic operator: a†(p, s).

For a field specification 𝓕, 𝓕.crAnFieldOpToCreateAnnihilate is the map from 𝓕.CrAnFieldOp to CreateAnnihilate taking φ to create if

• φ corresponds to an incoming asymptotic field operator or the creation part of a position based field operator.

otherwise it takes φ to annihilate.

For a field specification 𝓕, and an element φ in 𝓕.CrAnFieldOp, the field statistic crAnStatistics φ is defined to be the statistic associated with the field 𝓕.Field (or the 𝓕.FieldOp) underlying φ.

The following notation is used in relation to crAnStatistics:

• For φ an element of 𝓕.CrAnFieldOp, 𝓕 |>s φ is crAnStatistics φ.

• For φs a list of 𝓕.CrAnFieldOp, 𝓕 |>s φs is the product of crAnStatistics φ over the list φs.

For a field specification 𝓕, the algebra 𝓕.FieldOpFreeAlgebra is the free algebra generated by 𝓕.CrAnFieldOp.

For a field specification 𝓕, and a element φ of 𝓕.CrAnFieldOp, ofCrAnOpF φ is defined as the element of 𝓕.FieldOpFreeAlgebra formed by φ.

The algebra 𝓕.FieldOpFreeAlgebra satisfies the universal property that for any other algebra A (e.g. the operator algebra of the theory) with a map f : 𝓕.CrAnFieldOp → A (e.g. the inclusion of the creation and annihilation parts of field operators into the operator algebra) there is a unique algebra map g : 𝓕.FieldOpFreeAlgebra → A such that g ∘ ofCrAnOpF = f.

The unique g is given by FreeAlgebra.lift ℂ f.

For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp, ofCrAnListF φs is defined as the element of 𝓕.FieldOpFreeAlgebra obtained by the product of ofCrAnListF φ for each φ in φs. For example ofCrAnListF [φ₁, φ₂, φ₃] = ofCrAnOpF φ₁ * ofCrAnOpF φ₂ * ofCrAnOpF φ₃. The set of all ofCrAnListF φs forms a basis of FieldOpFreeAlgebra 𝓕.

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, ofFieldOpF φ is the element of 𝓕.FieldOpFreeAlgebra formed by summing over ofCrAnOpF of the creation and annihilation parts of φ.

For example, for φ an incoming asymptotic field operator we get ofCrAnOpF ⟨φ, ()⟩, and for φ a position field operator we get ofCrAnOpF ⟨φ, .create⟩ + ofCrAnOpF ⟨φ, .annihilate⟩.

For a field specification 𝓕, and a list φs of 𝓕.FieldOp, 𝓕.ofFieldOpListF φs is defined as the element of 𝓕.FieldOpFreeAlgebra obtained by the product of ofFieldOpF φ for each φ in φs. For example ofFieldOpListF [φ₁, φ₂, φ₃] = ofFieldOpF φ₁ * ofFieldOpF φ₂ * ofFieldOpF φ₃.

For a field specification 𝓕, the algebra 𝓕.FieldOpFreeAlgebra is graded by FieldStatistic. Those ofCrAnListF φs for which φs has an overall bosonic statistic (i.e. 𝓕 |>s φs = bosonic) span bosonic submodule, whilst those ofCrAnListF φs for which φs has an overall fermionic statistic (i.e. 𝓕 |>s φs = fermionic) span the fermionic submodule.

For a field specification 𝓕, the super commutator superCommuteF is defined as the linear map 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra which on the lists φs and φs' of 𝓕.CrAnFieldOp gives

superCommuteF φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs.

The notation [a, b]ₛF can be used for superCommuteF a b.

For a field specification 𝓕, and two lists φs = φ₀…φₙ and φs' of 𝓕.CrAnFieldOp the following super commutation relation holds:

[φs', φ₀…φₙ]ₛF = ∑ i, 𝓢(φs', φ₀…φᵢ₋₁) • φ₀…φᵢ₋₁ * [φs', φᵢ]ₛF * φᵢ₊₁ … φₙ

The proof of this relation is via induction on the length of φs.

For a field specification 𝓕, the algebra 𝓕.FieldOpAlgebra is defined as the quotient of the free algebra 𝓕.FieldOpFreeAlgebra by the ideal generated by

• [ofCrAnOpF φc, ofCrAnOpF φc']ₛF for φc and φc' field creation operators. This corresponds to the condition that two creation operators always super-commute.

• [ofCrAnOpF φa, ofCrAnOpF φa']ₛF for φa and φa' field annihilation operators. This corresponds to the condition that two annihilation operators always super-commute.

• [ofCrAnOpF φ, ofCrAnOpF φ']ₛF for φ and φ' operators with different statistics. This corresponds to the condition that two operators with different statistics always super-commute. In other words, fermions and bosons always super-commute.

• [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF. This corresponds to the condition, when combined with the conditions above, that the super-commutator is in the center of the algebra.

For a field specification 𝓕, ι is defined as the projection

𝓕.FieldOpFreeAlgebra →ₐ[ℂ] 𝓕.FieldOpAlgebra

taking each element of 𝓕.FieldOpFreeAlgebra to its equivalence class in FieldOpAlgebra 𝓕.

For a field specification 𝓕 and an element φ of 𝓕.CrAnFieldOp, ofCrAnOp φ is defined as the element of 𝓕.FieldOpAlgebra given by ι (ofCrAnOpF φ).

For a field specification 𝓕 and a list φs of 𝓕.CrAnFieldOp, ofCrAnList φs is defined as the element of 𝓕.FieldOpAlgebra given by ι (ofCrAnListF φ).

For a field specification 𝓕 and an element φ of 𝓕.FieldOp, ofFieldOp φ is defined as the element of 𝓕.FieldOpAlgebra given by ι (ofFieldOpF φ).

For a field specification 𝓕 and a list φs of 𝓕.FieldOp, ofFieldOpList φs is defined as the element of 𝓕.FieldOpAlgebra given by ι (ofFieldOpListF φ).

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the annihilation part of 𝓕.FieldOp as an element of 𝓕.FieldOpAlgebra. Thus for φ

• an incoming asymptotic state this is 0.

• a position based state this is ofCrAnOp ⟨φ, .create⟩.

• an outgoing asymptotic state this is ofCrAnOp ⟨φ, ()⟩.

For a field specification 𝓕, and an element φ of 𝓕.FieldOp, the creation part of 𝓕.FieldOp as an element of 𝓕.FieldOpAlgebra. Thus for φ

• an incoming asymptotic state this is ofCrAnOp ⟨φ, ()⟩.

• a position based state this is ofCrAnOp ⟨φ, .create⟩.

• an outgoing asymptotic state this is 0.

For field specification 𝓕, and an element φ of 𝓕.FieldOp the following relation holds:

ofFieldOp φ = crPart φ + anPart φ

That is, every field operator splits into its creation part plus its annihilation part.

For a field statistic 𝓕, the algebra 𝓕.FieldOpAlgebra is graded by FieldStatistic. Those ofCrAnList φs for which φs has an overall bosonic statistic (i.e. 𝓕 |>s φs = bosonic) span bosonic submodule, whilst those ofCrAnList φs for which φs has an overall fermionic statistic (i.e. 𝓕 |>s φs = fermionic) span the fermionic submodule.

For a field specification 𝓕, superCommute is the linear map

FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕

defined as the descent of ι ∘ superCommuteF in both arguments. In particular for φs and φs' lists of 𝓕.CrAnFieldOp in FieldOpAlgebra 𝓕 the following relation holds:

superCommute φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs

The notation [a, b]ₛ is used for superCommute a b.

Given a natural number n, which will correspond to the number of fields needing contracting, a Wick contraction is a finite set of pairs of Fin n (numbers 0, ..., n-1), such that no element of Fin n occurs in more than one pair. The pairs are the positions of fields we 'contract' together.

For n = 3 there are 4 possible Wick contractions:

• ∅, corresponding to the case where no fields are contracted.

• {{0, 1}}, corresponding to the case where the field at position 0 and 1 are contracted.

• {{0, 2}}, corresponding to the case where the field at position 0 and 2 are contracted.

• {{1, 2}}, corresponding to the case where the field at position 1 and 2 are contracted.

The proof of this result uses the fact that Lean is an executable programming language and can calculate all Wick contractions for a given n.

For n = 4 there are 10 possible Wick contractions including e.g.

• ∅, corresponding to the case where no fields are contracted.

• {{0, 1}, {2, 3}}, corresponding to the case where the fields at position 0 and 1 are contracted, and the fields at position 2 and 3 are contracted.

• {{0, 2}, {1, 3}}, corresponding to the case where the fields at position 0 and 2 are contracted, and the fields at position 1 and 3 are contracted.

The proof of this result uses the fact that Lean is an executable programming language and can calculate all Wick contractions for a given n.

For a field specification 𝓕, φs a list of 𝓕.FieldOp and a Wick contraction φsΛ of φs, the Wick contraction φsΛ is said to be GradingCompliant if for every pair in φsΛ the contracted fields are either both fermionic or both bosonic. In other words, in a GradingCompliant Wick contraction if no contracted pairs occur between fermionic and bosonic fields.

The number of Wick contractions in WickContraction n is equal to the terms in Online Encyclopedia of Integer Sequences (OEIS) A000085. That is: 1, 1, 2, 4, 10, 26, 76, 232, 764, 2620, 9496, ...

For a Wick contraction c, c.uncontracted is defined as the finset of elements of Fin n which are not in any contracted pair.

Given a Wick Contraction φsΛ of a list φs of 𝓕.FieldOp. The list φsΛ.uncontractedListGet of 𝓕.FieldOp is defined as the list φs with all contracted positions removed, leaving the uncontracted 𝓕.FieldOp.

The notation [φsΛ]ᵘᶜ is used for φsΛ.uncontractedListGet.

Given a Wick contraction φsΛ for a list φs of 𝓕.FieldOp, an element φ of 𝓕.FieldOp, an i ≤ φs.length and a k in Option φsΛ.uncontracted i.e. is either none or some element of φsΛ.uncontracted, the new Wick contraction φsΛ.insertAndContract φ i k is defined by inserting φ into φs after the first i-elements and moving the values representing the contracted pairs in φsΛ accordingly. If k is not none, but rather some k, to this contraction is added the contraction of φ (at position i) with the new position of k after φ is added.

In other words, φsΛ.insertAndContract φ i k is formed by adding φ to φs at position i, and contracting φ with the field originally at position k if k is not none. It is a Wick contraction of the list φs.insertIdx φ i corresponding to φs with φ inserted at position i.

The notation φsΛ ↩Λ φ i k is used to denote φsΛ.insertAndContract φ i k.

For a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp and a i ≤ φs.length then a sum over Wick contractions of φs with φ inserted at i is equal to the sum over Wick contractions φsΛ of just φs and the sum over optional uncontracted elements of the φsΛ.

In other words,

∑ (φsΛ : WickContraction (φs.insertIdx i φ).length), f φsΛ

where (φs.insertIdx i φ) is φs with φ inserted at position i. is equal to

∑ (φsΛ : WickContraction φs.length), ∑ k, f (φsΛ ↩Λ φ i k) .

where the sum over k is over all k in Option φsΛ.uncontracted.

Given a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, join φsΛ φsucΛ is defined as the Wick contraction of φs consisting of the contractions in φsΛ and those in φsucΛ.

As an example, for φs = [φ1, φ2, φ3, φ4], φsΛ = {{0, 1}} corresponding to the contraction of φ1 and φ2 in φs and φsucΛ = {{0, 1}} corresponding to the contraction of φ3 and φ4 in [φsΛ]ᵘᶜ = [φ3, φ4], then join φsΛ φsucΛ is the contraction {{0, 1}, {2, 3}} of φs.

For a list φs of 𝓕.FieldOp, and a Wick contraction φsΛ of φs, the complex number φsΛ.sign is defined to be the sign (1 or -1) corresponding to the number of fermionic-fermionic exchanges that must be done to put contracted pairs within φsΛ next to one another, starting recursively from the contracted pair whose first element occurs at the left-most position.

As an example, if [φ1, φ2, φ3, φ4] correspond to fermionic fields then the sign associated with

• {{0, 1}} is 1

• {{0, 1}, {2, 3}} is 1

• {{0, 2}, {1, 3}} is -1

For a list φs of 𝓕.FieldOp, a grading compliant Wick contraction φsΛ of φs, and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, the following relation holds (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign.

In φsΛ.sign the sign is determined by starting with the contracted pair whose first element occurs at the left-most position. This lemma manifests that this choice does not matter, and that contracted pairs can be brought together in any order.

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a graded compliant Wick contraction φsΛ of φs, an i ≤ φs.length, and a φ in 𝓕.FieldOp, then (φsΛ ↩Λ φ i none).sign = s * φsΛ.sign where s is the sign arrived at by moving φ through the elements of φ₀…φᵢ₋₁ which are contracted with some element.

The proof of this result involves a careful consideration of the contributions of different FieldOps in φs to the sign of φsΛ ↩Λ φ i none.

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a graded compliant Wick contraction φsΛ of φs, and a φ in 𝓕.FieldOp, then (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign.

This is a direct corollary of sign_insert_none.

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 such that i ≤ k, the sign of φsΛ ↩Λ φ i (some k) is equal to the product of

• the sign associated with moving φ through the φsΛ-uncontracted FieldOp in φ₀…φₖ₋₁,

• the sign associated with moving φ through all the FieldOp in φ₀…φᵢ₋₁,

• the sign of φsΛ.

The proof of this result involves a careful consideration of the contributions of different FieldOp in φs to the sign of φsΛ ↩Λ φ i (some k).

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 such that k<i, the sign of φsΛ ↩Λ φ i (some k) is equal to the product of

• the sign associated with moving φ through the φsΛ-uncontracted FieldOp in φ₀…φₖ,

• the sign associated with moving φ through all FieldOp in φ₀…φᵢ₋₁,

• the sign of φsΛ.

The proof of this result involves a careful consideration of the contributions of different FieldOp in φs to the sign of φsΛ ↩Λ φ i (some k).

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

• the sign associated with moving φ through the φsΛ-uncontracted FieldOp in φ₀…φₖ₋₁,

• the sign of φsΛ.

This is a direct corollary of sign_insert_some_of_not_lt.

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]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)

where s is the exchange sign for φ and the uncontracted fields in φ₀…φᵢ₋₁.

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

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)]ᵘᶜ) is equal to the normal ordering of [φsΛ]ᵘᶜ with the 𝓕.FieldOp corresponding to k removed.

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

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.

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.

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.

For a list φs of 𝓕.FieldOp, and a Wick contraction φsΛ of φs, the element of 𝓕.FieldOpAlgebra, φsΛ.staticWickTerm is defined as

φsΛ.sign • φsΛ.staticContract * 𝓝([φsΛ]ᵘᶜ).

This is a term which appears in the static version Wick's theorem.

For the empty list [] of 𝓕.FieldOp, the staticWickTerm of the Wick contraction corresponding to the empty set ∅ (the only Wick contraction of []) is 1.

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, and an element φ of 𝓕.FieldOp, then (φsΛ ↩Λ φ 0 none).staticWickTerm is equal to

φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)

The proof of this result relies on

• staticContract_insert_none to rewrite the static contract.

• sign_insert_none_zero to rewrite the sign.

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

• the sign 𝓢(φ, φ₀…φᵢ₋₁)

• the sign φsΛ.sign

• φsΛ.staticContract

• s • [anPart φ, ofFieldOp φs[k]]ₛ where s is the sign associated with moving φ through uncontracted fields in φ₀…φₖ₋₁

• the normal ordering of [φsΛ]ᵘᶜ with the field operator φs[k] removed.

The proof of this result ultimately relies on

• staticContract_insert_some to rewrite static contractions.

• normalOrder_uncontracted_some to rewrite normal orderings.

• sign_insert_some_zero to rewrite signs.

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, the following relation holds

φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ 0 k).staticWickTerm

where the sum is over all k in Option φsΛ.uncontracted, so k is either none or some k.

The proof proceeds as follows:

• ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum is used to expand φ 𝓝([φsΛ]ᵘᶜ) as a sum over k in Option φsΛ.uncontracted of terms involving [anPart φ, φs[k]]ₛ.

• Then staticWickTerm_insert_zero_none and staticWickTerm_insert_zero_some are used to equate terms.

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:

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

2. 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:

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

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

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

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

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

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

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

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

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

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

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

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 such that k < i, with the condition that φs[k] does not have time greater or equal to φ, then (φsΛ ↩Λ φ i (some k)).timeContract is equal to the product of

• [anPart φ, φs[k]]ₛ

• φsΛ.timeContract

• the exchange sign of φ with the uncontracted fields in φ₀…φₖ₋₁.

• the exchange sign of φ with the uncontracted fields in φ₀…φₖ.

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

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 such that i ≤ k, with the condition that φ has greater or equal time to φs[k], then (φsΛ ↩Λ φ i (some k)).timeContract is equal to the product of

• [anPart φ, φs[k]]ₛ

• φsΛ.timeContract

• two copies of the exchange sign of φ with the uncontracted fields in φ₀…φₖ₋₁. These two exchange signs cancel each other out but are included for convenience.

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

For a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs, and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, (join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract is equal to the product of

• φsΛ.sign • φsΛ.timeContract and

• φsucΛ.sign • φsucΛ.timeContract.

For a list φs of 𝓕.FieldOp, and a Wick contraction φsΛ of φs, the element of 𝓕.FieldOpAlgebra, φsΛ.wickTerm is defined as

φsΛ.sign • φsΛ.timeContract * 𝓝([φsΛ]ᵘᶜ).

This is a term which appears in the Wick's theorem.

For the empty list [] of 𝓕.FieldOp, the wickTerm of the Wick contraction corresponding to the empty set ∅ (the only Wick contraction of []) is 1.

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and i ≤ φs.length, then (φsΛ ↩Λ φ i none).wickTerm is equal to

𝓢(φ, φ₀…φᵢ₋₁) φsΛ.sign • φsΛ.timeContract * 𝓝(φ :: [φsΛ]ᵘᶜ)

The proof of this result relies on

• normalOrder_uncontracted_none to rewrite normal orderings.

• timeContract_insert_none to rewrite the time contract.

• sign_insert_none to rewrite the sign.

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, i ≤ φs.length and a k in φsΛ.uncontracted, such that all 𝓕.FieldOp in φ₀…φᵢ₋₁ have time strictly less than φ and φ has a time greater than or equal to all FieldOp in φ₀…φₙ, then (φsΛ ↩Λ φ i (some k)).staticWickTerm is equal to the product of

• the sign 𝓢(φ, φ₀…φᵢ₋₁)

• the sign φsΛ.sign

• φsΛ.timeContract

• s • [anPart φ, ofFieldOp φs[k]]ₛ where s is the sign associated with moving φ through uncontracted fields in φ₀…φₖ₋₁

• the normal ordering [φsΛ]ᵘᶜ with the field corresponding to k removed.

The proof of this result relies on

• timeContract_insert_some_of_not_lt and timeContract_insert_some_of_lt to rewrite time contractions.

• normalOrder_uncontracted_some to rewrite normal orderings.

• sign_insert_some_of_not_lt and sign_insert_some_of_lt to rewrite signs.

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and i ≤ φs.length such that all 𝓕.FieldOp in φ₀…φᵢ₋₁ have time strictly less than φ and φ has a time greater than or equal to all FieldOp in φ₀…φₙ, then

φ * φsΛ.wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) • ∑ k, (φsΛ ↩Λ φ i k).wickTerm

where the sum is over all k in Option φsΛ.uncontracted, so k is either none or some k.

The proof proceeds as follows:

• ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum is used to expand φ 𝓝([φsΛ]ᵘᶜ) as a sum over k in Option φsΛ.uncontracted of terms involving [anPart φ, φs[k]]ₛ.

• Then wickTerm_insert_none and wickTerm_insert_some are used to equate terms.

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:

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

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

3. 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:

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