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

Normal Ordering on Field operator algebra

@[expose] public section

Normal order on super-commutators.

The main result of this is ฮน_normalOrderF_superCommuteF_eq_zero_mul which states that applying ฮน to the normal order of something containing a super-commutator is zero.

๐“•:FieldSpecificationฯ†a:๐“•.CrAnFieldOpฯ†a':๐“•.CrAnFieldOpฯ†s:List ๐“•.CrAnFieldOpฯ†s':List ๐“•.CrAnFieldOphฯ†a:๐“•|>แถœฯ†a = CreateAnnihilate.annihilatehฯ†a':๐“•|>แถœฯ†a' = CreateAnnihilate.annihilateโŠข normalOrderSign (ฯ†s ++ ฯ†a' :: ฯ†a :: ฯ†s') โ€ข (ฮน (ofCrAnListF (createFilter (ฯ†s ++ ฯ†s'))) * ฮน (ofCrAnListF (annihilateFilter ฯ†s)) * 0 * ฮน (ofCrAnListF (annihilateFilter ฯ†s'))) = 0 All goals completed! ๐Ÿ™๐“•:FieldSpecificationฯ†a:๐“•.CrAnFieldOpฯ†a':๐“•.CrAnFieldOpฯ†s:List ๐“•.CrAnFieldOpa:๐“•.FieldOpFreeAlgebrahf:ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap (ofCrAnListF ฯ†s * (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a')) = 0โŠข 0 a = 0 All goals completed! ๐Ÿ™๐“•:FieldSpecificationฯ†a:๐“•.CrAnFieldOpฯ†a':๐“•.CrAnFieldOpa:๐“•.FieldOpFreeAlgebrab:๐“•.FieldOpFreeAlgebrahf:ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip ((superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a') * b) = 0โŠข 0 a = 0 All goals completed! ๐Ÿ™All goals completed! ๐Ÿ™๐“•:FieldSpecificationฯ†a:๐“•.CrAnFieldOpฯ†s:List ๐“•.CrAnFieldOpa:๐“•.FieldOpFreeAlgebrab:๐“•.FieldOpFreeAlgebraโŠข -(exchangeSign (ofList ๐“•.crAnStatistics ฯ†s)) (๐“•.crAnStatistics ฯ†a) โ€ข 0 = 0 All goals completed! ๐Ÿ™All goals completed! ๐Ÿ™๐“•:FieldSpecificationฯ†s:List ๐“•.CrAnFieldOpa:๐“•.FieldOpFreeAlgebrab:๐“•.FieldOpFreeAlgebrac:๐“•.FieldOpFreeAlgebrahf:ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF (ofCrAnListF ฯ†s) = 0โŠข 0 c = 0 All goals completed! ๐Ÿ™๐“•:FieldSpecificationa:๐“•.FieldOpFreeAlgebrab:๐“•.FieldOpFreeAlgebrac:๐“•.FieldOpFreeAlgebrad:๐“•.FieldOpFreeAlgebrahf:ฮน.toLinearMap โˆ˜โ‚— normalOrderF โˆ˜โ‚— mulLinearMap.flip b โˆ˜โ‚— mulLinearMap a โˆ˜โ‚— superCommuteF.flip c = 0โŠข 0 d = 0 All goals completed! ๐Ÿ™๐“•:FieldSpecificationb:๐“•.FieldOpFreeAlgebrac:๐“•.FieldOpFreeAlgebrad:๐“•.FieldOpFreeAlgebraโŠข ฮน (normalOrderF ((superCommuteF d) c * b)) = ฮน (normalOrderF (1 * (superCommuteF d) c * b)) All goals completed! ๐Ÿ™๐“•:FieldSpecificationa:๐“•.FieldOpFreeAlgebrac:๐“•.FieldOpFreeAlgebrad:๐“•.FieldOpFreeAlgebraโŠข ฮน (normalOrderF (a * (superCommuteF d) c)) = ฮน (normalOrderF (a * (superCommuteF d) c * 1)) All goals completed! ๐Ÿ™๐“•:FieldSpecificationa:๐“•.FieldOpFreeAlgebrab1:๐“•.FieldOpFreeAlgebrab2:๐“•.FieldOpFreeAlgebrac:๐“•.FieldOpFreeAlgebrad:๐“•.FieldOpFreeAlgebraโŠข ฮน (normalOrderF (a * (superCommuteF d) c * b1 * b2)) = ฮน (normalOrderF (a * (superCommuteF d) c * (b1 * b2))) ๐“•:FieldSpecificationa:๐“•.FieldOpFreeAlgebrab1:๐“•.FieldOpFreeAlgebrab2:๐“•.FieldOpFreeAlgebrac:๐“•.FieldOpFreeAlgebrad:๐“•.FieldOpFreeAlgebraโŠข a * (superCommuteF d) c * b1 * b2 = a * (superCommuteF d) c * (b1 * b2) All goals completed! ๐Ÿ™๐“•:FieldSpecificationc:๐“•.FieldOpFreeAlgebrad:๐“•.FieldOpFreeAlgebraโŠข ฮน (normalOrderF ((superCommuteF d) c)) = ฮน (normalOrderF (1 * (superCommuteF d) c * 1)) All goals completed! ๐Ÿ™

