Sign associated with a contraction

def WickContraction.signFinset {n : ℕ} (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n)

Given a Wick contraction c : WickContraction n and i1 i2 : Fin n the finite set of elements of Fin n between i1 and i2 which are either uncontracted or are contracted but are contracted with an element occurring after i1. In other words, the elements of Fin n between i1 and i2 which are not contracted with before i1. One should assume i1 < i2 otherwise this finite set is empty.

Equations

• c.signFinset i1 i2 = {i : Fin n | i1 < i ∧ i < i2 ∧ (c.getDual? i = none ∨ ∀ (h : (c.getDual? i).isSome = true), i1 < (c.getDual? i).get h)}

def WickContraction.sign {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : ℂ

For a list φs of 𝓕.FieldOp, and a Wick contraction φsΛ of φs, the complex number φsΛ.sign is defined to be the sign (1 or -1) corresponding to the number of fermionic-fermionic exchanges that must be done to put contracted pairs within φsΛ next to one another, starting recursively from the contracted pair whose first element occurs at the left-most position.

As an example, if [φ1, φ2, φ3, φ4] correspond to fermionic fields then the sign associated with

• {{0, 1}} is 1
• {{0, 1}, {2, 3}} is 1
• {{0, 2}, {1, 3}} is -1

Equations

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

theorem WickContraction.sign_empty {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : sign φs empty = 1

theorem WickContraction.sign_congr {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (φsΛ : WickContraction φs.length) : sign φs' ((congr ⋯) φsΛ) = sign φs φsΛ