1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickAlgebra
  5. TimeOrder
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.WickAlgebra.SuperCommute public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder

Time Ordering on Field operator algebra

@[expose] public section𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧ crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧ crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2l1:List 𝓕.CrAnFieldOp := List.takeWhile (fun c => decide ¬crAnTimeOrderRel φ1 c) (List.insertionSort crAnTimeOrderRel (φs1 ++ φs2)) ++ List.filter (fun c => decide (crAnTimeOrderRel φ1 c ∧ crAnTimeOrderRel c φ1)) φs1l2:List 𝓕.CrAnFieldOp := List.filter (fun c => decide (crAnTimeOrderRel φ1 c ∧ crAnTimeOrderRel c φ1)) φs2 ++ List.filter (fun c => decide (crAnTimeOrderRel φ1 c ∧ ¬crAnTimeOrderRel c φ1)) (List.insertionSort crAnTimeOrderRel (φs1 ++ φs2))h123:ι (timeOrderF (ofCrAnListF (φs1 ++ φ1 :: φ2 :: φ3 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ1, φ2, φ3]) * ι (ofCrAnListF l2))h132:ι (timeOrderF (ofCrAnListF (φs1 ++ φ1 :: φ3 :: φ2 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ1, φ3, φ2]) * ι (ofCrAnListF l2))hp231:[φ2, φ3, φ1].Perm [φ1, φ2, φ3]h231:ι (timeOrderF (ofCrAnListF (φs1 ++ φ2 :: φ3 :: φ1 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ2, φ3, φ1]) * ι (ofCrAnListF l2))h321:ι (timeOrderF (ofCrAnListF (φs1 ++ φ3 :: φ2 :: φ1 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ3, φ2, φ1]) * ι (ofCrAnListF l2))⊢ crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ1, φ2, φ3]) * ι (ofCrAnListF l2))) - (exchangeSign (𝓕.crAnStatistics φ1)) (ofList 𝓕.crAnStatistics [φ2, φ3]) • crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ2, φ3, φ1]) * ι (ofCrAnListF l2)) - (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • (crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ1, φ3, φ2]) * ι (ofCrAnListF l2)) - (exchangeSign (𝓕.crAnStatistics φ1)) (ofList 𝓕.crAnStatistics [φ3, φ2]) • crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ3, φ2, φ1]) * ι (ofCrAnListF l2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF ([φ1] ++ [φ2, φ3]) - (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ2, φ3]) • ofCrAnListF ([φ2, φ3] ++ [φ1])) - (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • ι (ofCrAnListF ([φ1] ++ [φ3, φ2]) - (exchangeSign (ofList 𝓕.crAnStatistics [φ1])) (ofList 𝓕.crAnStatistics [φ3, φ2]) • ofCrAnListF ([φ3, φ2] ++ [φ1]))) * ι (ofCrAnListF l2)) 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOph:crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧ crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧ crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2l1:List 𝓕.CrAnFieldOp := List.takeWhile (fun c => decide ¬crAnTimeOrderRel φ1 c) (List.insertionSort crAnTimeOrderRel (φs1 ++ φs2)) ++ List.filter (fun c => decide (crAnTimeOrderRel φ1 c ∧ crAnTimeOrderRel c φ1)) φs1l2:List 𝓕.CrAnFieldOp := List.filter (fun c => decide (crAnTimeOrderRel φ1 c ∧ crAnTimeOrderRel c φ1)) φs2 ++ List.filter (fun c => decide (crAnTimeOrderRel φ1 c ∧ ¬crAnTimeOrderRel c φ1)) (List.insertionSort crAnTimeOrderRel (φs1 ++ φs2))h123:ι (timeOrderF (ofCrAnListF (φs1 ++ φ1 :: φ2 :: φ3 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ1, φ2, φ3]) * ι (ofCrAnListF l2))h132:ι (timeOrderF (ofCrAnListF (φs1 ++ φ1 :: φ3 :: φ2 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ1, φ3, φ2]) * ι (ofCrAnListF l2))hp231:[φ2, φ3, φ1].Perm [φ1, φ2, φ3]h231:ι (timeOrderF (ofCrAnListF (φs1 ++ φ2 :: φ3 :: φ1 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ2, φ3, φ1]) * ι (ofCrAnListF l2))h321:ι (timeOrderF (ofCrAnListF (φs1 ++ φ3 :: φ2 :: φ1 :: φs2))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * ι (ofCrAnListF [φ3, φ2, φ1]) * ι (ofCrAnListF l2))⊢ crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ1, φ2, φ3]) * ι (ofCrAnListF l2))) - (exchangeSign (𝓕.crAnStatistics φ1)) (ofList 𝓕.crAnStatistics [φ2, φ3]) • crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ2, φ3, φ1]) * ι (ofCrAnListF l2))) - (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • (crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ1, φ3, φ2]) * ι (ofCrAnListF l2))) - (exchangeSign (𝓕.crAnStatistics φ1)) (ofList 𝓕.crAnStatistics [φ3, φ2]) • crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ3, φ2, φ1]) * ι (ofCrAnListF l2)))) = crAnTimeOrderSign (φs1 ++ φ1 :: φ2 :: φ3 :: φs2) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ1, φ2, φ3]) * ι (ofCrAnListF l2)) - (exchangeSign (𝓕.crAnStatistics φ1)) (ofList 𝓕.crAnStatistics [φ2, φ3]) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ2, φ3, φ1]) * ι (ofCrAnListF l2))) - (exchangeSign (𝓕.crAnStatistics φ2)) (𝓕.crAnStatistics φ3) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ1, φ3, φ2]) * ι (ofCrAnListF l2)) - (exchangeSign (𝓕.crAnStatistics φ1)) (ofList 𝓕.crAnStatistics [φ3, φ2]) • (ι (ofCrAnListF l1) * (ι (ofCrAnListF [φ3, φ2, φ1]) * ι (ofCrAnListF l2))))) All goals completed! 🐙𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOph:¬(crAnTimeOrderRel φ1 φ2 ∧ crAnTimeOrderRel φ1 φ3 ∧ crAnTimeOrderRel φ2 φ1 ∧ crAnTimeOrderRel φ2 φ3 ∧ crAnTimeOrderRel φ3 φ1 ∧ crAnTimeOrderRel φ3 φ2)⊢ ι (timeOrderF (ofCrAnListF φs1 * timeOrderF ((superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3))) * ofCrAnListF φs2)) = 0 All goals completed! 🐙@[simp] lemma ι_timeOrderF_superCommuteF_superCommuteF {φ1 φ2 φ3 : 𝓕.CrAnFieldOp} (a b : 𝓕.FieldOpFreeAlgebra) : ι 𝓣ᶠ(a * [ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛF]ₛF * b) = 0 := 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ pb b ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pb x ⋯𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ pb 0 ⋯𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)) (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb y hy → pb (x + y) ⋯𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb (a • x) ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pb x ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOp⊢ pb (ofCrAnListFBasis φs) ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOp⊢ ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ pa a ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pa x ⋯𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ pa 0 ⋯𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)) (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa y hy → pa (x + y) ⋯𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa (a • x) ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (h : x ∈ Set.range ⇑ofCrAnListFBasis), pa x ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0φs':List 𝓕.CrAnFieldOp⊢ pa (ofCrAnListFBasis φs') ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ pa 0 ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)) (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa y hy → pa (x + y) ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hy:y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hpx:pa x hxhpy:pa y hy⊢ pa (x + y) ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa (a • x) ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * ofCrAnListF φs)) = 0x:ℂhx:𝓕.FieldOpFreeAlgebrahpx:hx ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)⊢ pa hx hpx → pa (x • hx) ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ pb 0 ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)) (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb y hy → pb (x + y) ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hy:y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hpx:pb x hxhpy:pb y hy⊢ pb (x + y) ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb (a • x) ⋯ 𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) * b)) = 0x:ℂhx:𝓕.FieldOpFreeAlgebrahpx:hx ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)⊢ pb hx hpx → pb (x • hx) ⋯ All goals completed! 🐙example (c1 c2 : ℂ) (a : 𝓕.WickAlgebra) : c1 • c2 • a = c2 • c1 • a := smul_comm c1 c2 a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * ofCrAnListF φs)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * ofCrAnListF φs))φs':List 𝓕.CrAnFieldOph1:List.insertionSort crAnTimeOrderRel (φs' ++ φs) = List.takeWhile (fun c => !decide (crAnTimeOrderRel φ c)) (List.insertionSort crAnTimeOrderRel (φs' ++ φs)) ++ (List.filter (fun c => decide (crAnTimeOrderRel φ c) && decide (crAnTimeOrderRel c φ)) φs' ++ (List.filter (fun c => decide (crAnTimeOrderRel φ c) && decide (crAnTimeOrderRel c φ)) φs ++ List.filter (fun c => decide (crAnTimeOrderRel φ c) && !decide (crAnTimeOrderRel c φ)) (List.insertionSort crAnTimeOrderRel (φs' ++ φs))))hq:¬𝓕.crAnStatistics φ ≠ 𝓕.crAnStatistics ψ⊢ crAnTimeOrderSign (φs' ++ φs) • (ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι (ofCrAnListF (crAnTimeOrderList (φs' ++ φs)))) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * ι (crAnTimeOrderSign (φs' ++ φs) • ofCrAnListF (crAnTimeOrderList (φs' ++ φs))) All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * ofCrAnListF φs)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * ofCrAnListF φs))⊢ pa 0 ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * ofCrAnListF φs)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * ofCrAnListF φs))⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)) (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa y hy → pa (x + y) ⋯ 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * ofCrAnListF φs)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * ofCrAnListF φs))x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hy:y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hpx:pa x hxhpy:pa y hy⊢ pa (x + y) ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * ofCrAnListF φs)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * ofCrAnListF φs))⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pa x hx → pa (a • x) ⋯ 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))φs:List 𝓕.CrAnFieldOppa:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun a hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * ofCrAnListF φs)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * ofCrAnListF φs))x:ℂhx:𝓕.FieldOpFreeAlgebrahpx:hx ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)⊢ pa hx hpx → pa (x • hx) ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))⊢ pb 0 ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)) (hy : y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb y hy → pb (x + y) ⋯ 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hy:y ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)hpx:pb x hxhpy:pb y hy⊢ pb (x + y) ⋯ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))⊢ ∀ (a : ℂ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)), pb x hx → pb (a • x) ⋯ 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrapb:(b : 𝓕.FieldOpFreeAlgebra) → b ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis) → Prop := fun b hc => ι (timeOrderF (a * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b))x:ℂhx:𝓕.FieldOpFreeAlgebrahpx:hx ∈ Submodule.span ℂ (Set.range ⇑ofCrAnListFBasis)⊢ pb hx hpx → pb (x • hx) ⋯ All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ✝:¬(crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)a:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrahφψ:¬crAnTimeOrderRel ψ φ⊢ ι (timeOrderF (a * timeOrderF (-(exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) • (superCommuteF (ofCrAnOpF ψ)) (ofCrAnOpF φ)) * b)) = 0 All goals completed! 🐙

Defining time order for FiedOpAlgebra.

All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ι (timeOrderF a) = 0⊢ p 0 ⋯ All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ι (timeOrderF a) = 0⊢ ∀ (x y : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)) (hy : y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)), p x hx → p y hy → p (x + y) ⋯ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ι (timeOrderF a) = 0x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)hy:y ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)h1:p x hxh2:p y hy⊢ p (x + y) ⋯ All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ι (timeOrderF a) = 0⊢ ∀ (x : 𝓕.FieldOpFreeAlgebra) (hx : x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)), p x hx → p (-x) ⋯ 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrah:a ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)p:{k : Set 𝓕.FieldOpFreeAlgebra} → (a : 𝓕.FieldOpFreeAlgebra) → a ∈ AddSubgroup.closure k → Prop := fun {k} a h => ι (timeOrderF a) = 0x:𝓕.FieldOpFreeAlgebrahx:x ∈ AddSubgroup.closure (Set.univ * 𝓕.fieldOpIdealSet * Set.univ)⊢ p x hx → p (-x) ⋯ All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:a ≈ b⊢ ι (timeOrderF (a - b)) = 0 All goals completed! 🐙@[inherit_doc timeOrder] scoped[FieldSpecification.WickAlgebra] notation "𝓣(" a ")" => timeOrder a

Properties of time ordering

lemma timeOrder_eq_ι_timeOrderF (a : 𝓕.FieldOpFreeAlgebra) : 𝓣(ι a) = ι 𝓣ᶠ(a) := rflAll goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ofFieldOpF ψ * ofFieldOpF φ) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ι (ofFieldOpF ψ) * ι (ofFieldOpF φ) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • ι (timeOrderF (ofFieldOpF ψ * ofFieldOpF φ)) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) • timeOrder (ι (ofFieldOpF ψ) * ι (ofFieldOpF φ)) All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙

For a field specification 𝓕, the time order operator acting on a list of 𝓕.FieldOp, 𝓣(φ₀…φₙ), is equal to 𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ) where φᵢ is the maximal time field operator in φ₀…φₙ.

