Sign on inserting and contracting

The main results of this file are sign_insert_some_of_lt and sign_insert_some_of_not_lt which write the sign of (φsΛ ↩Λ φ i (some k)).sign in terms of the sign of φsΛ.

Sign insert some

theorem WickContraction.stat_ofFinset_eq_one_of_gradingCompliant {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (a : Finset (Fin φs.length)) (φsΛ : WickContraction φs.length) (hg : GradingCompliant φs φsΛ) (hnon : ∀ (i : Fin φs.length), φsΛ.getDual? i = none → i ∉ a) (hsom : ∀ (i : Fin φs.length) (h : (φsΛ.getDual? i).isSome = true), i ∈ a → (φsΛ.getDual? i).get h ∈ a) : FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get a = 1

theorem WickContraction.signFinset_insertAndContract_some {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (i1 i2 : Fin φs.length) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : (insertAndContract φ φsΛ i (some j)).signFinset ((finCongr ⋯) (i.succAbove i1)) ((finCongr ⋯) (i.succAbove i2)) = if i.succAbove i1 < i ∧ i < i.succAbove i2 ∧ i1 < ↑j then insert ((finCongr ⋯) i) (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)) else if i1 < ↑j ∧ ↑j < i2 ∧ ¬i.succAbove i1 < i then (insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)).erase ((finCongr ⋯) (i.succAbove ↑j)) else insertAndContractLiftFinset φ i (φsΛ.signFinset i1 i2)

def WickContraction.signInsertSomeProd {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : ℂ

Given a Wick contraction φsΛ the sign defined in the following way, related to inserting a field φ at position i and contracting it with j : φsΛ.uncontracted.

• For each contracted pair {a1, a2} in φsΛ with a1 < a2 the sign 𝓢(φ, φₐ₂) if a₁ < i ≤ a₂ and a₁ < j.
• For each contracted pair {a1, a2} in φsΛ with a1 < a2 the sign 𝓢(φⱼ, φₐ₂) if a₁ < j < a₂ and i < a₁.

Equations

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

def WickContraction.signInsertSomeCoef {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : ℂ

Given a Wick contraction φsΛ the sign defined in the following way, related to inserting a field φ at position i and contracting it with j : φsΛ.uncontracted.

• If j < i, for each field φₐ in φⱼ₊₁…φᵢ₋₁ without a dual at position < j the sign 𝓢(φₐ, φᵢ).
• Else, for each field φₐ in φᵢ…φⱼ₋₁ of φs without dual at position < i the sign 𝓢(φₐ, φⱼ).

Equations

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

def WickContraction.signInsertSome {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : ℂ

Given a Wick contraction φsΛ associated with a list of states φs and an i : Fin φs.length.succ, the change in sign of the contraction associated with inserting φ into φs at position i and contracting it with j : c.uncontracted.

Equations

• WickContraction.signInsertSome φ φs φsΛ i j = WickContraction.signInsertSomeCoef φ φs φsΛ i j * WickContraction.signInsertSomeProd φ φs φsΛ i j

theorem WickContraction.sign_insert_some {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : sign (List.insertIdx (↑i) φ φs) (insertAndContract φ φsΛ i (some j)) = signInsertSome φ φs φsΛ i j * sign φs φsΛ

theorem WickContraction.signInsertSomeProd_eq_one_if {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hφj : 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑j]) : signInsertSomeProd φ φs φsΛ i j = ∏ a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }, if φsΛ.fstFieldOfContract a < ↑j ∧ (i.succAbove (φsΛ.fstFieldOfContract a) < i ∧ i < i.succAbove (φsΛ.sndFieldOfContract a) ∨ ↑j < φsΛ.sndFieldOfContract a ∧ ¬i.succAbove (φsΛ.fstFieldOfContract a) < i) then (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φs[φsΛ.sndFieldOfContract a]) else 1

theorem WickContraction.signInsertSomeProd_eq_prod_prod {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hφj : 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑j]) (hg : GradingCompliant φs φsΛ) : signInsertSomeProd φ φs φsΛ i j = ∏ a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }, ∏ x : { x : Fin φs.length // x ∈ ↑a }, if ↑x < ↑j ∧ (i.succAbove ↑x < i ∧ i < i.succAbove ((φsΛ.getDual? ↑x).get ⋯) ∨ ↑j < (φsΛ.getDual? ↑x).get ⋯ ∧ ¬i.succAbove ↑x < i) then (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φs[↑x]) else 1

theorem WickContraction.signInsertSomeProd_eq_prod_fin {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hφj : 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑j]) (hg : GradingCompliant φs φsΛ) : signInsertSomeProd φ φs φsΛ i j = ∏ x : Fin φs.length, if h : (φsΛ.getDual? x).isSome = true then if x < ↑j ∧ (i.succAbove x < i ∧ i < i.succAbove ((φsΛ.getDual? x).get h) ∨ ↑j < (φsΛ.getDual? x).get h ∧ ¬i.succAbove x < i) then (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φs[↑x]) else 1 else 1