Defining normal order for FiedOpAlgebra.

๐“•:FieldSpecificationa:๐“•.FieldOpFreeAlgebrah:a โˆˆ AddSubgroup.closure (Set.univ * ๐“•.fieldOpIdealSet * Set.univ)โŠข ฮน (normalOrderF a) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0โŠข ฮน (normalOrderF a) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0โŠข p a h ๐“•: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 => ฮน (normalOrderF a) = 0โŠข โˆ€ (x : ๐“•.FieldOpFreeAlgebra) (hx : x โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univ), 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 => ฮน (normalOrderF a) = 0โŠข p 0 โ‹ฏ๐“•: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 => ฮน (normalOrderF 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 => ฮน (normalOrderF 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 => ฮน (normalOrderF a) = 0โŠข โˆ€ (x : ๐“•.FieldOpFreeAlgebra) (hx : x โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univ), 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 => ฮน (normalOrderF a) = 0x:๐“•.FieldOpFreeAlgebrahx:x โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univโŠข 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 => ฮน (normalOrderF a) = 0a:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univ * ๐“•.fieldOpIdealSetb:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univhx:a * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univโŠข p (a * b) โ‹ฏ ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univc:๐“•.FieldOpFreeAlgebrahc:c โˆˆ ๐“•.fieldOpIdealSethx:(fun x1 x2 => x1 * x2) a c * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univโŠข p ((fun x1 x2 => x1 * x2) a c * b) โ‹ฏ ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univc:๐“•.FieldOpFreeAlgebrahc:c โˆˆ ๐“•.fieldOpIdealSethx:(fun x1 x2 => x1 * x2) a c * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univโŠข ฮน (normalOrderF (a * c * b)) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univc:๐“•.FieldOpFreeAlgebrahx:(fun x1 x2 => x1 * x2) a c * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhc:(โˆƒ ฯ†1 ฯ†2 ฯ†3, c = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง c = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a, ๐“•|>แถœฯ†a = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง c = (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง c = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')โŠข ฮน (normalOrderF (a * c * b)) = 0 match hc with ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univc:๐“•.FieldOpFreeAlgebrahx:(fun x1 x2 => x1 * x2) a c * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhcโœ:(โˆƒ ฯ†1 ฯ†2 ฯ†3, c = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง c = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a, ๐“•|>แถœฯ†a = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง c = (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง c = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')hc:โˆƒ ฯ†1 ฯ†2 ฯ†3, c = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))โŠข ฮน (normalOrderF (a * c * b)) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univฯ†a:๐“•.CrAnFieldOpฯ†a':๐“•.CrAnFieldOphฯ†a:๐“•.CrAnFieldOphx:(fun x1 x2 => x1 * x2) a ((superCommuteF (ofCrAnOpF ฯ†a)) ((superCommuteF (ofCrAnOpF ฯ†a')) (ofCrAnOpF hฯ†a))) * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhc:(โˆƒ ฯ†1 ฯ†2 ฯ†3, (superCommuteF (ofCrAnOpF ฯ†a)) ((superCommuteF (ofCrAnOpF ฯ†a')) (ofCrAnOpF hฯ†a)) = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง (superCommuteF (ofCrAnOpF ฯ†a)) ((superCommuteF (ofCrAnOpF ฯ†a')) (ofCrAnOpF hฯ†a)) = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a_1, ๐“•|>แถœฯ†a_1 = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง (superCommuteF (ofCrAnOpF ฯ†a)) ((superCommuteF (ofCrAnOpF ฯ†a')) (ofCrAnOpF hฯ†a)) = (superCommuteF (ofCrAnOpF ฯ†a_1)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง (superCommuteF (ofCrAnOpF ฯ†a)) ((superCommuteF (ofCrAnOpF ฯ†a')) (ofCrAnOpF hฯ†a)) = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')โŠข ฮน (normalOrderF (a * (superCommuteF (ofCrAnOpF ฯ†a)) ((superCommuteF (ofCrAnOpF ฯ†a')) (ofCrAnOpF hฯ†a)) * b)) = 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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univc:๐“•.FieldOpFreeAlgebrahx:(fun x1 x2 => x1 * x2) a c * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhcโœ:(โˆƒ ฯ†1 ฯ†2 ฯ†3, c = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง c = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a, ๐“•|>แถœฯ†a = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง c = (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง c = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')hc:โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง c = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)โŠข ฮน (normalOrderF (a * c * b)) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univฯ†a:๐“•.CrAnFieldOpฯ†a':๐“•|>แถœฯ†a = CreateAnnihilate.createhฯ†a:๐“•.CrAnFieldOphฯ†a':๐“•|>แถœhฯ†a = CreateAnnihilate.createhx:(fun x1 x2 => x1 * x2) a ((superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a)) * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhc:(โˆƒ ฯ†1 ฯ†2 ฯ†3, (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a_1, ๐“•|>แถœฯ†a_1 = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†a_1)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')โŠข ฮน (normalOrderF (a * (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) * b)) = 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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univc:๐“•.FieldOpFreeAlgebrahx:(fun x1 x2 => x1 * x2) a c * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhcโœ:(โˆƒ ฯ†1 ฯ†2 ฯ†3, c = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง c = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a, ๐“•|>แถœฯ†a = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง c = (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง c = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')hc:โˆƒ ฯ†a, ๐“•|>แถœฯ†a = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง c = (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF x)โŠข ฮน (normalOrderF (a * c * b)) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univฯ†a:๐“•.CrAnFieldOpฯ†a':๐“•|>แถœฯ†a = CreateAnnihilate.annihilatehฯ†a:๐“•.CrAnFieldOphฯ†a':๐“•|>แถœhฯ†a = CreateAnnihilate.annihilatehx:(fun x1 x2 => x1 * x2) a ((superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a)) * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhc:(โˆƒ ฯ†1 ฯ†2 ฯ†3, (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a_1, ๐“•|>แถœฯ†a_1 = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†a_1)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')โŠข ฮน (normalOrderF (a * (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF hฯ†a) * b)) = 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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univc:๐“•.FieldOpFreeAlgebrahx:(fun x1 x2 => x1 * x2) a c * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhcโœ:(โˆƒ ฯ†1 ฯ†2 ฯ†3, c = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง c = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a, ๐“•|>แถœฯ†a = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง c = (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง c = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')hc:โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง c = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')โŠข ฮน (normalOrderF (a * c * b)) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0b:๐“•.FieldOpFreeAlgebrahb:b โˆˆ Set.univa:๐“•.FieldOpFreeAlgebraha:a โˆˆ Set.univฯ†a:๐“•.CrAnFieldOpฯ†a':๐“•.CrAnFieldOphฯ†a:ยฌ๐“•.crAnStatistics ฯ†a = ๐“•.crAnStatistics ฯ†a'hx:(fun x1 x2 => x1 * x2) a ((superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a')) * b โˆˆ Set.univ * ๐“•.fieldOpIdealSet * Set.univhc:(โˆƒ ฯ†1 ฯ†2 ฯ†3, (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a') = (superCommuteF (ofCrAnOpF ฯ†1)) ((superCommuteF (ofCrAnOpF ฯ†2)) (ofCrAnOpF ฯ†3))) โˆจ (โˆƒ ฯ†c, ๐“•|>แถœฯ†c = CreateAnnihilate.create โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.create โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a') = (superCommuteF (ofCrAnOpF ฯ†c)) (ofCrAnOpF x)) โˆจ (โˆƒ ฯ†a_1, ๐“•|>แถœฯ†a_1 = CreateAnnihilate.annihilate โˆง โˆƒ x, ๐“•|>แถœx = CreateAnnihilate.annihilate โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a') = (superCommuteF (ofCrAnOpF ฯ†a_1)) (ofCrAnOpF x)) โˆจ โˆƒ ฯ† ฯ†', ยฌ๐“•.crAnStatistics ฯ† = ๐“•.crAnStatistics ฯ†' โˆง (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a') = (superCommuteF (ofCrAnOpF ฯ†)) (ofCrAnOpF ฯ†')โŠข ฮน (normalOrderF (a * (superCommuteF (ofCrAnOpF ฯ†a)) (ofCrAnOpF ฯ†a') * b)) = 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 => ฮน (normalOrderF 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 => ฮน (normalOrderF 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 => ฮน (normalOrderF a) = 0x:๐“•.FieldOpFreeAlgebray:๐“•.FieldOpFreeAlgebrahx: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 => ฮน (normalOrderF a) = 0x:๐“•.FieldOpFreeAlgebray:๐“•.FieldOpFreeAlgebrahx:x โˆˆ AddSubgroup.closure (Set.univ * ๐“•.fieldOpIdealSet * Set.univ)hy:y โˆˆ AddSubgroup.closure (Set.univ * ๐“•.fieldOpIdealSet * Set.univ)โŠข ฮน (normalOrderF x) = 0 โ†’ ฮน (normalOrderF y) = 0 โ†’ ฮน (normalOrderF x) + ฮน (normalOrderF y) = 0 ๐“•: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 => ฮน (normalOrderF a) = 0x:๐“•.FieldOpFreeAlgebray:๐“•.FieldOpFreeAlgebrahx:x โˆˆ AddSubgroup.closure (Set.univ * ๐“•.fieldOpIdealSet * Set.univ)hy:y โˆˆ AddSubgroup.closure (Set.univ * ๐“•.fieldOpIdealSet * Set.univ)h1:ฮน (normalOrderF x) = 0h2:ฮน (normalOrderF y) = 0โŠข ฮน (normalOrderF x) + ฮน (normalOrderF y) = 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 => ฮน (normalOrderF 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 => ฮน (normalOrderF a) = 0x:๐“•.FieldOpFreeAlgebrahx:x โˆˆ AddSubgroup.closure (Set.univ * ๐“•.fieldOpIdealSet * Set.univ)โŠข p x hx โ†’ p (-x) โ‹ฏ All goals completed! ๐Ÿ™๐“•:FieldSpecificationa:๐“•.FieldOpFreeAlgebrab:๐“•.FieldOpFreeAlgebrah:a - b โˆˆ TwoSidedIdeal.span ๐“•.fieldOpIdealSetโŠข ฮน (normalOrderF (a - b)) = 0 All goals completed! ๐Ÿ™@[inherit_doc normalOrder] scoped[FieldSpecification.WickAlgebra] notation "๐“(" a ")" => normalOrder a