From 7fbf2284683d02beeb56fd76bdbdb9432ce5bb3e Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 23 Jan 2025 14:18:02 +0000 Subject: [PATCH] feat: Wick contraction docs --- .../ProtoOperatorAlgebra/NormalOrder.lean | 9 ++ .../Algebras/StateAlgebra/TimeOrder.lean | 53 +++++++++++ .../FieldSpecification/Examples.lean | 13 ++- HepLean/PerturbationTheory/WicksTheorem.lean | 94 +++++++++---------- docs/CuratedNotes/PerturbationTheory.html | 3 +- scripts/MetaPrograms/notes.lean | 47 ++++++++-- 6 files changed, 154 insertions(+), 65 deletions(-) diff --git a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean index 87905b6..de00e2a 100644 --- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean @@ -356,6 +356,11 @@ noncomputable def contractStateAtIndex (Ο† : 𝓕.States) (Ο†s : List 𝓕.State | some n => 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› (Ο†s.take n)) β€’ π“ž.crAnF (⟨anPart (StateAlgebra.ofState Ο†), ofState Ο†s[n]βŸ©β‚›ca) +/-- +Within a proto-operator algebra, +`Ο† * N(φ₀φ₁…φₙ) = N(φφ₀φ₁…φₙ) + βˆ‘ i, (sα΅’ β€’ [anPart Ο†, Ο†α΅’]β‚›) * N(Ο†β‚€Ο†β‚β€¦Ο†α΅’β‚‹β‚Ο†α΅’β‚Šβ‚β€¦Ο†β‚™)`, +where `sβ‚™` is the exchange sign for `Ο†` and `φ₀φ₁…φᡒ₋₁`. +-/ lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : π“ž.crAnF (ofState Ο† * normalOrder (ofStateList Ο†s)) = @@ -374,6 +379,10 @@ lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (Ο† : 𝓕.States) -/ +/-- +Within a proto-operator algebra, `N(φφ₀φ₁…φₙ) = s β€’ N(φ₀…φₖ₋₁φφₖ…φₙ)`, where +`s` is the exchange sign for `Ο†` and `φ₀…φₖ₋₁`. +-/ lemma crAnF_ofState_normalOrder_insert (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (k : Fin Ο†s.length.succ) : π“ž.crAnF (normalOrder (ofStateList (Ο† :: Ο†s))) = diff --git a/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean index 07740e3..7f349fb 100644 --- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean @@ -18,6 +18,7 @@ noncomputable section namespace StateAlgebra open FieldStatistic +open HepLean.List /-- The linear map on the free state algebra defined as the map taking a list of states to the time-ordered list of states multiplied by @@ -64,6 +65,8 @@ lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {Ο† ψ : 𝓕.States} ( have hx := IsTotal.total (r := timeOrderRel) ψ Ο† simp_all +/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * Ο†α΅’ * T(Ο†β‚€Ο†β‚β€¦Ο†α΅’β‚‹β‚Ο†α΅’β‚Šβ‚β€¦Ο†β‚™)` where `Ο†α΅’` is the state + which has maximum time and `s` is the exchange sign of `Ο†α΅’` and `φ₀φ₁…φᡒ₋₁`. -/ lemma timeOrder_eq_maxTimeField_mul (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : timeOrder (ofList (Ο† :: Ο†s)) = 𝓒(𝓕 |>β‚› maxTimeField Ο† Ο†s, 𝓕 |>β‚› (Ο† :: Ο†s).take (maxTimeFieldPos Ο† Ο†s)) β€’ @@ -75,6 +78,56 @@ lemma timeOrder_eq_maxTimeField_mul (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) rw [timerOrderSign_of_eraseMaxTimeField, mul_assoc] simp +/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * Ο†α΅’ * T(Ο†β‚€Ο†β‚β€¦Ο†α΅’β‚‹β‚Ο†α΅’β‚Šβ‚β€¦Ο†β‚™)` where `Ο†α΅’` is the state + which has maximum time and `s` is the exchange sign of `Ο†α΅’` and `φ₀φ₁…φᡒ₋₁`. + Here `s` is written using finite sets. -/ +lemma timeOrder_eq_maxTimeField_mul_finset (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : + timeOrder (ofList (Ο† :: Ο†s)) = 𝓒(𝓕 |>β‚› maxTimeField Ο† Ο†s, 𝓕 |>β‚› ⟨(eraseMaxTimeField Ο† Ο†s).get, + (Finset.filter (fun x => + (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) Finset.univ)⟩) β€’ + StateAlgebra.ofState (maxTimeField Ο† Ο†s) * timeOrder (ofList (eraseMaxTimeField Ο† Ο†s)) := by + rw [timeOrder_eq_maxTimeField_mul] + congr 3 + apply FieldStatistic.ofList_perm + nth_rewrite 1 [← List.finRange_map_get (Ο† :: Ο†s)] + simp only [List.length_cons, eraseMaxTimeField, insertionSortDropMinPos] + rw [eraseIdx_get, ← List.map_take, ← List.map_map] + refine List.Perm.map (Ο† :: Ο†s).get ?_ + apply (List.perm_ext_iff_of_nodup _ _).mpr + Β· intro i + simp only [List.length_cons, maxTimeFieldPos, mem_take_finrange, Fin.val_fin_lt, List.mem_map, + Finset.mem_sort, Finset.mem_filter, Finset.mem_univ, true_and, Function.comp_apply] + refine Iff.intro (fun hi => ?_) (fun h => ?_) + Β· have h2 := (maxTimeFieldPosFin Ο† Ο†s).2 + simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one, + maxTimeFieldPosFin, insertionSortMinPosFin] at h2 + use ⟨i, by omega⟩ + apply And.intro + Β· simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, maxTimeFieldPosFin, + insertionSortMinPosFin, Nat.succ_eq_add_one, Fin.mk_lt_mk, Fin.val_fin_lt, Fin.succ_mk] + rw [Fin.lt_def] + split + Β· simp only [Fin.val_fin_lt] + omega + Β· omega + Β· simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, Fin.succ_mk, Fin.ext_iff, + Fin.coe_cast] + split + Β· simp + Β· simp_all [Fin.lt_def] + Β· obtain ⟨j, h1, h2⟩ := h + subst h2 + simp only [Fin.lt_def, Fin.coe_cast] + exact h1 + Β· exact List.Sublist.nodup (List.take_sublist _ _) <| + List.nodup_finRange (Ο†s.length + 1) + Β· refine List.Nodup.map ?_ ?_ + Β· refine Function.Injective.comp ?hf.hg Fin.succAbove_right_injective + exact Fin.cast_injective (eraseIdx_length (Ο† :: Ο†s) (insertionSortMinPos timeOrderRel Ο† Ο†s)) + Β· exact Finset.sort_nodup (fun x1 x2 => x1 ≀ x2) + (Finset.filter (fun x => (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) + Finset.univ) + end StateAlgebra end end FieldSpecification diff --git a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean index c93cbbb..c1461dc 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean @@ -13,18 +13,23 @@ import HepLean.PerturbationTheory.FieldSpecification.Basic namespace FieldSpecification variable (𝓕 : FieldSpecification) -/-- The Field specification corresponding to a single bosonic field. -/ +/-- The Field specification corresponding to a single bosonic field. + The type of fields is the unit type, and the statistic of the unique element of the unit + type is bosonic. -/ def singleBoson : FieldSpecification where Fields := Unit statistics := fun _ => FieldStatistic.bosonic -/-- The Field specification corresponding to a single fermionic field. -/ +/-- The Field specification corresponding to a single fermionic field. + The type of fields is the unit type, and the statistic of the unique element of the unit + type is fermionic. -/ def singleFermion : FieldSpecification where Fields := Unit statistics := fun _ => FieldStatistic.fermionic -/-- The Field specification corresponding to a two bosonic field and - two fermionic fields. -/ +/-- The Field specification corresponding to two bosonic fields and two fermionic fields. + The type of fields is `Fin 2 βŠ• Fin 2`, and the statistic of the two `.inl` (left) elements + is bosonic and the statistic of the two `.inr` (right) elements is fermionic. -/ def doubleBosonDoubleFermion : FieldSpecification where Fields := Fin 2 βŠ• Fin 2 statistics := fun b => diff --git a/HepLean/PerturbationTheory/WicksTheorem.lean b/HepLean/PerturbationTheory/WicksTheorem.lean index 9f3f786..e02512f 100644 --- a/HepLean/PerturbationTheory/WicksTheorem.lean +++ b/HepLean/PerturbationTheory/WicksTheorem.lean @@ -25,6 +25,11 @@ open HepLean.List open WickContraction open FieldStatistic +/-- +Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. +We have (roughly) `N(c.insertList Ο† Ο†s i none).uncontractedList = s β€’ N(Ο† * c.uncontractedList)` +Where `s` is the exchange sign for `Ο†` and the uncontracted fields in `φ₀φ₁…φᡒ`. +-/ lemma insertList_none_normalOrder (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (c : WickContraction Ο†s.length) : π“ž.crAnF (normalOrder (ofStateList (List.map (Ο†s.insertIdx i Ο†).get @@ -91,6 +96,12 @@ lemma insertList_none_normalOrder (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) simp only [Nat.succ_eq_add_one] rw [insertList_uncontractedList_none_map] +/-- +Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. +We have (roughly) `N(c.insertList Ο† Ο†s i k).uncontractedList` +is equal to `N((c.uncontractedList).eraseIdx k')` +where `k'` is the position in `c.uncontractedList` corresponding to `k`. +-/ lemma insertList_some_normalOrder (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (c : WickContraction Ο†s.length) (k : c.uncontracted) : π“ž.crAnF (normalOrder (ofStateList (List.map (Ο†s.insertIdx i Ο†).get @@ -107,6 +118,12 @@ lemma insertList_some_normalOrder (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) congr conv_rhs => rw [get_eq_insertIdx_succAbove Ο† Ο†s i] +/-- +Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. +This lemma states that `(c.sign β€’ c.timeContract π“ž) * N(c.uncontracted)` +for `c` equal to `c.insertList Ο† Ο†s i none` is equal to that for just `c` +mulitiplied by the exchange sign of `Ο†` and `φ₀φ₁…φᡒ₋₁`. +-/ lemma sign_timeContract_normalOrder_insertList_none (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (c : WickContraction Ο†s.length) : (c.insertList Ο† Ο†s i none).sign β€’ (c.insertList Ο† Ο†s i none).timeContract π“ž @@ -150,6 +167,13 @@ lemma sign_timeContract_normalOrder_insertList_none (Ο† : 𝓕.States) (Ο†s : Li simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero] exact hg +/-- +Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. +This lemma states that +`(c.sign β€’ c.timeContract π“ž) * N(c.uncontracted)` +for `c` equal to `c.insertList Ο† Ο†s i (some k)` is equal to that for just `c` +mulitiplied by the exchange sign of `Ο†` and `φ₀φ₁…φᡒ₋₁`. +-/ lemma sign_timeContract_normalOrder_insertList_some (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (c : WickContraction Ο†s.length) (k : c.uncontracted) (hlt : βˆ€ (k : Fin Ο†s.length), timeOrderRel Ο† Ο†s[k]) @@ -214,6 +238,15 @@ lemma sign_timeContract_normalOrder_insertList_some (Ο† : 𝓕.States) (Ο†s : Li zero_mul, instCommGroup.eq_1] exact hg' +/-- +Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. +This lemma states that +`(c.sign β€’ c.timeContract π“ž) * N(c.uncontracted)` +is equal to the sum of +`(c'.sign β€’ c'.timeContract π“ž) * N(c'.uncontracted)` +for all `c' = (c.insertList Ο† Ο†s i k)` for `k : Option (c.uncontracted)`, multiplied by +the exchange sign of `Ο†` and `φ₀φ₁…φᡒ₋₁`. +-/ lemma mul_sum_contractions (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (c : WickContraction Ο†s.length) (hlt : βˆ€ (k : Fin Ο†s.length), timeOrderRel Ο† Ο†s[k]) (hn : βˆ€ (k : Fin Ο†s.length), i.succAbove k < i β†’ Β¬timeOrderRel Ο†s[k] Ο†) : @@ -226,8 +259,7 @@ lemma mul_sum_contractions (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin (ofStateList ((c.insertList Ο† Ο†s i k).uncontractedList.map (Ο†s.insertIdx i Ο†).get)))) := by rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, Finset.mul_sum, uncontractedStatesEquiv_list_sum, Finset.smul_sum] - simp only [Finset.univ_eq_attach, instCommGroup.eq_1, - Nat.succ_eq_add_one, timeContract_insertList_none] + simp only [instCommGroup.eq_1, Nat.succ_eq_add_one] congr 1 funext n match n with @@ -261,54 +293,6 @@ lemma wicks_theorem_congr {Ο†s Ο†s' : List 𝓕.States} (h : Ο†s = Ο†s') : subst h simp -lemma timeOrder_eq_maxTimeField_mul_finset (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) : - timeOrder (ofList (Ο† :: Ο†s)) = 𝓒(𝓕 |>β‚› maxTimeField Ο† Ο†s, 𝓕 |>β‚› ⟨(eraseMaxTimeField Ο† Ο†s).get, - (Finset.filter (fun x => - (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) Finset.univ)⟩) β€’ - StateAlgebra.ofState (maxTimeField Ο† Ο†s) * timeOrder (ofList (eraseMaxTimeField Ο† Ο†s)) := by - rw [timeOrder_eq_maxTimeField_mul] - congr 3 - apply FieldStatistic.ofList_perm - nth_rewrite 1 [← List.finRange_map_get (Ο† :: Ο†s)] - simp only [List.length_cons, eraseMaxTimeField, insertionSortDropMinPos] - rw [eraseIdx_get, ← List.map_take, ← List.map_map] - refine List.Perm.map (Ο† :: Ο†s).get ?_ - apply (List.perm_ext_iff_of_nodup _ _).mpr - Β· intro i - simp only [List.length_cons, maxTimeFieldPos, mem_take_finrange, Fin.val_fin_lt, List.mem_map, - Finset.mem_sort, Finset.mem_filter, Finset.mem_univ, true_and, Function.comp_apply] - refine Iff.intro (fun hi => ?_) (fun h => ?_) - Β· have h2 := (maxTimeFieldPosFin Ο† Ο†s).2 - simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one, - maxTimeFieldPosFin, insertionSortMinPosFin] at h2 - use ⟨i, by omega⟩ - apply And.intro - Β· simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, maxTimeFieldPosFin, - insertionSortMinPosFin, Nat.succ_eq_add_one, Fin.mk_lt_mk, Fin.val_fin_lt, Fin.succ_mk] - rw [Fin.lt_def] - split - Β· simp only [Fin.val_fin_lt] - omega - Β· omega - Β· simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, Fin.succ_mk, Fin.ext_iff, - Fin.coe_cast] - split - Β· simp - Β· simp_all [Fin.lt_def] - Β· obtain ⟨j, h1, h2⟩ := h - subst h2 - simp only [Fin.lt_def, Fin.coe_cast] - exact h1 - Β· exact List.Sublist.nodup (List.take_sublist _ _) <| - List.nodup_finRange (Ο†s.length + 1) - Β· refine List.Nodup.map ?_ ?_ - Β· refine Function.Injective.comp ?hf.hg Fin.succAbove_right_injective - exact Fin.cast_injective (eraseIdx_length (Ο† :: Ο†s) (insertionSortMinPos timeOrderRel Ο† Ο†s)) - Β· exact Finset.sort_nodup (fun x1 x2 => x1 ≀ x2) - (Finset.filter (fun x => (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) - Finset.univ) - - /-! ## Wick's theorem @@ -335,7 +319,15 @@ remark wicks_theorem_context := " the remaining fields. Wick's theorem is also the precursor to the diagrammatic approach to quantum field theory called Feynman diagrams." -/-- Wick's theorem for time-ordered products of bosonic and fermionic fields. -/ +/-- Wick's theorem for time-ordered products of bosonic and fermionic fields. + The time ordered product `T(φ₀φ₁…φₙ)` is equal to the sum of terms, + for all possible Wick contractions `c` of the list of fields `Ο†s := φ₀φ₁…φₙ`, given by + the multiple of: +- The sign corresponding to the number of fermionic-fermionic exchanges one must do + to put elements in contracted pairs of `c` next to each other. +- The product of time-contractions of the contracted pairs of `c`. +- The normal-ordering of the uncontracted fields in `c`. +-/ theorem wicks_theorem : (Ο†s : List 𝓕.States) β†’ π“ž.crAnF (ofStateAlgebra (timeOrder (ofList Ο†s))) = βˆ‘ (c : WickContraction Ο†s.length), (c.sign Ο†s β€’ c.timeContract π“ž) * π“ž.crAnF (normalOrder (ofStateList (c.uncontractedList.map Ο†s.get))) diff --git a/docs/CuratedNotes/PerturbationTheory.html b/docs/CuratedNotes/PerturbationTheory.html index 8f65dad..1089d6e 100644 --- a/docs/CuratedNotes/PerturbationTheory.html +++ b/docs/CuratedNotes/PerturbationTheory.html @@ -54,12 +54,13 @@ layout: default {% if entry.type == "name" %}
-

{{ entry.name }}: {{ entry.docString }}

+

{{ entry.name }}: {{ entry.docString | markdownify}}

Show Lean code: 
{{ entry.declString }}
+
{% endif %} {% if entry.type == "remark" %} diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 3b04336..eb9b3fc 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -39,14 +39,18 @@ def DeclInfo.ofName (n : Name) : MetaM DeclInfo := do declString := declString, docString := docString} -def DeclInfo.toYML (d : DeclInfo) : String := +def DeclInfo.toYML (d : DeclInfo) : MetaM String := do let declStringIndent := d.declString.replace "\n" "\n " - s!" + let docStringIndent := d.docString.replace "\n" "\n " + let link ← Name.toGitHubLink d.fileName d.line + return s!" - type: name name: {d.name} line: {d.line} fileName: {d.fileName} - docString: \"{d.docString}\" + link: \"{link}\" + docString: | + {docStringIndent} declString: | {declStringIndent}" @@ -82,7 +86,7 @@ def NotePart.toYMLM : ((List String) Γ— Nat Γ— Nat) β†’ NotePart β†’ MetaM ((Li {contentIndent}" return ⟨x.1 ++ [newString], x.2⟩ | false => - let newString := (← DeclInfo.ofName n).toYML + let newString ← (← DeclInfo.ofName n).toYML return ⟨x.1 ++ [newString], x.2⟩ structure Note where @@ -126,15 +130,40 @@ def perturbationTheory : Note where .h2 "Field specifications", .name `fieldSpecification_intro, .name `FieldSpecification, + .p "Some examples of `FieldSpecification`s are given below:", + .name `FieldSpecification.singleBoson, + .name `FieldSpecification.singleFermion, + .name `FieldSpecification.doubleBosonDoubleFermion, .h2 "States", + .p "Given a field, there are three common states (or operators) of that field that we work with. + These are the in and out asymptotic states and the position states.", + .p "For a field structure `𝓕` these states are defined as:", + .name `FieldSpecification.IncomingAsymptotic, + .name `FieldSpecification.OutgoingAsymptotic, + .name `FieldSpecification.PositionStates, + .p "We will want to consider all three of these types of states simultanously so we define + and inductive type `States` which is the disjoint union of these three types of states.", + .name `FieldSpecification.States, + .name `FieldSpecification.StateAlgebra, .h2 "Time ordering", + .name `FieldSpecification.timeOrderRel, + .name `FieldSpecification.timeOrderSign, + .name `FieldSpecification.StateAlgebra.timeOrder, + .name `FieldSpecification.StateAlgebra.timeOrder_eq_maxTimeField_mul_finset, .h2 "Creation and annihilation states", .h2 "Normal ordering", - .h1 "Algebras", - .h2 "State free-algebra", - .h2 "CrAnState free-algebra", - .h2 "Proto operator algebra", - .h1 "Contractions" + .h2 "Proto-operator algebra", + .h1 "Wick Contractions", + .h1 "Proof of Wick's theorem", + .h2 "The case of the nil list", + .p "Our proof of Wick's theorem will be via induction on the number of fields that + are in the time-ordered product. The base case is when there are no files. + The proof of Wick's theorem follows from definitions and simple lemmas.", + .name `FieldSpecification.wicks_theorem_nil, + .name `FieldSpecification.ProtoOperatorAlgebra.crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, + .name `FieldSpecification.ProtoOperatorAlgebra.crAnF_ofState_normalOrder_insert, + .name `FieldSpecification.mul_sum_contractions, + .name `FieldSpecification.wicks_theorem, ] unsafe def main (_ : List String) : IO UInt32 := do