theorem WickContraction.signInsertSomeProd_eq_finset {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hφj : 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑j]) (hg : GradingCompliant φs φsΛ) : signInsertSomeProd φ φs φsΛ i j = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => (φsΛ.getDual? x).isSome = true ∧ ∀ (h : (φsΛ.getDual? x).isSome = true), x < ↑j ∧ (i.succAbove x < i ∧ i < i.succAbove ((φsΛ.getDual? x).get h) ∨ ↑j < (φsΛ.getDual? x).get h ∧ ¬i.succAbove x < i)) Finset.univ))

theorem WickContraction.signInsertSomeCoef_if {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hφj : 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑j]) : signInsertSomeCoef φ φs φsΛ i j = if i < i.succAbove ↑j then (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic (List.insertIdx (↑i) φ φs).get ((insertAndContract φ φsΛ i (some j)).signFinset ((finCongr ⋯) i) ((finCongr ⋯) (i.succAbove ↑j)))) else (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic (List.insertIdx (↑i) φ φs).get ((insertAndContract φ φsΛ i (some j)).signFinset ((finCongr ⋯) (i.succAbove ↑j)) ((finCongr ⋯) i)))

theorem WickContraction.stat_signFinset_insert_some_self_fst {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : FieldStatistic.ofFinset 𝓕.fieldOpStatistic (List.insertIdx (↑i) φ φs).get ((insertAndContract φ φsΛ i (some j)).signFinset ((finCongr ⋯) i) ((finCongr ⋯) (i.succAbove ↑j))) = FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => i < i.succAbove x ∧ x < ↑j ∧ (φsΛ.getDual? x = none ∨ ∀ (h : (φsΛ.getDual? x).isSome = true), i < i.succAbove ((φsΛ.getDual? x).get h))) Finset.univ)

theorem WickContraction.stat_signFinset_insert_some_self_snd {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : FieldStatistic.ofFinset 𝓕.fieldOpStatistic (List.insertIdx (↑i) φ φs).get ((insertAndContract φ φsΛ i (some j)).signFinset ((finCongr ⋯) (i.succAbove ↑j)) ((finCongr ⋯) i)) = FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => ↑j < x ∧ i.succAbove x < i ∧ (φsΛ.getDual? x = none ∨ ∀ (h : (φsΛ.getDual? x).isSome = true), ↑j < (φsΛ.getDual? x).get h)) Finset.univ)

theorem WickContraction.signInsertSomeCoef_eq_finset {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hφj : 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑j]) : signInsertSomeCoef φ φs φsΛ i j = if i < i.succAbove ↑j then (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => i < i.succAbove x ∧ x < ↑j ∧ (φsΛ.getDual? x = none ∨ ∀ (h : (φsΛ.getDual? x).isSome = true), i < i.succAbove ((φsΛ.getDual? x).get h))) Finset.univ)) else (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => ↑j < x ∧ i.succAbove x < i ∧ (φsΛ.getDual? x = none ∨ ∀ (h : (φsΛ.getDual? x).isSome = true), ↑j < (φsΛ.getDual? x).get h)) Finset.univ))

theorem WickContraction.signInsertSome_mul_filter_contracted_of_lt {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hk : i.succAbove ↑k < i) (hg : GradingCompliant φs φsΛ ∧ 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑k]) : signInsertSome φ φs φsΛ i k * (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => x ≤ ↑k) φsΛ.uncontracted)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => i.succAbove x < i) Finset.univ))

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 i < a₁. 1c. For each field φₐ in φₖ₊₁…φᵢ₋₁ without a dual at position < k the sign 𝓢(φₐ, φᵢ). and the sign constructed as follows: 2a. For each uncontracted field φₐ in φ₀…φₖ in φsΛ the sign 𝓢(φ, φₐ) 2b. For each field in φₐ in φ₀…φᵢ₋₁ the sign 𝓢(φ, φₐ).

The outline of why this is true can be got by considering contributions of fields.

• φₐ, i ≤ a. No contributions.
• φₖ, k -> 2a, k -> 2b
• φₐ, a ≤ k uncontracted a -> 2a, a -> 2b.
• φₐ, k < a < i uncontracted a -> 1c, a -> 2b.

For contracted fields {a₁, a₂} in φsΛ with a₁ < a₂ we have the following cases:

• φₐ₁ φₐ₂ a₁ < a₂ < k < i, a₁ -> 2b, a₂ -> 2b,
• φₐ₁ φₐ₂ a₁ < k < a₂ < i, a₁ -> 2b, a₂ -> 2b,
• φₐ₁ φₐ₂ a₁ < k < i ≤ a₂, a₁ -> 2b, a₂ -> 1a
• φₐ₁ φₐ₂ k < a₁ < a₂ < i, a₁ -> 2b, a₂ -> 2b, a₁ -> 1c, a₂ -> 1c
• φₐ₁ φₐ₂ k < a₁ < i ≤ a₂ ,a₁ -> 2b, a₁ -> 1c
• φₐ₁ φₐ₂ k < i ≤ a₁ < a₂ , No contributions.

