Research proof index

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

Given a Wick contraction c for n, a position i : Fin n.succ and an optional uncontracted element j : Option (c.uncontracted) of c. The Wick contraction for n.succ formed by 'inserting' i into Fin n and contracting it optionally with j. -/ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c.uncontracted)) : Wi...

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

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

The following signs for a grading compliant Wick contraction are equal: - The sign φsΛ.signInsertNone φ φs i which is given by the following: For each contracted pair {a1, a2} in φsΛ if a1 < a2 such that i is within the range a1 < i < a2 we pick up a sign equal to 𝓢(φ, φs[a2]). - The sign got by moving φ through φ₀…φᵢ₋₁ and only picking...

The following two signs are equal for i.succAbove k < i. The sign signInsertSome φ φs φsΛ i k which is constructed as follows: 1a. For each contracted pair {a1, a2} in φsΛ with a1 < a2 the sign 𝓢(φ, φₐ₂) if a₁ < i ≤ a₂ and a₁ < k. 1b. For each contracted pair {a1, a2} in φsΛ with a1 < a2 the sign 𝓢(φⱼ, φₐ₂) if a₁ < k < a₂ and `...