Time contractions

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

def FieldSpecification.WickAlgebra.timeContract {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) : 𝓕.WickAlgebra

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

Equations

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

theorem FieldSpecification.WickAlgebra.timeContract_eq_smul {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) : timeContract φ ψ = timeOrder (ofFieldOp φ * ofFieldOp ψ) + -1 • normalOrder (ofFieldOp φ * ofFieldOp ψ)

theorem FieldSpecification.WickAlgebra.timeContract_of_timeOrderRel {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) (h : timeOrderRel φ ψ) : timeContract φ ψ = (superCommute (anPart φ)) (ofFieldOp ψ)

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

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

theorem FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) (h : ¬timeOrderRel φ ψ) : timeContract φ ψ = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic ψ) • timeContract ψ φ

theorem FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel_expand {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) (h : ¬timeOrderRel φ ψ) : timeContract φ ψ = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic ψ) • (superCommute (anPart ψ)) (ofFieldOp φ)

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

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

theorem FieldSpecification.WickAlgebra.timeContract_eq_superCommute {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) : timeContract φ ψ = if timeOrderRel φ ψ then (superCommute (anPart φ)) (ofFieldOp ψ) else (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic ψ) • (superCommute (anPart ψ)) (ofFieldOp φ)

theorem FieldSpecification.WickAlgebra.timeContract_mem_center {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) : timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.WickAlgebra

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

theorem FieldSpecification.WickAlgebra.timeContract_zero_of_diff_grade {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) (h : 𝓕.fieldOpStatistic φ ≠ 𝓕.fieldOpStatistic ψ) : timeContract φ ψ = 0

theorem FieldSpecification.WickAlgebra.normalOrder_timeContract {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) : normalOrder (timeContract φ ψ) = 0

theorem FieldSpecification.WickAlgebra.timeOrder_timeContract_eq_time_mid {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (a b : 𝓕.WickAlgebra) : timeOrder (a * timeContract φ ψ * b) = timeContract φ ψ * timeOrder (a * b)

theorem FieldSpecification.WickAlgebra.timeOrder_timeContract_eq_time_left {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (b : 𝓕.WickAlgebra) : timeOrder (timeContract φ ψ * b) = timeContract φ ψ * timeOrder b

theorem FieldSpecification.WickAlgebra.timeOrder_timeContract_neq_time {𝓕 : FieldSpecification} {φ ψ : 𝓕.FieldOp} (h1 : ¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) : timeOrder (timeContract φ ψ) = 0

theorem FieldSpecification.WickAlgebra.timeContract_inAsymp_inAsymp {𝓕 : FieldSpecification} (φ ψ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : timeContract (FieldOp.inAsymp φ) (FieldOp.inAsymp ψ) = 0

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.

theorem FieldSpecification.WickAlgebra.timeContract_outAsymp_outAsymp {𝓕 : FieldSpecification} (φ ψ : ((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum) : timeContract (FieldOp.outAsymp φ) (FieldOp.outAsymp ψ) = 0

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.