Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions

(φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) : 𝓝(ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ) = 𝓢(𝓕|>ₛφ,𝓕|>ₛ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) • 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ))

Let $\mathcal{F}$ be a field specification and $\phi_s$ be a list of field operators. Let $\Lambda$ be a Wick contraction on $\phi_s$. Suppose we insert a field operator $\phi$ into $\phi_s$ at index $i$ and contract it with an existing uncontracted index $k$ of $\Lambda$ to form a new contraction $\Lambda' = \Lambda \hookleftarrow_\Lambda \phi, i, \text{some } k$. Then the normal ordering of the product of uncontracted field operators of $\Lambda'$, denoted $\mathcal{N}([\Lambda']^{uc})$, is equal to the normal ordering of the list of uncontracted operators of $\Lambda$ with the operator corresponding to the index $k$ removed. Formally, $$\mathcal{N}([\Lambda \hookleftarrow_\Lambda \phi, i, \text{some } k]^{uc}) = \mathcal{N}(\text{eraseIdx}([\Lambda]^{uc}, \text{pos}(k)))$$ where $\text{pos}(k)$ is the position of the uncontracted index $k$ in the sorted list of uncontracted indices of $\Lambda$.