theorem WickContraction.signInsertSome_mul_filter_contracted_of_not_lt {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hk : ¬i.succAbove ↑k < i) (hg : GradingCompliant φs φsΛ ∧ 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑k]) : signInsertSome φ φs φsΛ i k * (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => x < ↑k) φsΛ.uncontracted)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => i.succAbove x < i) Finset.univ))

The following two signs are equal for i < i.succAbove k. 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 i < a₁. 1c. For each field φₐ in φᵢ…φₖ₋₁ of φs without dual at position < i the sign 𝓢(φₐ, φⱼ). and the sign constructed as follows: 2a. For each uncontracted field φₐ in φ₀…φₖ₋₁ in φsΛ the sign 𝓢(φ, φₐ) 2b. For each field in φₐ in φ₀…φᵢ₋₁ the sign 𝓢(φ, φₐ).

The outline of why this is true can be got by considering contributions of fields.

• φₐ, k < a. No contributions.
• φₖ, No Contributes
• φₐ, a < i uncontracted a -> 2a, a -> 2b.
• φₐ, i ≤ a < k uncontracted a -> 1c, a -> 2a.

For contracted fields {a₁, a₂} in φsΛ with a₁ < a₂ we have the following cases:

• φₐ₁ φₐ₂ a₁ < a₂ < i ≤ k, a₁ -> 2b, a₂ -> 2b
• φₐ₁ φₐ₂ a₁ < i ≤ a₂ < k, a₁ -> 2b, a₂ -> 1a
• φₐ₁ φₐ₂ a₁ < i ≤ k < a₂, a₁ -> 2b, a₂ -> 1a
• φₐ₁ φₐ₂ i ≤ a₁ < a₂ < k, a₂ -> 1c, a₁ -> 1c
• φₐ₁ φₐ₂ i ≤ a₁ < k < a₂ , a₁ -> 1c, a₁ -> 1b
• φₐ₁ φₐ₂ i ≤ k ≤ a₁ < a₂ , No contributions

theorem WickContraction.sign_insert_some_of_lt {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hk : i.succAbove ↑k < i) (hg : GradingCompliant φs φsΛ ∧ 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑k]) : sign (List.insertIdx (↑i) φ φs) (insertAndContract φ φsΛ i (some k)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => x ≤ ↑k) φsΛ.uncontracted)) * (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => i.succAbove x < i) Finset.univ)) * sign φs φsΛ

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted such that k<i, the sign of φsΛ ↩Λ φ i (some k) is equal to the product of

• the sign associated with moving φ through the φsΛ-uncontracted FieldOp in φ₀…φₖ,
• the sign associated with moving φ through all FieldOp in φ₀…φᵢ₋₁,
• the sign of φsΛ.

The proof of this result involves a careful consideration of the contributions of different FieldOp in φs to the sign of φsΛ ↩Λ φ i (some k).

theorem WickContraction.sign_insert_some_of_not_lt {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hk : ¬i.succAbove ↑k < i) (hg : GradingCompliant φs φsΛ ∧ 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑k]) : sign (List.insertIdx (↑i) φ φs) (insertAndContract φ φsΛ i (some k)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => x < ↑k) φsΛ.uncontracted)) * (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => i.succAbove x < i) Finset.univ)) * sign φs φsΛ

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted such that i ≤ k, the sign of φsΛ ↩Λ φ i (some k) is equal to the product of

• the sign associated with moving φ through the φsΛ-uncontracted FieldOp in φ₀…φₖ₋₁,
• the sign associated with moving φ through all the FieldOp in φ₀…φᵢ₋₁,
• the sign of φsΛ.

The proof of this result involves a careful consideration of the contributions of different FieldOp in φs to the sign of φsΛ ↩Λ φ i (some k).

theorem WickContraction.sign_insert_some_zero {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hn : GradingCompliant φs φsΛ ∧ 𝓕.fieldOpStatistic φ = 𝓕.fieldOpStatistic φs[↑k]) : sign (List.insertIdx (↑0) φ φs) (insertAndContract φ φsΛ 0 (some k)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.filter (fun (x : Fin φs.length) => x < ↑k) φsΛ.uncontracted)) * sign φs φsΛ

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a k in φsΛ.uncontracted, the sign of φsΛ ↩Λ φ 0 (some k) is equal to the product of

• the sign associated with moving φ through the φsΛ-uncontracted FieldOp in φ₀…φₖ₋₁,
• the sign of φsΛ.

This is a direct corollary of sign_insert_some_of_not_lt.