The proof of this result ultimately relies on basic properties of ordering and signs.

𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) • ofFieldOpF (maxTimeField φ φs) * timeOrderF (ofFieldOpListF (eraseMaxTimeField φ φs))) = (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField φ φs).get {x | (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs}) • ofFieldOp (maxTimeField φ φs) * timeOrder (ofFieldOpList (eraseMaxTimeField φ φs)) All goals completed! 🐙
𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * timeOrderF (a * b)) = ι ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ)) * timeOrder (ι a * ι b) All goals completed! 🐙lemma timeOrder_superCommute_eq_time_left {φ ψ : 𝓕.CrAnFieldOp} (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (b : 𝓕.WickAlgebra) : 𝓣([ofCrAnOp φ, ofCrAnOp ψ]ₛ * b) = [ofCrAnOp φ, ofCrAnOp ψ]ₛ * 𝓣(b) := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:crAnTimeOrderRel φ ψhψφ:crAnTimeOrderRel ψ φb:𝓕.WickAlgebra⊢ timeOrder ((superCommute (ofCrAnOp φ)) (ofCrAnOp ψ) * b) = (superCommute (ofCrAnOp φ)) (ofCrAnOp ψ) * timeOrder b All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOphφψ:¬(crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)⊢ ι (timeOrderF ((superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ))) = 0 All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOphφψ:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)⊢ timeOrder ((superCommute (anPart φ)) (∑ i, ofCrAnOp ⟨ψ, i⟩)) = 0 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOphφψ:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)⊢ ∑ x, timeOrder ((superCommute (anPart φ)) (ofCrAnOp ⟨ψ, x⟩)) = 0 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOphφψ:¬(timeOrderRel φ ψ ∧ timeOrderRel ψ φ)a:𝓕.fieldOpToCrAnType ψha:a ∈ Finset.univ⊢ timeOrder ((superCommute (anPart φ)) (ofCrAnOp ⟨ψ, a⟩)) = 0 match φ with 𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.fieldOpToCrAnType ψha:a ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumhφψ:¬(timeOrderRel (FieldOp.inAsymp φ) ψ ∧ timeOrderRel ψ (FieldOp.inAsymp φ))⊢ timeOrder ((superCommute (anPart (FieldOp.inAsymp φ))) (ofCrAnOp ⟨ψ, a⟩)) = 0 All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.fieldOpToCrAnType ψha:a ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumhφψ:¬(timeOrderRel (FieldOp.outAsymp φ) ψ ∧ timeOrderRel ψ (FieldOp.outAsymp φ))⊢ timeOrder ((superCommute (anPart (FieldOp.outAsymp φ))) (ofCrAnOp ⟨ψ, a⟩)) = 0𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.fieldOpToCrAnType ψha:a ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimehφψ:¬(timeOrderRel (FieldOp.position φ) ψ ∧ timeOrderRel ψ (FieldOp.position φ))⊢ timeOrder ((superCommute (anPart (FieldOp.position φ))) (ofCrAnOp ⟨ψ, a⟩)) = 0 𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.fieldOpToCrAnType ψha:a ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumhφψ:¬(timeOrderRel (FieldOp.outAsymp φ) ψ ∧ timeOrderRel ψ (FieldOp.outAsymp φ))⊢ timeOrder ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofCrAnOp ⟨ψ, a⟩)) = 0 𝓕:FieldSpecificationφ✝:𝓕.FieldOpψ:𝓕.FieldOpa:𝓕.fieldOpToCrAnType ψha:a ∈ Finset.univφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumhφψ:¬(timeOrderRel (FieldOp.outAsymp φ) ψ ∧ timeOrderRel ψ (FieldOp.outAsymp φ))⊢ ¬(crAnTimeOrderRel ⟨FieldOp.outAsymp φ, ()⟩ ⟨ψ, a⟩ ∧ crAnTimeOrderRel ⟨ψ, a⟩ ⟨FieldOp.outAsymp φ, ()⟩) All goals completed! 🐙

For a field specification 𝓕, and a, b, c in 𝓕.WickAlgebra, then 𝓣(a * b * c) = 𝓣(a * 𝓣(b) * c).

All goals completed! 🐙
lemma timeOrder_timeOrder_left (b c : 𝓕.WickAlgebra) : 𝓣(b * c) = 𝓣(𝓣(b) * c) := 𝓕:FieldSpecificationb:𝓕.WickAlgebrac:𝓕.WickAlgebra⊢ timeOrder (b * c) = timeOrder (timeOrder b * c) All goals completed! 🐙lemma timeOrder_timeOrder_right (a b : 𝓕.WickAlgebra) : 𝓣(a * b) = 𝓣(a * 𝓣(b)) := 𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ timeOrder (a * b) = timeOrder (a * timeOrder b) All goals completed! 🐙

Time ordering is a projection.

lemma timeOrder_timeOrder (a : 𝓕.WickAlgebra) : 𝓣(𝓣(a)) = 𝓣(a) := 𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ timeOrder (timeOrder a) = timeOrder a All goals completed! 🐙