Time contractions

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

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

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

Equations

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

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

theorem FieldSpecification.FieldOpAlgebra.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.FieldOpAlgebra.timeContract_of_not_timeOrderRel {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) (h : ¬timeOrderRel φ ψ) : timeContract φ ψ = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic ψ) • timeContract ψ φ

theorem FieldSpecification.FieldOpAlgebra.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.FieldOpAlgebra.timeContract_mem_center {𝓕 : FieldSpecification} (φ ψ : 𝓕.FieldOp) : timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra

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

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

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

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

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

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