1. Physlib
  2. QFT
  3. PerturbationTheory
  4. FieldSpecification
  5. NormalOrder
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.FieldSpecification.Filters public import Physlib.QFT.PerturbationTheory.Koszul.KoszulSign import all Mathlib.Data.List.Sort

Normal Ordering of states

@[expose] public section

For a field specification 𝓕, 𝓕.normalOrderRel is a relation on 𝓕.CrAnFieldOp representing normal ordering. It is defined such that 𝓕.normalOrderRel φ₀ φ₁ is true if one of the following is true

    φ₀ is a field creation operator

    φ₁ is a field annihilation operator.

Thus, colloquially 𝓕.normalOrderRel φ₀ φ₁ says the creation operators are less than annihilation operators.

def normalOrderRel : 𝓕.CrAnFieldOp → 𝓕.CrAnFieldOp → Prop := fun a b => CreateAnnihilate.normalOrder (𝓕 |>ᶜ a) (𝓕 |>ᶜ b)

Normal ordering is total.

instance : Std.Total 𝓕.normalOrderRel where total _ _ := total_of CreateAnnihilate.normalOrder _ _

Normal ordering is transitive.

instance : IsTrans 𝓕.CrAnFieldOp 𝓕.normalOrderRel where trans _ _ _ := fun h h' => IsTrans.trans (α := CreateAnnihilate) _ _ _ h h'

A decidable instance on the normal ordering relation.

instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (normalOrderRel φ φ') := CreateAnnihilate.instDecidableNormalOrder (𝓕 |>ᶜ φ) (𝓕 |>ᶜ φ')

Normal order sign.

For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp, 𝓕.normalOrderSign φs is the sign corresponding to the number of fermionic-fermionic exchanges undertaken to normal-order φs using the insertion sort algorithm.

def normalOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ := Wick.koszulSign 𝓕.crAnStatistics 𝓕.normalOrderRel φs
@[simp] lemma normalOrderSign_mul_self (φs : List 𝓕.CrAnFieldOp) : normalOrderSign φs * normalOrderSign φs = 1 := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign φs * normalOrderSign φs = 1 All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφ':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ CreateAnnihilate.create.normalOrder (𝓕|>ᶜφ') All goals completed! 🐙lemma normalOrderSign_cons_create (φ : 𝓕.CrAnFieldOp) (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnFieldOp) : normalOrderSign (φ :: φs) = normalOrderSign φs := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign (φ :: φs) = normalOrderSign φs All goals completed! 🐙@[simp] lemma normalOrderSign_singleton (φ : 𝓕.CrAnFieldOp) : normalOrderSign [φ] = 1 := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOp⊢ normalOrderSign [φ] = 1 All goals completed! 🐙@[simp] lemma normalOrderSign_nil : normalOrderSign (𝓕 := 𝓕) [] = 1 := rflAll goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ ¬CreateAnnihilate.annihilate.normalOrder CreateAnnihilate.create All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign (φa :: φs) = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φa φs * normalOrderSign φs All goals completed! 🐙lemma koszulSignInsert_swap (φ φc φa : 𝓕.CrAnFieldOp) (φs φs' : List 𝓕.CrAnFieldOp) : Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa :: φc :: φs') = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φa :: φs') := Wick.koszulSignInsert_eq_perm _ _ _ _ _ (List.Perm.append_left φs (List.Perm.swap φc φa φs'))All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφc':𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφc':𝓕|>ᶜφc' = CreateAnnihilate.createφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φc' :: φs') * normalOrderSign (φs ++ φc' :: φc :: φs') = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc' :: φc :: φs') * normalOrderSign (φs ++ φc' :: φc :: φs') 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφc':𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφc':𝓕|>ᶜφc' = CreateAnnihilate.createφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc :: φc' :: φs') = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φc' :: φc :: φs') ∨ normalOrderSign (φs ++ φc' :: φc :: φs') = 0 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφc':𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφc':𝓕|>ᶜφc' = CreateAnnihilate.createφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ (φs ++ φc :: φc' :: φs').Perm (φs ++ φc' :: φc :: φs') All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilateφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa :: φa' :: φs') * normalOrderSign (φs ++ φa' :: φa :: φs') = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa' :: φa :: φs') * normalOrderSign (φs ++ φa' :: φa :: φs') 𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilateφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa :: φa' :: φs') = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa' :: φa :: φs') ∨ normalOrderSign (φs ++ φa' :: φa :: φs') = 0 𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilateφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa :: φa' :: φs') = Wick.koszulSignInsert 𝓕.crAnStatistics normalOrderRel φ (φs ++ φa' :: φa :: φs') 𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilateφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ (φs ++ φa :: φa' :: φs').Perm (φs ++ φa' :: φa :: φs') 𝓕:FieldSpecificationφa:𝓕.CrAnFieldOpφa':𝓕.CrAnFieldOphφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatehφa':𝓕|>ᶜφa' = CreateAnnihilate.annihilateφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp⊢ (φa :: φa' :: φs').Perm (φa' :: φa :: φs') All goals completed! 🐙

