refactor: Rename asymptotic states

2025-01-23 10:46:50 +00:00 · 2025-01-23 10:46:50 +00:00 · c9deac6cfe
commit c9deac6cfe
parent ba51484b1f
14 changed files with 279 additions and 155 deletions
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean
@ -137,13 +137,13 @@ lemma ofStateList_sum (φs : List 𝓕.States) :
 def crPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
  FreeAlgebra.lift ℂ fun φ =>
  match φ with
-  | States.negAsymp φ => ofCrAnState ⟨States.negAsymp φ, ()⟩
+  | States.inAsymp φ => ofCrAnState ⟨States.inAsymp φ, ()⟩
  | States.position φ => ofCrAnState ⟨States.position φ, CreateAnnihilate.create⟩
-  | States.posAsymp _ => 0
+  | States.outAsymp _ => 0

@[simp]
-lemma crPart_negAsymp (φ : 𝓕.AsymptoticNegTime) :
-    crPart (StateAlgebra.ofState (States.negAsymp φ)) = ofCrAnState ⟨States.negAsymp φ, ()⟩ := by
+lemma crPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+    crPart (StateAlgebra.ofState (States.inAsymp φ)) = ofCrAnState ⟨States.inAsymp φ, ()⟩ := by
  dsimp only [crPart, StateAlgebra.ofState]
  rw [FreeAlgebra.lift_ι_apply]

@ -155,8 +155,8 @@ lemma crPart_position (φ : 𝓕.PositionStates) :
  rw [FreeAlgebra.lift_ι_apply]

@[simp]
-lemma crPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
-    crPart (StateAlgebra.ofState (States.posAsymp φ)) = 0 := by
+lemma crPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+    crPart (StateAlgebra.ofState (States.outAsymp φ)) = 0 := by
  dsimp only [crPart, StateAlgebra.ofState]
  rw [FreeAlgebra.lift_ι_apply]

@ -166,13 +166,13 @@ lemma crPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
 def anPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
  FreeAlgebra.lift ℂ fun φ =>
  match φ with
-  | States.negAsymp _ => 0
+  | States.inAsymp _ => 0
  | States.position φ => ofCrAnState ⟨States.position φ, CreateAnnihilate.annihilate⟩
-  | States.posAsymp φ => ofCrAnState ⟨States.posAsymp φ, ()⟩
+  | States.outAsymp φ => ofCrAnState ⟨States.outAsymp φ, ()⟩

@[simp]
-lemma anPart_negAsymp (φ : 𝓕.AsymptoticNegTime) :
-    anPart (StateAlgebra.ofState (States.negAsymp φ)) = 0 := by
+lemma anPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+    anPart (StateAlgebra.ofState (States.inAsymp φ)) = 0 := by
  dsimp only [anPart, StateAlgebra.ofState]
  rw [FreeAlgebra.lift_ι_apply]

@ -184,8 +184,8 @@ lemma anPart_position (φ : 𝓕.PositionStates) :
  rw [FreeAlgebra.lift_ι_apply]

@[simp]
-lemma anPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
-    anPart (StateAlgebra.ofState (States.posAsymp φ)) = ofCrAnState ⟨States.posAsymp φ, ()⟩ := by
+lemma anPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+    anPart (StateAlgebra.ofState (States.outAsymp φ)) = ofCrAnState ⟨States.outAsymp φ, ()⟩ := by
  dsimp only [anPart, StateAlgebra.ofState]
  rw [FreeAlgebra.lift_ι_apply]

@ -193,14 +193,14 @@ lemma ofState_eq_crPart_add_anPart (φ : 𝓕.States) :
    ofState φ = crPart (StateAlgebra.ofState φ) + anPart (StateAlgebra.ofState φ) := by
  rw [ofState]
  cases φ with
-  | negAsymp φ =>
+  | inAsymp φ =>
    dsimp only [statesToCrAnType]
    simp
  | position φ =>
    dsimp only [statesToCrAnType]
    rw [CreateAnnihilate.sum_eq]
    simp
-  | posAsymp φ =>
+  | outAsymp φ =>
    dsimp only [statesToCrAnType]
    simp

--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@ -107,30 +107,30 @@ lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
    normalOrder (crPart (StateAlgebra.ofState φ) * a) =
    crPart (StateAlgebra.ofState φ) * normalOrder a := by
  match φ with
