From c9607c459f71be528cf35463d49a47013a33b0e3 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 7 Feb 2025 06:58:41 +0000 Subject: [PATCH] docs: Docs for Wick contractions --- .../FieldOpAlgebra/NormalOrder/Lemmas.lean | 5 ++- .../NormalOrder/WickContractions.lean | 22 +++++++----- .../WickContraction/Basic.lean | 22 +++++++++--- .../WickContraction/Card.lean | 6 ++-- .../WickContraction/InsertAndContract.lean | 20 ++++++----- .../WickContraction/Join.lean | 6 ++-- .../WickContraction/Sign/Basic.lean | 9 ++--- .../WickContraction/Sign/InsertNone.lean | 13 +++++-- .../WickContraction/Sign/InsertSome.lean | 29 ++++++++++----- .../WickContraction/Sign/Join.lean | 10 +++--- .../WickContraction/Uncontracted.lean | 3 +- .../WickContraction/UncontractedList.lean | 7 ++-- scripts/MetaPrograms/notes.lean | 35 ++++++++++--------- 13 files changed, 123 insertions(+), 64 deletions(-) diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean index f4042d8..29e2b61 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean @@ -118,6 +118,9 @@ lemma crPart_mul_normalOrder (φ : 𝓕.FieldOp) (a : 𝓕.FieldOpAlgebra) : -/ + +/-- For a field specfication `𝓕`, and `a` and `b` in `𝓕.FieldOpAlgebra` the normal ordering + of the super commutator of `a` and `b` vanishes. I.e. `𝓝([a,b]ₛ) = 0`. -/ @[simp] lemma normalOrder_superCommute_eq_zero (a b : 𝓕.FieldOpAlgebra) : 𝓝([a, b]ₛ) = 0 := by @@ -226,7 +229,7 @@ The proof of this result ultimetly goes as follows - The definition of `normalOrder` is used to rewrite `𝓝(φ₀…φₙ)` as a scalar multiple of a `ofCrAnList φsn` where `φsn` is the normal ordering of `φ₀…φₙ`. - `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ` - (considered as a list with one lement) with + (considered as a list with one element) with `ofCrAnList φsn` as a sum of supercommutors, one for each element of `φsn`. - The fact that super-commutors are in the center of `𝓕.FieldOpAlgebra` is used to rearange terms. - Properties of ordered lists, and `normalOrderSign_eraseIdx` is then used to complete the proof. diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean index 9777e88..01926f0 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean @@ -25,10 +25,14 @@ variable {𝓕 : FieldSpecification} -/ -/-- -Let `c` be a Wick Contraction for `φs := φ₀φ₁…φₙ`. -We have (roughly) `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)` -Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`. +/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of + `𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds + + `𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)` + + where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀…φᵢ₋₁`. + + The prove of this result ultimately a consequence of `normalOrder_superCommute_eq_zero`. -/ lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) : @@ -95,10 +99,12 @@ lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp rw [insertAndContract_uncontractedList_none_map] /-- -Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. -We have (roughly) `N(c ↩Λ φ i k).uncontractedList` -is equal to `N((c.uncontractedList).eraseIdx k')` -where `k'` is the position in `c.uncontractedList` corresponding to `k`. + For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of + `𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then + `𝓝([φsΛ ↩Λ φ i none]ᵘᶜ)` is equal to the normal ordering of `[φsΛ]ᵘᶜ` with the `FieldOp` + corresponding to `k` removed. + + The proof of this result ultimately a consequence of definitions. -/ lemma normalOrder_uncontracted_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) : diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean index e209148..308a9b1 100644 --- a/HepLean/PerturbationTheory/WickContraction/Basic.lean +++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean @@ -14,13 +14,18 @@ open FieldSpecification variable {𝓕 : FieldSpecification} /-- -Given a natural number `n` corresponding to the number of fields, a Wick contraction -is a finite set of pairs of `Fin n`, such that no element of `Fin n` occurs in more then one pair. +Given a natural number `n`, which will correspond to the number of fields needing +contracting, a Wick contraction +is a finite set of pairs of `Fin n` (numbers `0`, …, `n-1`), such that no +element of `Fin n` occurs in more then one pair. The pairs are the positions of fields we +'contract' together. + For example for `n = 3` there are `4` Wick contractions: - `∅`, corresponding to the case where no fields are contracted. - `{{0, 1}}`, corresponding to the case where the field at position `0` and `1` are contracted. - `{{0, 2}}`, corresponding to the case where the field at position `0` and `2` are contracted. - `{{1, 2}}`, corresponding to the case where the field at position `1` and `2` are contracted. + For `n=4` some possible Wick contractions are - `∅`, corresponding to the case where no fields are contracted. - `{{0, 1}, {2, 3}}`, corresponding to the case where the field at position `0` and `1` are @@ -37,6 +42,12 @@ namespace WickContraction variable {n : ℕ} (c : WickContraction n) open HepLean.List +remark contraction_notation := "Given a field specification `𝓕`, and a list `φs` + of `𝓕.FieldOp`, a Wick contraction of `φs` will mean a Wick contraction in + `WickContraction φs.length`. The notation `φsΛ` will be used for such contractions. + The terminology that `φsΛ` contracts pairs within of `φs` will also be used, even though + `φsΛ` is really contains positions of `φs`." + /-- Wick contractions are decidable. -/ instance : DecidableEq (WickContraction n) := Subtype.instDecidableEq @@ -520,8 +531,11 @@ lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1) rw [← (c.contractEquivFinTwo a).symm.prod_comp] simp [contractEquivFinTwo] -/-- A Wick contraction associated with a list of states is said to be `GradingCompliant` if in any - contracted pair of states they are either both fermionic or both bosonic. -/ +/-- For a field specification `𝓕`, `φs` a list of `𝓕.FieldOp` and a Wick contraction + `φsΛ` of `φs`, the Wick contraction `φsΛ` is said to be `GradingCompliant` if + for every pair in `φsΛ` the contracted fields are either both `fermionic` or both `bosonic`. + I.e. in a `GradingCompliant` Wick contraction no contractions occur between `fermionic` and + `bosonic` fields. -/ def GradingCompliant (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) := ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a]) diff --git a/HepLean/PerturbationTheory/WickContraction/Card.lean b/HepLean/PerturbationTheory/WickContraction/Card.lean index 275c361..9796036 100644 --- a/HepLean/PerturbationTheory/WickContraction/Card.lean +++ b/HepLean/PerturbationTheory/WickContraction/Card.lean @@ -236,9 +236,9 @@ def cardFun : ℕ → ℕ | 1 => 1 | Nat.succ (Nat.succ n) => cardFun (Nat.succ n) + (n + 1) * cardFun n -/-- The number of Wick contractions for `n : ℕ` fields, i.e. the cardinality of - `WickContraction n`, is equal to the terms in - Online Encyclopedia of Integer Sequences (OEIS) A000085. -/ +/-- The number of Wick contractions in `WickContraction n` is equal to the terms in + Online Encyclopedia of Integer Sequences (OEIS) A000085. That is: + 1, 1, 2, 4, 10, 26, 76, 232, 764, 2620, 9496, ... -/ theorem card_eq_cardFun : (n : ℕ) → Fintype.card (WickContraction n) = cardFun n | 0 => by decide | 1 => by decide diff --git a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean index 40851ba..a9bd3dd 100644 --- a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean +++ b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean @@ -24,15 +24,19 @@ open HepLean.Fin -/ -/-- Given a Wick contraction `φsΛ` associated to a list `φs`, - a position `i : Fin φs.lengthsucc`, an element `φ`, and an optional uncontracted element - `j : Option (φsΛ.uncontracted)` of `φsΛ`. - The Wick contraction `φsΛ.insertAndContract φ i j` is defined to be the Wick contraction - associated with `(φs.insertIdx i φ)` formed by 'inserting' `φ` into `φs` after the first `i` - elements and contracting `φ` optionally with `j`. +/-- Given a Wick contraction `φsΛ` for a list `φs` of `𝓕.FieldOp`, + a `𝓕.FieldOp` `φ`, an `i ≤ φs.length` and a `j` which is either `none` or + some element of `φsΛ.uncontracted`, the new Wick contraction + `φsΛ.insertAndContract φ i j` is defined by inserting `φ` into `φs` after + the first `i`-elements and moving the values representing the contracted pairs in `φsΛ` + accordingly. + If `j` is not `none`, but rather `some j`, to this contraction is added the contraction + of `φ` (at position `i`) with the new position of `j` after `φ` is added. - The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. Thus, - `φsΛ ↩Λ φ i none` indicates the case when we insert `φ` into `φs` but do not contract it. -/ + In other words, `φsΛ.insertAndContract φ i j` is formed by adding `φ` to `φs` at position `i`, + and contracting `φ` with the field orginally at position `j` if `j` is not none. + + The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. -/ def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) : WickContraction (φs.insertIdx i φ).length := diff --git a/HepLean/PerturbationTheory/WickContraction/Join.lean b/HepLean/PerturbationTheory/WickContraction/Join.lean index 67b8e5f..ec1754d 100644 --- a/HepLean/PerturbationTheory/WickContraction/Join.lean +++ b/HepLean/PerturbationTheory/WickContraction/Join.lean @@ -23,9 +23,9 @@ variable {n : ℕ} (c : WickContraction n) open HepLean.List open FieldOpAlgebra -/-- Given a Wick contraction `φsΛ` on `φs` and a Wick contraction `φsucΛ` on the uncontracted fields -within `φsΛ`, a Wick contraction on `φs`consisting of the contractins in `φsΛ` and -the contractions in `φsucΛ`. -/ +/-- Given a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs` and a Wick contraction + `φsucΛ` of `[φsΛ]ᵘᶜ`, `join φsΛ φsucΛ` is defined as the Wick contraction of `φs` consisting of + the contractions in `φsΛ` and those in `φsucΛ`. -/ def join {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : WickContraction φs.length := ⟨φsΛ.1 ∪ φsucΛ.1.map (Finset.mapEmbedding uncontractedListEmd).toEmbedding, by diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean index fd5c0c4..866a125 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean @@ -28,10 +28,11 @@ def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) := Finset.univ.filter (fun i => i1 < i ∧ i < i2 ∧ (c.getDual? i = none ∨ ∀ (h : (c.getDual? i).isSome), i1 < (c.getDual? i).get h)) -/-- Given a Wick contraction `φsΛ` associated with a list of states `φs` - the sign associated with `φsΛ` is the sign corresponding to the number - of fermionic-fermionic exchanges one must do to put elements in contracted pairs - of `φsΛ` next to each other. -/ +/-- For a list `φs` of `𝓕.FieldOp`, and a Wick contraction `φsΛ` of `φs`, + the complex number `φsΛ.sign` is defined to be the sign (`1` or `-1`) corresponding + to the number of `fermionic`-`fermionic` exchanges that must done to put + contracted pairs with `φsΛ` next to one another, starting from the contracted pair + whose first element occurs at the left-most position. -/ def sign (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : ℂ := ∏ (a : φsΛ.1), 𝓢(𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a], 𝓕 |>ₛ ⟨φs.get, φsΛ.signFinset (φsΛ.fstFieldOfContract a) (φsΛ.sndFieldOfContract a)⟩) diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean b/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean index 9323984..b60aa34 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean @@ -238,10 +238,14 @@ lemma signInsertNone_eq_filterset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) simp [h] · exact hG -/-- For `φsΛ` a grading compliant Wick contraction, and `i : Fin φs.length.succ` we have +/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a graded compliant Wick contraction `φsΛ` of `φs`, + an `i ≤ φs.length` and a `φ` in `𝓕.FieldOp`, the following relation holds `(φsΛ ↩Λ φ i none).sign = s * φsΛ.sign` where `s` is the sign got by moving `φ` through the elements of `φ₀…φᵢ₋₁` which - are contracted. -/ + are contracted with some element. + + The proof of this result involves a careful consideration of the contributions of different + `FieldOp`s in `φs` to the sign of `φsΛ ↩Λ φ i none`. -/ lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) : (φsΛ ↩Λ φ i none).sign = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter @@ -250,6 +254,11 @@ lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) rw [signInsertNone_eq_filterset] exact hG +/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a graded compliant Wick contraction `φsΛ` of `φs`, + and a `φ` in `𝓕.FieldOp`, the following relation holds + `(φsΛ ↩Λ φ 0 none).sign = φsΛ.sign`. + + This is a direct corollary of `sign_insert_none`. -/ lemma sign_insert_none_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by rw [sign_insert_none_eq_signInsertNone_mul_sign] diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean b/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean index 7208fe3..42cad05 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean @@ -855,13 +855,15 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.FieldOp) (φs : exact fun h => lt_of_le_of_ne h (Fin.succAbove_ne i ((φsΛ.getDual? j).get hj)) /-- -For `k < i`, the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of -- the sign associated with moving `φ` through the `φsΛ`-uncontracted fields in `φ₀…φₖ`, -- the sign associated with moving `φ` through the fields in `φ₀…φᵢ₋₁`, +For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of + `𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `kₛφ) = 𝓕|>ₛφs[k.1]) : diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean b/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean index 223ff6e..a540dae 100644 --- a/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean +++ b/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean @@ -417,11 +417,13 @@ lemma join_sign_induction {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs apply sign_congr exact join_uncontractedListGet (singleton hij) φsucΛ' -/-- Let `φsΛ` be a grading compliant Wick contraction for `φs` and - `φsucΛ` a Wick contraction for `[φsΛ]ᵘᶜ`. Then `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`. +/-- For a list `φs` of `𝓕.FieldOp`, a grading compliant Wick contraction `φsΛ` of `φs`, + and a Wick contraction `φsucΛ` of `[φsΛ]ᵘᶜ`, the following relation holds + `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`. - This lemma manifests the fact that it does not matter which order contracted pairs are brought - together when defining the sign of a contraction. -/ + In `φsΛ.sign` the sign is determined by starting with the contracted pair + whose first element occurs at the left-most position. This lemma manifests that + choice does not matter, and that contracted pairs can be brought together in any order. -/ lemma join_sign {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : φsΛ.GradingCompliant) : (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign := by diff --git a/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean b/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean index ec89410..d5dabf8 100644 --- a/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean +++ b/HepLean/PerturbationTheory/WickContraction/Uncontracted.lean @@ -16,7 +16,8 @@ namespace WickContraction variable {n : ℕ} (c : WickContraction n) open HepLean.List -/-- Given a Wick contraction, the finset of elements of `Fin n` which are not contracted. -/ +/-- For a Wick contraction `c`, `c.uncontracted` is defined as the finset of elements of `Fin n` + which are not in any contracted pair. -/ def uncontracted : Finset (Fin n) := Finset.filter (fun i => c.getDual? i = none) (Finset.univ) lemma congr_uncontracted {n m : ℕ} (c : WickContraction n) (h : n = m) : diff --git a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean index a5464c0..efb5b39 100644 --- a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean +++ b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean @@ -314,8 +314,11 @@ lemma take_uncontractedIndexEquiv_symm (k : c.uncontracted) : -/ -/-- Given a Wick Contraction `φsΛ` for a list of states `φs`. The list of uncontracted - states in `φs`. -/ +/-- Given a Wick Contraction `φsΛ` of a list `φs` of `𝓕.FieldOp`. The list + `φsΛ.uncontractedListGet` of `𝓕.FieldOp` is defined as the list `φs` with + all contracted positions removed, leaving the uncontracted `𝓕.FieldOp`. + + The notation `[φsΛ]ᵘᶜ` is used for `φsΛ.uncontractedListGet`. -/ def uncontractedListGet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : List 𝓕.FieldOp := φsΛ.uncontractedList.map φs.get diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 05e43c5..06fdecf 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -192,30 +192,33 @@ def perturbationTheory : Note where .name ``FieldSpecification.normalOrderSign_eraseIdx .complete, .name ``FieldSpecification.FieldOpFreeAlgebra.normalOrderF .complete, .name ``FieldSpecification.FieldOpAlgebra.normalOrder .complete, + .name ``FieldSpecification.FieldOpAlgebra.normalOrder_superCommute_eq_zero .complete, .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum .complete, .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum .complete, .h1 "Wick Contractions", .h2 "Definition", - .name ``WickContraction .incomplete, - .name ``WickContraction.GradingCompliant .incomplete, + .name ``WickContraction .complete, + .name `WickContraction.contraction_notation .complete, + .name ``WickContraction.GradingCompliant .complete, .h2 "Aside: Cardinality", - .name ``WickContraction.card_eq_cardFun .incomplete, + .name ``WickContraction.card_eq_cardFun .complete, + .h2 "Uncontracted elements", + .name ``WickContraction.uncontracted .complete, + .name ``WickContraction.uncontractedListGet .complete, .h2 "Constructors", - .p "There are a number of ways to construct a Wick contraction from - other Wick contractions or single contractions.", - .name ``WickContraction.insertAndContract .incomplete, - .name ``WickContraction.join .incomplete, + .name ``WickContraction.insertAndContract .complete, + .name ``WickContraction.join .complete, .h2 "Sign", - .name ``WickContraction.sign .incomplete, - .name ``WickContraction.join_sign .incomplete, - .name ``WickContraction.sign_insert_none .incomplete, - .name ``WickContraction.sign_insert_none_zero .incomplete, - .name ``WickContraction.sign_insert_some_of_not_lt .incomplete, - .name ``WickContraction.sign_insert_some_of_lt .incomplete, - .name ``WickContraction.sign_insert_some_zero .incomplete, + .name ``WickContraction.sign .complete, + .name ``WickContraction.join_sign .complete, + .name ``WickContraction.sign_insert_none .complete, + .name ``WickContraction.sign_insert_none_zero .complete, + .name ``WickContraction.sign_insert_some_of_not_lt .complete, + .name ``WickContraction.sign_insert_some_of_lt .complete, + .name ``WickContraction.sign_insert_some_zero .complete, .h2 "Normal order", - .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none .incomplete, - .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some .incomplete, + .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none .complete, + .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some .complete, .h1 "Static contractions", .name ``WickContraction.staticContract .incomplete, .name ``WickContraction.staticContract_insert_some_of_lt .incomplete,