## Normal order of lists

For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp, 𝓕.normalOrderList φs is the list φs normal-ordered using the insertion sort algorithm. It puts creation operators on the left and annihilation operators on the right. For example:

𝓕.normalOrderList [φ1c, φ1a, φ2c, φ2a] = [φ1c, φ2c, φ1a, φ2a]

def normalOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp := List.insertionSort 𝓕.normalOrderRel φs
@[simp] lemma normalOrderList_nil : normalOrderList (𝓕 := 𝓕) [] = [] := 𝓕:FieldSpecification⊢ normalOrderList [] = [] All goals completed! 🐙@[simp] lemma normalOrderList_statistics (φs : List 𝓕.CrAnFieldOp) : (𝓕 |>ₛ (normalOrderList φs)) = 𝓕 |>ₛ φs := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ofList 𝓕.crAnStatistics (normalOrderList φs) = ofList 𝓕.crAnStatistics φs All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.createφ':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ CreateAnnihilate.create.normalOrder (𝓕|>ᶜφ') All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφ':𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOphi:List.orderedInsert normalOrderRel φ' (φs ++ [φ]) = List.orderedInsert normalOrderRel φ' φs ++ [φ]⊢ (if normalOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ [φ]) else φ'' :: (List.orderedInsert normalOrderRel φ' φs ++ [φ])) = (if normalOrderRel φ' φ'' then φ' :: φ'' :: φs else φ'' :: List.orderedInsert normalOrderRel φ' φs) ++ [φ] 𝓕:FieldSpecificationφ':𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOphi:List.orderedInsert normalOrderRel φ' (φs ++ [φ]) = List.orderedInsert normalOrderRel φ' φs ++ [φ]h✝:normalOrderRel φ' φ''⊢ φ' :: φ'' :: (φs ++ [φ]) = φ' :: φ'' :: φs ++ [φ]𝓕:FieldSpecificationφ':𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOphi:List.orderedInsert normalOrderRel φ' (φs ++ [φ]) = List.orderedInsert normalOrderRel φ' φs ++ [φ]h✝:¬normalOrderRel φ' φ''⊢ φ'' :: (List.orderedInsert normalOrderRel φ' φs ++ [φ]) = φ'' :: List.orderedInsert normalOrderRel φ' φs ++ [φ] next h 𝓕:FieldSpecificationφ':𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOphi:List.orderedInsert normalOrderRel φ' (φs ++ [φ]) = List.orderedInsert normalOrderRel φ' φs ++ [φ]h:normalOrderRel φ' φ''⊢ φ' :: φ'' :: (φs ++ [φ]) = φ' :: φ'' :: φs ++ [φ] All goals completed! 🐙 next h 𝓕:FieldSpecificationφ':𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOphφ:𝓕|>ᶜφ = CreateAnnihilate.annihilateφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOphi:List.orderedInsert normalOrderRel φ' (φs ++ [φ]) = List.orderedInsert normalOrderRel φ' φs ++ [φ]h:¬normalOrderRel φ' φ''⊢ φ'' :: (List.orderedInsert normalOrderRel φ' φs ++ [φ]) = φ'' :: List.orderedInsert normalOrderRel φ' φs ++ [φ] All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOphi:List.insertionSort normalOrderRel (φc :: φs) = φc :: normalOrderList φsh:CreateAnnihilate.annihilate.normalOrder CreateAnnihilate.create⊢ φc :: normalOrderList (φa :: φs) = φa :: φc :: normalOrderList φs All goals completed! 🐙 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOphi:List.insertionSort normalOrderRel (φc :: φs) = φc :: normalOrderList φsh✝:¬normalOrderRel φa φc⊢ φc :: normalOrderList (φa :: φs) = φc :: List.orderedInsert normalOrderRel φa (normalOrderList φs) All goals completed! 🐙All goals completed! 🐙