-  | .negAsymp φ =>
+  | .inAsymp φ =>
    dsimp only [crPart, StateAlgebra.ofState]
    simp only [FreeAlgebra.lift_ι_apply]
-    exact normalOrder_create_mul ⟨States.negAsymp φ, ()⟩ rfl a
+    exact normalOrder_create_mul ⟨States.inAsymp φ, ()⟩ rfl a
  | .position φ =>
    dsimp only [crPart, StateAlgebra.ofState]
    simp only [FreeAlgebra.lift_ι_apply]
    refine normalOrder_create_mul _ ?_ _
    simp [crAnStatesToCreateAnnihilate]
-  | .posAsymp φ =>
+  | .outAsymp φ =>
    simp

 lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
    normalOrder (a * anPart (StateAlgebra.ofState φ)) =
    normalOrder a * anPart (StateAlgebra.ofState φ) := by
  match φ with
-  | .negAsymp φ =>
+  | .inAsymp φ =>
    simp
  | .position φ =>
    dsimp only [anPart, StateAlgebra.ofState]
    simp only [FreeAlgebra.lift_ι_apply]
    refine normalOrder_mul_annihilate _ ?_ _
    simp [crAnStatesToCreateAnnihilate]
-  | .posAsymp φ =>
+  | .outAsymp φ =>
    dsimp only [anPart, StateAlgebra.ofState]
    simp only [FreeAlgebra.lift_ι_apply]
    refine normalOrder_mul_annihilate _ ?_ _
@ -221,9 +221,9 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
    normalOrder (a * (anPart (StateAlgebra.ofState φ')) *
      (crPart (StateAlgebra.ofState φ)) * b) := by
  match φ, φ' with
-  | _, .negAsymp φ' =>
+  | _, .inAsymp φ' =>
    simp
-  | .posAsymp φ, _ =>
+  | .outAsymp φ, _ =>
    simp
  | .position φ, .position φ' =>
    simp only [crPart_position, anPart_position, instCommGroup.eq_1]
@ -231,19 +231,19 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
    rfl
    rfl
-  | .negAsymp φ, .posAsymp φ' =>
+  | .inAsymp φ, .outAsymp φ' =>
    simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1]
    rw [normalOrder_swap_create_annihlate]
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
    rfl
    rfl
-  | .negAsymp φ, .position φ' =>
+  | .inAsymp φ, .position φ' =>
    simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1]
    rw [normalOrder_swap_create_annihlate]
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
    rfl
    rfl
-  | .position φ, .posAsymp φ' =>
+  | .position φ, .outAsymp φ' =>
    simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1]
    rw [normalOrder_swap_create_annihlate]
    simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
