Sign associated with joining two Wick contractions

theorem WickContraction.stat_signFinset_right {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i j : Fin φsΛ.uncontractedListGet.length) : FieldStatistic.ofFinset 𝓕.fieldOpStatistic φsΛ.uncontractedListGet.get (φsucΛ.signFinset i j) = FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.map uncontractedListEmd (φsucΛ.signFinset i j))

theorem WickContraction.signFinset_right_map_uncontractedListEmd_eq_filter {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i j : Fin φsΛ.uncontractedListGet.length) : Finset.map uncontractedListEmd (φsucΛ.signFinset i j) = {c ∈ (φsΛ.join φsucΛ).signFinset (uncontractedListEmd i) (uncontractedListEmd j) | c ∈ φsΛ.uncontracted}

theorem WickContraction.sign_right_eq_prod_mul_prod {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : sign φsΛ.uncontractedListGet φsucΛ = (∏ a : ↥↑φsucΛ, (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φsΛ.uncontractedListGet[φsucΛ.sndFieldOfContract a])) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ({c ∈ (φsΛ.join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a)) | c ∉ φsΛ.uncontracted}))) * ∏ a : ↥↑φsucΛ, (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φsΛ.uncontractedListGet[φsucΛ.sndFieldOfContract a])) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ((φsΛ.join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a))))

theorem WickContraction.join_singleton_signFinset_eq_filter {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : ((singleton h).join φsucΛ).signFinset i j = {c ∈ (singleton h).signFinset i j | ¬((((singleton h).join φsucΛ).getDual? c).isSome = true ∧ ∀ (h1 : (((singleton h).join φsucΛ).getDual? c).isSome = true), (((singleton h).join φsucΛ).getDual? c).get h1 < i)}

theorem WickContraction.join_singleton_left_signFinset_eq_filter {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ((singleton h).signFinset i j) = FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset i j) * FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ({c ∈ (singleton h).signFinset i j | (((singleton h).join φsucΛ).getDual? c).isSome = true ∧ ∀ (h1 : (((singleton h).join φsucΛ).getDual? c).isSome = true), (((singleton h).join φsucΛ).getDual? c).get h1 < i})

def WickContraction.joinSignRightExtra {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : ℂ

The difference in sign between φsucΛ.sign and the direct contribution of φsucΛ to (join (singleton h) φsucΛ).

Equations

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

def WickContraction.joinSignLeftExtra {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : ℂ

The difference in sign between (singleton h).sign and the direct contribution of (singleton h) to (join (singleton h) φsucΛ).

Equations

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

theorem WickContraction.join_singleton_sign_left {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : sign φs (singleton h) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φs[j])) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset i j)) * joinSignLeftExtra h φsucΛ

theorem WickContraction.join_singleton_sign_right {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : sign (singleton h).uncontractedListGet φsucΛ = joinSignRightExtra h φsucΛ * ∏ a : ↥↑φsucΛ, (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (singleton h).uncontractedListGet[φsucΛ.sndFieldOfContract a])) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a))))

theorem WickContraction.joinSignRightExtra_eq_i_j_finset_eq_if {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : joinSignRightExtra h φsucΛ = ∏ a : ↥↑φsucΛ, (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (singleton h).uncontractedListGet[φsucΛ.sndFieldOfContract a])) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ((if uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j ∧ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i then {j} else ∅) ∪ if uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i ∧ i < uncontractedListEmd (φsucΛ.sndFieldOfContract a) then {i} else ∅))

theorem WickContraction.joinSignLeftExtra_eq_joinSignRightExtra {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (hs : 𝓕.fieldOpStatistic φs[i] = 𝓕.fieldOpStatistic φs[j]) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : joinSignLeftExtra h φsucΛ = joinSignRightExtra h φsucΛ

theorem WickContraction.join_sign_singleton {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (hs : 𝓕.fieldOpStatistic φs[i] = 𝓕.fieldOpStatistic φs[j]) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : sign φs ((singleton h).join φsucΛ) = sign φs (singleton h) * sign (singleton h).uncontractedListGet φsucΛ

theorem WickContraction.join_sign_induction {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (hc : GradingCompliant φs φsΛ) (n : ℕ) (hn : (↑φsΛ).card = n) : sign φs (φsΛ.join φsucΛ) = sign φs φsΛ * sign φsΛ.uncontractedListGet φsucΛ

theorem WickContraction.join_sign {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (hc : GradingCompliant φs φsΛ) : sign φs (φsΛ.join φsucΛ) = sign φs φsΛ * sign φsΛ.uncontractedListGet φsucΛ

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.

theorem WickContraction.join_sign_timeContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : sign φs (φsΛ.join φsucΛ) • ↑(φsΛ.join φsucΛ).timeContract = sign φs φsΛ • ↑φsΛ.timeContract * sign φsΛ.uncontractedListGet φsucΛ • ↑φsucΛ.timeContract

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.