For a list of creation and annihilation states, the equivalence between Fin φs.length and Fin (normalOrderList φs).length taking each position in φs to it's corresponding position in the normal ordered list. This assumes that we are using the insertion sort method. For example:

    For [φ1c, φ1a, φ2c, φ2a] this equivalence sends 0 ↦ 0, 1 ↦ 2, 2 ↦ 1, 3 ↦ 3.

def normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} : Fin φs.length ≃ Fin (normalOrderList φs).length := Physlib.List.insertionSortEquiv 𝓕.normalOrderRel φs
lemma sum_normalOrderList_length {M : Type} [AddCommMonoid M] (φs : List 𝓕.CrAnFieldOp) (f : Fin (normalOrderList φs).length → M) : ∑ (n : Fin (normalOrderList φs).length), f n = ∑ (n : Fin φs.length), f (normalOrderEquiv n) := Eq.symm (Equiv.sum_comp normalOrderEquiv f)set_option backward.isDefEq.respectTransparency false in @[simp] lemma normalOrderList_get_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n : Fin φs.length) : (normalOrderList φs)[(normalOrderEquiv n).val] = φs[n.val] := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (normalOrderList φs)[↑(normalOrderEquiv n)] = φs[↑n] 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (normalOrderList φs).get (normalOrderEquiv n) = φs[↑n] 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (List.insertionSort normalOrderRel φs).get ((Physlib.List.insertionSortEquiv normalOrderRel φs) n) = φs[↑n] erw [𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (φs.get ∘ ⇑(Physlib.List.insertionSortEquiv normalOrderRel φs).symm) ((Physlib.List.insertionSortEquiv normalOrderRel φs) n) = φs[↑n]𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (φs.get ∘ ⇑(Physlib.List.insertionSortEquiv normalOrderRel φs).symm) ((Physlib.List.insertionSortEquiv normalOrderRel φs) n) = φs[↑n] All goals completed! 🐙All goals completed! 🐙

For a field specification 𝓕, a list φs = φ₀…φₙ of 𝓕.CrAnFieldOp and an i < φs.length, then normalOrderSign (φ₀…φᵢ₋₁φᵢ₊₁…φₙ) is equal to the product of

    normalOrderSign φ₀…φₙ,

    𝓢(φᵢ, φ₀…φᵢ₋₁) i.e. the sign needed to remove φᵢ from φ₀…φₙ,

    𝓢(φᵢ, _) where _ is the list of elements appearing before φᵢ after normal ordering, i.e. the sign needed to insert φᵢ back into the normal-ordered list at the correct place.

𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpi:Fin φs.length⊢ normalOrderSign φs * (exchangeSign (𝓕.crAnStatistics (φs.get i))) (ofList 𝓕.crAnStatistics (List.take (↑i) φs)) * (exchangeSign (𝓕.crAnStatistics (φs.get i))) (ofList 𝓕.crAnStatistics (List.take (↑((Physlib.List.insertionSortEquiv normalOrderRel φs) i)) (List.insertionSort normalOrderRel φs))) = normalOrderSign φs * (exchangeSign (𝓕.crAnStatistics (φs.get i))) (ofList 𝓕.crAnStatistics (List.take (↑i) φs)) * (exchangeSign (𝓕.crAnStatistics (φs.get i))) (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv i)) (normalOrderList φs))) All goals completed! 🐙
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOphφ':𝓕|>ᶜφ' = CreateAnnihilate.annihilatehφ:𝓕|>ᶜφ = CreateAnnihilate.annihilate⊢ CreateAnnihilate.annihilate.normalOrder CreateAnnihilate.annihilate All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