@ -270,20 +270,20 @@ lemma normalOrder_superCommute_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnA
    normalOrder (a * superCommute
    (crPart (StateAlgebra.ofState φ)) (anPart (StateAlgebra.ofState φ')) * b) = 0 := by
  match φ, φ' with
-  | _, .negAsymp φ' =>
+  | _, .inAsymp φ' =>
    simp
-  | .posAsymp φ', _ =>
+  | .outAsymp φ', _ =>
    simp
  | .position φ, .position φ' =>
    simp only [crPart_position, anPart_position]
    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
-  | .negAsymp φ, .posAsymp φ' =>
+  | .inAsymp φ, .outAsymp φ' =>
    simp only [crPart_negAsymp, anPart_posAsymp]
    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
-  | .negAsymp φ, .position φ' =>
+  | .inAsymp φ, .position φ' =>
    simp only [crPart_negAsymp, anPart_position]
    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _
-  | .position φ, .posAsymp φ' =>
+  | .position φ, .outAsymp φ' =>
    simp only [crPart_position, anPart_posAsymp]
    refine normalOrder_superCommute_create_annihilate _ _ (by rfl) (by rfl) _ _

@ -291,20 +291,20 @@ lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnA
    normalOrder (a * superCommute
    (anPart (StateAlgebra.ofState φ)) (crPart (StateAlgebra.ofState φ')) * b) = 0 := by
  match φ, φ' with
-  | .negAsymp φ', _ =>
+  | .inAsymp φ', _ =>
    simp
-  | _, .posAsymp φ' =>
+  | _, .outAsymp φ' =>
    simp
  | .position φ, .position φ' =>
    simp only [anPart_position, crPart_position]
    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
-  | .posAsymp φ', .negAsymp φ =>
+  | .outAsymp φ', .inAsymp φ =>
    simp only [anPart_posAsymp, crPart_negAsymp]
    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
-  | .position φ', .negAsymp φ =>
+  | .position φ', .inAsymp φ =>
    simp only [anPart_position, crPart_negAsymp]
    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
-  | .posAsymp φ, .position φ' =>
+  | .outAsymp φ, .position φ' =>
    simp only [anPart_posAsymp, crPart_position]
    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _

@ -576,13 +576,13 @@ lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
    + ⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φs')⟩ₛca := by
  rw [normalOrder_mul_anPart]
  match φ with
-  | .negAsymp φ =>
+  | .inAsymp φ =>
    simp
  | .position φ =>
    simp only [anPart_position, instCommGroup.eq_1]
    rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute]
    simp [crAnStatistics]
-  | .posAsymp φ =>
+  | .outAsymp φ =>
    simp only [anPart_posAsymp, instCommGroup.eq_1]
    rw [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute]
    simp [crAnStatistics]
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
@ -101,26 +101,26 @@ lemma superCommute_anPart_crPart (φ φ' : 𝓕.States) :
    anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
  match φ, φ' with
-  | States.negAsymp φ, _ =>
+  | States.inAsymp φ, _ =>
    simp
-  | _, States.posAsymp φ =>
+  | _, States.outAsymp φ =>
    simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul,
      sub_self]
  | States.position φ, States.position φ' =>
    simp only [anPart_position, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.posAsymp φ, States.position φ' =>
+  | States.outAsymp φ, States.position φ' =>
    simp only [anPart_posAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.position φ, States.negAsymp φ' =>
+  | States.position φ, States.inAsymp φ' =>
    simp only [anPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp only [List.singleton_append, instCommGroup.eq_1, crAnStatistics,
      FieldStatistic.ofList_singleton, Function.comp_apply, crAnStatesToStates_prod, ←
      ofCrAnList_append]
-  | States.posAsymp φ, States.negAsymp φ' =>
+  | States.outAsymp φ, States.inAsymp φ' =>
    simp only [anPart_posAsymp, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
@ -131,25 +131,25 @@ lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
    match φ, φ' with
-    | States.posAsymp φ, _ =>
+    | States.outAsymp φ, _ =>
    simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
      mul_zero, sub_self]
-    | _, States.negAsymp φ =>
+    | _, States.inAsymp φ =>
    simp only [anPart_negAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul,
      sub_self]
    | States.position φ, States.position φ' =>
    simp only [crPart_position, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-    | States.position φ, States.posAsymp φ' =>
+    | States.position φ, States.outAsymp φ' =>
    simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-    | States.negAsymp φ, States.position φ' =>
+    | States.inAsymp φ, States.position φ' =>
    simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-    | States.negAsymp φ, States.posAsymp φ' =>
+    | States.inAsymp φ, States.outAsymp φ' =>
    simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
@ -160,24 +160,24 @@ lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) :
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    crPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
  match φ, φ' with
-  | States.posAsymp φ, _ =>
+  | States.outAsymp φ, _ =>
  simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
    mul_zero, sub_self]
-  | _, States.posAsymp φ =>
+  | _, States.outAsymp φ =>
  simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self]
  | States.position φ, States.position φ' =>
  simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
  simp [crAnStatistics, ← ofCrAnList_append]
-  | States.position φ, States.negAsymp φ' =>
+  | States.position φ, States.inAsymp φ' =>
  simp only [crPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
  simp [crAnStatistics, ← ofCrAnList_append]
-  | States.negAsymp φ, States.position φ' =>
+  | States.inAsymp φ, States.position φ' =>
  simp only [crPart_negAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
  simp [crAnStatistics, ← ofCrAnList_append]
-  | States.negAsymp φ, States.negAsymp φ' =>
+  | States.inAsymp φ, States.inAsymp φ' =>
  simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
  simp [crAnStatistics, ← ofCrAnList_append]
@ -188,23 +188,23 @@ lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    anPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
  match φ, φ' with
-  | States.negAsymp φ, _ =>
+  | States.inAsymp φ, _ =>
    simp
-  | _, States.negAsymp φ =>
+  | _, States.inAsymp φ =>
    simp
  | States.position φ, States.position φ' =>
    simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.position φ, States.posAsymp φ' =>
+  | States.position φ, States.outAsymp φ' =>
    simp only [anPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.posAsymp φ, States.position φ' =>
+  | States.outAsymp φ, States.position φ' =>
    simp only [anPart_posAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.posAsymp φ, States.posAsymp φ' =>
+  | States.outAsymp φ, States.outAsymp φ' =>
    simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
    simp [crAnStatistics, ← ofCrAnList_append]
@ -214,7 +214,7 @@ lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States
    crPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs *
    crPart (StateAlgebra.ofState φ) := by
  match φ with
-  | States.negAsymp φ =>
+  | States.inAsymp φ =>
    simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
    simp [crAnStatistics]
@ -222,7 +222,7 @@ lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States
    simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
    simp [crAnStatistics]
-  | States.posAsymp φ =>
+  | States.outAsymp φ =>
    simp

 lemma superCommute_anPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States) :
@ -230,13 +230,13 @@ lemma superCommute_anPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States
    anPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) •
    ofStateList φs * anPart (StateAlgebra.ofState φ) := by
  match φ with
-  | States.negAsymp φ =>
+  | States.inAsymp φ =>
    simp
  | States.position φ =>
    simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
    simp [crAnStatistics]
-  | States.posAsymp φ =>
+  | States.outAsymp φ =>
    simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
    simp [crAnStatistics]
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
@ -63,13 +63,13 @@ lemma crAnF_superCommute_ofCrAnState_ofState_mem_center (φ : 𝓕.CrAnStates) (
 lemma crAnF_superCommute_anPart_ofState_mem_center (φ ψ : 𝓕.States) :
    𝓞.crAnF ⟨anPart (StateAlgebra.ofState φ), ofState ψ⟩ₛca ∈ Subalgebra.center ℂ 𝓞.A := by
  match φ with
-  | States.negAsymp _ =>
+  | States.inAsymp _ =>
    simp only [anPart_negAsymp, map_zero, LinearMap.zero_apply]
    exact Subalgebra.zero_mem (Subalgebra.center ℂ 𝓞.A)
  | States.position φ =>
    simp only [anPart_position]
    exact 𝓞.crAnF_superCommute_ofCrAnState_ofState_mem_center _ _
-  | States.posAsymp _ =>
+  | States.outAsymp _ =>
    simp only [anPart_posAsymp]
    exact 𝓞.crAnF_superCommute_ofCrAnState_ofState_mem_center _ _

@ -86,13 +86,13 @@ lemma crAnF_superCommute_anPart_ofState_diff_grade_zero (φ ψ : 𝓕.States)
    (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) :
    𝓞.crAnF (superCommute (anPart (StateAlgebra.ofState φ)) (ofState ψ)) = 0 := by
  match φ with
-  | States.negAsymp _ =>
+  | States.inAsymp _ =>
    simp
  | States.position φ =>
    simp only [anPart_position]
    apply 𝓞.crAnF_superCommute_ofCrAnState_ofState_diff_grade_zero _ _ _
    simpa [crAnStatistics] using h
-  | States.posAsymp _ =>
+  | States.outAsymp _ =>
    simp only [anPart_posAsymp]
    apply 𝓞.crAnF_superCommute_ofCrAnState_ofState_diff_grade_zero _ _
    simpa [crAnStatistics] using h
@ -108,26 +108,26 @@ lemma crAnF_superCommute_ofState_ofState_mem_center (φ ψ : 𝓕.States) :
 lemma crAnF_superCommute_anPart_anPart (φ ψ : 𝓕.States) :
    𝓞.crAnF ⟨anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState ψ)⟩ₛca = 0 := by
  match φ, ψ with
-  | _, States.negAsymp _ =>
+  | _, States.inAsymp _ =>
    simp
-  | States.negAsymp _, _ =>
+  | States.inAsymp _, _ =>
    simp
  | States.position φ, States.position ψ =>
    simp only [anPart_position]
    rw [𝓞.superCommute_annihilate_annihilate]
    rfl
    rfl
-  | States.position φ, States.posAsymp _ =>
+  | States.position φ, States.outAsymp _ =>
    simp only [anPart_position, anPart_posAsymp]
    rw [𝓞.superCommute_annihilate_annihilate]
    rfl
    rfl
-  | States.posAsymp _, States.posAsymp _ =>
+  | States.outAsymp _, States.outAsymp _ =>
    simp only [anPart_posAsymp]
    rw [𝓞.superCommute_annihilate_annihilate]
    rfl
    rfl
-  | States.posAsymp _, States.position _ =>
+  | States.outAsymp _, States.position _ =>
    simp only [anPart_posAsymp, anPart_position]
    rw [𝓞.superCommute_annihilate_annihilate]
    rfl
@ -136,26 +136,26 @@ lemma crAnF_superCommute_anPart_anPart (φ ψ : 𝓕.States) :
 lemma crAnF_superCommute_crPart_crPart (φ ψ : 𝓕.States) :
    𝓞.crAnF ⟨crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState ψ)⟩ₛca = 0 := by
  match φ, ψ with
-  | _, States.posAsymp _ =>
+  | _, States.outAsymp _ =>
    simp
-  | States.posAsymp _, _ =>
+  | States.outAsymp _, _ =>
    simp
  | States.position φ, States.position ψ =>
    simp only [crPart_position]
    rw [𝓞.superCommute_create_create]
    rfl
    rfl
-  | States.position φ, States.negAsymp _ =>
+  | States.position φ, States.inAsymp _ =>
    simp only [crPart_position, crPart_negAsymp]
    rw [𝓞.superCommute_create_create]
    rfl
    rfl
-  | States.negAsymp _, States.negAsymp _ =>
+  | States.inAsymp _, States.inAsymp _ =>
    simp only [crPart_negAsymp]
    rw [𝓞.superCommute_create_create]
    rfl
    rfl
-  | States.negAsymp _, States.position _ =>
+  | States.inAsymp _, States.position _ =>
    simp only [crPart_negAsymp, crPart_position]
    rw [𝓞.superCommute_create_create]
    rfl
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
@ -222,13 +222,13 @@ lemma crAnF_normalOrder_anPart_ofStatesList_swap (φ : 𝓕.States)
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    𝓞.crAnF (normalOrder (ofStateList φ' * anPart (StateAlgebra.ofState φ))) := by
  match φ with
-  | .negAsymp φ =>
+  | .inAsymp φ =>
    simp
  | .position φ =>
    simp only [anPart_position, instCommGroup.eq_1]
    rw [crAnF_normalOrder_ofCrAnState_ofStatesList_swap]
    rfl
-  | .posAsymp φ =>
+  | .outAsymp φ =>
    simp only [anPart_posAsymp, instCommGroup.eq_1]
    rw [crAnF_normalOrder_ofCrAnState_ofStatesList_swap]
    rfl
@ -309,13 +309,13 @@ lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.States
    𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), ofState φs[n]⟩ₛca)
    * 𝓞.crAnF (normalOrder (ofStateList (φs.eraseIdx n))) := by
  match φ with
-  | .negAsymp φ =>
+  | .inAsymp φ =>
    simp
  | .position φ =>
    simp only [anPart_position, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc]
    rw [crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum]
    simp [crAnStatistics]
-  | .posAsymp φ =>
+  | .outAsymp φ =>
    simp only [anPart_posAsymp, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc]
    rw [crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum]
    simp [crAnStatistics]
--- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
@ -44,26 +44,26 @@ structure FieldSpecification where
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)

-/-- Negative asymptotic states are specified by a field and a momentum. -/
-def AsymptoticNegTime : Type := 𝓕.Fields × Lorentz.Contr 4
+/-- Incoming asymptotic states are specified by a field and a momentum. -/
+def IncomingAsymptotic : Type := 𝓕.Fields × Lorentz.Contr 4

-/-- Positive asymptotic states are specified by a field and a momentum. -/
-def AsymptoticPosTime : Type := 𝓕.Fields × Lorentz.Contr 4
+/-- Outgoing asymptotic states are specified by a field and a momentum. -/
+def OutgoingAsymptotic : Type := 𝓕.Fields × Lorentz.Contr 4

 /-- States specified by a field and a space-time position. -/
 def PositionStates : Type := 𝓕.Fields × SpaceTime

 /-- The combination of asymptotic states and position states. -/
 inductive States (𝓕 : FieldSpecification) where
-  | negAsymp : 𝓕.AsymptoticNegTime → 𝓕.States
+  | inAsymp : 𝓕.IncomingAsymptotic → 𝓕.States
  | position : 𝓕.PositionStates → 𝓕.States
-  | posAsymp : 𝓕.AsymptoticPosTime → 𝓕.States
+  | outAsymp : 𝓕.OutgoingAsymptotic → 𝓕.States

 /-- Taking a state to its underlying field. -/
 def statesToField : 𝓕.States → 𝓕.Fields
-  | States.negAsymp φ => φ.1
+  | States.inAsymp φ => φ.1
  | States.position φ => φ.1
-  | States.posAsymp φ => φ.1
+  | States.outAsymp φ => φ.1

 /-- The statistics associated to a state. -/
 def statesStatistic : 𝓕.States → FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField
--- a/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean
@ -38,23 +38,23 @@ variable (𝓕 : FieldSpecification)
  For asymptotic staes there is only one allowed part, whilst for position states
  there is two. -/
 def statesToCrAnType : 𝓕.States → Type
-  | States.negAsymp _ => Unit
+  | States.inAsymp _ => Unit
  | States.position _ => CreateAnnihilate
-  | States.posAsymp _ => Unit
+  | States.outAsymp _ => Unit

 /-- The instance of a finite type on `𝓕.statesToCreateAnnihilateType i`. -/
 instance : ∀ i, Fintype (𝓕.statesToCrAnType i) := fun i =>
  match i with
-  | States.negAsymp _ => inferInstanceAs (Fintype Unit)
+  | States.inAsymp _ => inferInstanceAs (Fintype Unit)
  | States.position _ => inferInstanceAs (Fintype CreateAnnihilate)
-  | States.posAsymp _ => inferInstanceAs (Fintype Unit)
+  | States.outAsymp _ => inferInstanceAs (Fintype Unit)

 /-- The instance of a decidable equality on `𝓕.statesToCreateAnnihilateType i`. -/
 instance : ∀ i, DecidableEq (𝓕.statesToCrAnType i) := fun i =>
  match i with
-  | States.negAsymp _ => inferInstanceAs (DecidableEq Unit)
+  | States.inAsymp _ => inferInstanceAs (DecidableEq Unit)
  | States.position _ => inferInstanceAs (DecidableEq CreateAnnihilate)
-  | States.posAsymp _ => inferInstanceAs (DecidableEq Unit)
+  | States.outAsymp _ => inferInstanceAs (DecidableEq Unit)

 /-- The equivalence between `𝓕.statesToCreateAnnihilateType i` and
  `𝓕.statesToCreateAnnihilateType j` from an equality `i = j`. -/
@ -77,10 +77,10 @@ lemma crAnStatesToStates_prod (s : 𝓕.States) (t : 𝓕.statesToCrAnType s) :
 /-- The map from creation and annihlation states to the type `CreateAnnihilate`
  specifying if a state is a creation or an annihilation state. -/
 def crAnStatesToCreateAnnihilate : 𝓕.CrAnStates → CreateAnnihilate
-  | ⟨States.negAsymp _, _⟩ => CreateAnnihilate.create
+  | ⟨States.inAsymp _, _⟩ => CreateAnnihilate.create
  | ⟨States.position _, CreateAnnihilate.create⟩ => CreateAnnihilate.create
  | ⟨States.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate
-  | ⟨States.posAsymp _, _⟩ => CreateAnnihilate.annihilate
+  | ⟨States.outAsymp _, _⟩ => CreateAnnihilate.annihilate

 /-- Takes a `CrAnStates` state to its corresponding fields statistic (bosonic or fermionic). -/
 def crAnStatistics : 𝓕.CrAnStates → FieldStatistic :=
--- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
@ -19,24 +19,24 @@ variable {𝓕 : FieldSpecification}
  if and only if `φ1` has a time less-then or equal to `φ0`, or `φ1` is a negative
  asymptotic state, or `φ0` is a positive asymptotic state. -/
 def timeOrderRel : 𝓕.States → 𝓕.States → Prop
-  | States.posAsymp _, _ => True
+  | States.outAsymp _, _ => True
  | States.position φ0, States.position φ1 => φ1.2 0 ≤ φ0.2 0
-  | States.position _, States.negAsymp _ => True
-  | States.position _, States.posAsymp _ => False
-  | States.negAsymp _, States.posAsymp _ => False
-  | States.negAsymp _, States.position _ => False
-  | States.negAsymp _, States.negAsymp _ => True
+  | States.position _, States.inAsymp _ => True
+  | States.position _, States.outAsymp _ => False
+  | States.inAsymp _, States.outAsymp _ => False
+  | States.inAsymp _, States.position _ => False
+  | States.inAsymp _, States.inAsymp _ => True

 /-- The relation `timeOrderRel` is decidable, but not computablly so due to
  `Real.decidableLE`. -/
 noncomputable instance : (φ φ' : 𝓕.States) → Decidable (timeOrderRel φ φ')
-  | States.posAsymp _, _ => isTrue True.intro
+  | States.outAsymp _, _ => isTrue True.intro
  | States.position φ0, States.position φ1 => inferInstanceAs (Decidable (φ1.2 0 ≤ φ0.2 0))
-  | States.position _, States.negAsymp _ => isTrue True.intro
-  | States.position _, States.posAsymp _ => isFalse (fun a => a)
-  | States.negAsymp _, States.posAsymp _ => isFalse (fun a => a)
-  | States.negAsymp _, States.position _ => isFalse (fun a => a)
-  | States.negAsymp _, States.negAsymp _ => isTrue True.intro
+  | States.position _, States.inAsymp _ => isTrue True.intro
+  | States.position _, States.outAsymp _ => isFalse (fun a => a)
+  | States.inAsymp _, States.outAsymp _ => isFalse (fun a => a)
+  | States.inAsymp _, States.position _ => isFalse (fun a => a)
+  | States.inAsymp _, States.inAsymp _ => isTrue True.intro

 /-- Time ordering is total. -/
 instance : IsTotal 𝓕.States 𝓕.timeOrderRel where
--- a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
@ -24,8 +24,10 @@ namespace FieldStatistic

 variable {𝓕 : Type}

-/-- The echange sign of two field statistics.
-  Defined to be `-1` if both field statistics are `fermionic` and `1` otherwise. -/
+/-- The exchange sign of two field statistics is defined to be
+  `-1` if both field statistics are `fermionic` and `1` otherwise.
+  It is a group homomorphism from `FieldStatistic` to the group of homomorphisms from
+  `FieldStatistic` to `ℂ`. -/
 def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
  toFun a :=
    {
--- a/HepLean/PerturbationTheory/WicksTheorem.lean
+++ b/HepLean/PerturbationTheory/WicksTheorem.lean
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.WickContraction.TimeContract
+import HepLean.Meta.Remark.Basic
 /-!

 # Wick's theorem
@ -260,19 +261,6 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') :
  subst h
  simp

-/-- Wick's theorem for the empty list. -/
-lemma wicks_theorem_nil :
-    𝓞.crAnF (ofStateAlgebra (timeOrder (ofList []))) = ∑ (c : WickContraction [].length),
-    (c.sign [] • c.timeContract 𝓞) *
-    𝓞.crAnF (normalOrder (ofStateList (c.uncontractedList.map [].get))) := by
-  rw [timeOrder_ofList_nil]
-  simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
-  rw [sum_WickContraction_nil, nil_zero_uncontractedList]
-  simp only [List.map_nil]
-  have h1 : ofStateList (𝓕 := 𝓕) [] = CrAnAlgebra.ofCrAnList [] := by simp
-  rw [h1, normalOrder_ofCrAnList]
-  simp [WickContraction.timeContract, empty, sign]
-
 lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.States) :
    timeOrder (ofList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
      (Finset.filter (fun x =>
@ -320,6 +308,33 @@ lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.S
        (Finset.filter (fun x => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs)
          Finset.univ)

+
+/-!
+
+## Wick's theorem
+
+-/
+
+/-- Wick's theorem for the empty list. -/
+lemma wicks_theorem_nil :
+    𝓞.crAnF (ofStateAlgebra (timeOrder (ofList []))) = ∑ (c : WickContraction [].length),
+    (c.sign [] • c.timeContract 𝓞) *
+    𝓞.crAnF (normalOrder (ofStateList (c.uncontractedList.map [].get))) := by
+  rw [timeOrder_ofList_nil]
+  simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
+  rw [sum_WickContraction_nil, nil_zero_uncontractedList]
+  simp only [List.map_nil]
+  have h1 : ofStateList (𝓕 := 𝓕) [] = CrAnAlgebra.ofCrAnList [] := by simp
+  rw [h1, normalOrder_ofCrAnList]
+  simp [WickContraction.timeContract, empty, sign]
+
+remark wicks_theorem_context := "
+  Wick's theorem is one of the most important results in perturbative quantum field theory.
+  It expresses a time-ordered product of fields as a sum of terms consisting of
+  time-contractions of pairs of fields multiplied by the normal-ordered product of
+  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. -/
 theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra (timeOrder (ofList φs))) =
    ∑ (c : WickContraction φs.length), (c.sign φs • c.timeContract 𝓞) *