fix: Typo

HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean

@@ -0,0 +1,822 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.Logic.Equiv.Fin
+import Mathlib.Tactic.FinCases
+import Mathlib.Data.Finset.Card
+import Mathlib.CategoryTheory.IsomorphismClasses
+import Mathlib.CategoryTheory.Functor.Category
+import Mathlib.CategoryTheory.Comma.Over
+import Mathlib.Data.Fintype.Pi
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.Data.Fintype.Prod
+import Mathlib.Data.Fintype.Perm
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
+import Mathlib.SetTheory.Cardinal.Basic
+/-!
+# Feynman diagrams
+
+Feynman diagrams are a graphical representation of the terms in the perturbation expansion of
+a quantum field theory.
+
+-/
+
+open CategoryTheory
+/-!
+
+## The definition of Pre Feynman rules
+
+We define the notion of a pre-Feynman rule, which specifies the possible
+half-edges, edges and vertices in a diagram. It does not specify how to turn a diagram
+into an algebraic expression.
+
+## TODO
+Prove that the `halfEdgeLimit` functor lands on limits of functors.
+
+-/
+
+/-- A `PreFeynmanRule` is a set of rules specifying the allowed half-edges,
+  edges and vertices in a diagram. (It does not specify how to turn the diagram
+  into an algebraic expression.) -/
+structure PreFeynmanRule where
+  /-- The type labelling the different types of half-edges. -/
+  HalfEdgeLabel : Type
+  /-- A type labelling the different types of edges. -/
+  EdgeLabel : Type
+  /-- A type labelling the different types of vertices. -/
+  VertexLabel : Type
+  /-- A function taking `EdgeLabels` to the half edges it contains.
+    This will usually land on `Fin 2 → _` -/
+  edgeLabelMap : EdgeLabel → CategoryTheory.Over HalfEdgeLabel
+  /-- A function taking `VertexLabels` to the half edges it contains.
+    For example, if the vertex is of order-3 it will land on `Fin 3 → _`. -/
+  vertexLabelMap : VertexLabel → CategoryTheory.Over HalfEdgeLabel
+
+namespace PreFeynmanRule
+
+variable (P : PreFeynmanRule)
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
+  to `Over (P.VertexLabel)` induced by projections on products. -/
+def toVertex {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓥 :=
+  Over.map <| Prod.snd ∘ Prod.snd
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
+  to `Over (P.EdgeLabel)` induced by projections on products. -/
+@[simps! obj_left obj_hom map_left map_right]
+def toEdge {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over 𝓔 :=
+  Over.map <| Prod.fst ∘ Prod.snd
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)`
+  to `Over (P.HalfEdgeLabel)` induced by projections on products. -/
+@[simps! obj_left obj_hom map_left map_right]
+def toHalfEdge {𝓔 𝓥 : Type} : Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel :=
+  Over.map Prod.fst
+
+/-- The functor from `Over P.VertexLabel` to `Type` induced by pull-back along insertion of
+  `v : P.VertexLabel`. -/
+@[simps!]
+def preimageType' {𝓥 : Type} (v : 𝓥) : Over 𝓥 ⥤ Type where
+  obj := fun f => f.hom ⁻¹' {v}
+  map {f g} F := fun x =>
+    ⟨F.left x.1, by
+      have h := congrFun F.w x
+      simp only [Functor.const_obj_obj, Functor.id_obj, Functor.id_map, types_comp_apply,
+        CostructuredArrow.right_eq_id, Functor.const_obj_map, types_id_apply] at h
+      simp only [Functor.id_obj, Functor.const_obj_obj, Set.mem_preimage, Set.mem_singleton_iff]
+      obtain ⟨val, property⟩ := x
+      simp_all only
+      simp_all only [Functor.id_obj, Functor.const_obj_obj, Set.mem_preimage,
+        Set.mem_singleton_iff]⟩
+
+/-- The functor from `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)` to
+  `Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.VertexLabel`.
+  For a given vertex, it returns all half edges corresponding to that vertex. -/
+def preimageVertex {𝓔 𝓥 : Type} (v : 𝓥) :
+    Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
+  obj f := Over.mk (fun x => Prod.fst (f.hom x.1) :
+      (P.toVertex ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel)
+  map {f g} F := Over.homMk ((P.toVertex ⋙ preimageType' v).map F)
+    (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
+
+/-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` to
+  `Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.EdgeLabel`.
+  For a given edge, it returns all half edges corresponding to that edge. -/
+def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
+    Over (P.HalfEdgeLabel × 𝓔 × 𝓥) ⥤ Over P.HalfEdgeLabel where
+  obj f := Over.mk (fun x => Prod.fst (f.hom x.1) :
+      (P.toEdge ⋙ preimageType' v).obj f ⟶ P.HalfEdgeLabel)
+  map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F)
+    (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
+
+/-!
+
+## Finitness of pre-Feynman rules
+
+We define a class of `PreFeynmanRule` which have nice properties with regard to
+decidablity and finitness.
+
+In practice, every pre-Feynman rule considered in the physics literature satisfies these
+properties.
+
+-/
+
+/-- A set of conditions on `PreFeynmanRule` for it to be considered finite. -/
+class IsFinitePreFeynmanRule (P : PreFeynmanRule) where
+  /-- The type of edge labels is decidable. -/
+  edgeLabelDecidable : DecidableEq P.EdgeLabel
+  /-- The type of vertex labels is decidable. -/
+  vertexLabelDecidable : DecidableEq P.VertexLabel
+  /-- The type of half-edge labels is decidable. -/
+  halfEdgeLabelDecidable : DecidableEq P.HalfEdgeLabel
+  /-- The type of half-edges associated with a vertex is finite. -/
+  vertexMapFintype : ∀ v : P.VertexLabel, Fintype (P.vertexLabelMap v).left
+  /-- The type of half-edges associated with a vertex is decidable. -/
+  vertexMapDecidable : ∀ v : P.VertexLabel, DecidableEq (P.vertexLabelMap v).left
+  /-- The type of half-edges associated with an edge is finite. -/
+  edgeMapFintype : ∀ v : P.EdgeLabel, Fintype (P.edgeLabelMap v).left
+  /-- The type of half-edges associated with an edge is decidable. -/
+  edgeMapDecidable : ∀ v : P.EdgeLabel, DecidableEq (P.edgeLabelMap v).left
+
+/-- If `P` is a finite pre feynman rule, then equality of edge labels of `P` is decidable. -/
+instance preFeynmanRuleDecEq𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
+    DecidableEq P.EdgeLabel :=
+  IsFinitePreFeynmanRule.edgeLabelDecidable
+
+/-- If `P` is a finite pre feynman rule, then equality of vertex labels of `P` is decidable. -/
+instance preFeynmanRuleDecEq𝓥 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
+    DecidableEq P.VertexLabel :=
+  IsFinitePreFeynmanRule.vertexLabelDecidable
+
+/-- If `P` is a finite pre feynman rule, then equality of half-edge labels of `P` is decidable. -/
+instance preFeynmanRuleDecEq𝓱𝓔 (P : PreFeynmanRule) [IsFinitePreFeynmanRule P] :
+    DecidableEq P.HalfEdgeLabel :=
+  IsFinitePreFeynmanRule.halfEdgeLabelDecidable
+
+/-- If `P` is a finite pre-feynman rule, then every vertex has a finite
+  number of half-edges associated to it. -/
+instance [IsFinitePreFeynmanRule P] (v : P.VertexLabel) : Fintype (P.vertexLabelMap v).left :=
+  IsFinitePreFeynmanRule.vertexMapFintype v
+
+/-- If `P` is a finite pre-feynman rule, then the indexing set of half-edges associated
+  to a vertex is decidable. -/
+instance [IsFinitePreFeynmanRule P] (v : P.VertexLabel) : DecidableEq (P.vertexLabelMap v).left :=
+  IsFinitePreFeynmanRule.vertexMapDecidable v
+
+/-- If `P` is a finite pre-feynman rule, then every edge has a finite
+  number of half-edges associated to it. -/
+instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : Fintype (P.edgeLabelMap v).left :=
+  IsFinitePreFeynmanRule.edgeMapFintype v
+
+/-- If `P` is a finite pre-feynman rule, then the indexing set of half-edges associated
+  to an edge is decidable. -/
+instance [IsFinitePreFeynmanRule P] (v : P.EdgeLabel) : DecidableEq (P.edgeLabelMap v).left :=
+  IsFinitePreFeynmanRule.edgeMapDecidable v
+
+/-- It is decidable to check whether a half edge of a diagram (an object in
+  `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given vertex. -/
+instance preimageVertexDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓥] (v : 𝓥)
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
+    DecidablePred fun x => x ∈ (P.toVertex.obj F).hom ⁻¹' {v} := fun y =>
+  match decEq ((P.toVertex.obj F).hom y) v with
+  | isTrue h => isTrue h
+  | isFalse h => isFalse h
+
+/-- It is decidable to check whether a half edge of a diagram (an object in
+  `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`) corresponds to a given edge. -/
+instance preimageEdgeDecidablePred {𝓔 𝓥 : Type} [DecidableEq 𝓔] (v : 𝓔)
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) :
+    DecidablePred fun x => x ∈ (P.toEdge.obj F).hom ⁻¹' {v} := fun y =>
+  match decEq ((P.toEdge.obj F).hom y) v with
+  | isTrue h => isTrue h
+  | isFalse h => isFalse h
+
+/-- If `F` is an object in `Over (P.HalfEdgeLabel × 𝓔 × 𝓥)`, with a decidable source,
+  then the object in `Over P.HalfEdgeLabel` formed by following the functor `preimageVertex`
+  has a decidable source (since it is the same source). -/
+instance preimageVertexDecidable {𝓔 𝓥 : Type} (v : 𝓥)
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] :
+    DecidableEq ((P.preimageVertex v).obj F).left := Subtype.instDecidableEq
+
+/-- The half edges corresponding to a given edge has an indexing set which is decidable. -/
+instance preimageEdgeDecidable {𝓔 𝓥 : Type} (v : 𝓔)
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] :
+    DecidableEq ((P.preimageEdge v).obj F).left := Subtype.instDecidableEq
+
+/-- The half edges corresponding to a given vertex has an indexing set which is decidable. -/
+instance preimageVertexFintype {𝓔 𝓥 : Type} [DecidableEq 𝓥]
+    (v : 𝓥) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] :
+    Fintype ((P.preimageVertex v).obj F).left := @Subtype.fintype _ _ _ h
+
+/-- The half edges corresponding to a given edge has an indexing set which is finite. -/
+instance preimageEdgeFintype {𝓔 𝓥 : Type} [DecidableEq 𝓔]
+    (v : 𝓔) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [h : Fintype F.left] :
+    Fintype ((P.preimageEdge v).obj F).left := @Subtype.fintype _ _ _ h
+
+/-- The half edges corresponding to a given vertex has an indexing set which is finite. -/
+instance preimageVertexMapFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
+    [DecidableEq 𝓥] (v : 𝓥) (f : 𝓥 ⟶ P.VertexLabel) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+    [Fintype F.left] :
+    Fintype ((P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left) :=
+  Pi.fintype
+
+/-- Given an edge, there is a finite number of maps between the indexing set of the
+  expected half-edges corresponding to that edges label, and the actual indexing
+  set of half-edges corresponding to that edge. Given various finiteness conditions. -/
+instance preimageEdgeMapFintype [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type}
+    [DecidableEq 𝓔] (v : 𝓔) (f : 𝓔 ⟶ P.EdgeLabel) (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+    [Fintype F.left] :
+    Fintype ((P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left) :=
+  Pi.fintype
+
+/-!
+
+## External and internal Vertices
+
+We say a vertex Label is `external` if it has only one half-edge associated with it.
+Otherwise, we say it is `internal`.
+
+We will show that for `IsFinitePreFeynmanRule` the condition of been external is decidable.
+-/
+
+/-- A vertex is external if it has a single half-edge associated to it. -/
+def External {P : PreFeynmanRule} (v : P.VertexLabel) : Prop :=
+  IsIsomorphic (P.vertexLabelMap v).left (Fin 1)
+
+lemma external_iff_exists_bijection {P : PreFeynmanRule} (v : P.VertexLabel) :
+    External v ↔ ∃ (κ : (P.vertexLabelMap v).left → Fin 1), Function.Bijective κ := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · obtain ⟨κ, κm1, h1, h2⟩ := h
+    let f : (P.vertexLabelMap v).left ≅ (Fin 1) := ⟨κ, κm1, h1, h2⟩
+    exact ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f⟩
+  · obtain ⟨κ, h1⟩ := h
+    let f : (P.vertexLabelMap v).left ⟶ (Fin 1) := κ
+    have ft : IsIso f := (isIso_iff_bijective κ).mpr h1
+    obtain ⟨fm, hf1, hf2⟩ := ft
+    exact ⟨f, fm, hf1, hf2⟩
+
+/-- Whether or not a vertex is external is decidable. -/
+instance externalDecidable [IsFinitePreFeynmanRule P] (v : P.VertexLabel) :
+    Decidable (External v) :=
+  decidable_of_decidable_of_iff (external_iff_exists_bijection v).symm
+
+/-!
+
+## Conditions to form a diagram.
+
+-/
+
+/-- The proposition on vertices which must be satisfied by an object
+  `F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` for it to be a Feynman diagram.
+  This condition corresponds to the vertices of `F` having the correct half-edges associated
+  with them. -/
+def DiagramVertexProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+    (f : 𝓥 ⟶ P.VertexLabel) :=
+  ∀ v, IsIsomorphic (P.vertexLabelMap (f v)) ((P.preimageVertex v).obj F)
+
+/-- The proposition on edges which must be satisfied by an object
+  `F : Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` for it to be a Feynman diagram.
+  This condition corresponds to the edges of `F` having the correct half-edges associated
+  with them. -/
+def DiagramEdgeProp {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+    (f : 𝓔 ⟶ P.EdgeLabel) :=
+  ∀ v, IsIsomorphic (P.edgeLabelMap (f v)) ((P.preimageEdge v).obj F)
+
+lemma diagramVertexProp_iff {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+    (f : 𝓥 ⟶ P.VertexLabel) : P.DiagramVertexProp F f ↔
+    ∀ v, ∃ (κ : (P.vertexLabelMap (f v)).left → ((P.preimageVertex v).obj F).left),
+    Function.Bijective κ
+    ∧ ((P.preimageVertex v).obj F).hom ∘ κ = (P.vertexLabelMap (f v)).hom := by
+  refine Iff.intro (fun h v => ?_) (fun h v => ?_)
+  · obtain ⟨κ, κm1, h1, h2⟩ := h v
+    let f := (Over.forget P.HalfEdgeLabel).mapIso ⟨κ, κm1, h1, h2⟩
+    exact ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f, κ.w⟩
+  · obtain ⟨κ, h1, h2⟩ := h v
+    let f : (P.vertexLabelMap (f v)) ⟶ ((P.preimageVertex v).obj F) := Over.homMk κ h2
+    have ft : IsIso ((Over.forget P.HalfEdgeLabel).map f) := (isIso_iff_bijective κ).mpr h1
+    obtain ⟨fm, hf1, hf2⟩ := (isIso_of_reflects_iso _ (Over.forget P.HalfEdgeLabel) : IsIso f)
+    exact ⟨f, fm, hf1, hf2⟩
+
+lemma diagramEdgeProp_iff {𝓔 𝓥 : Type} (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥))
+    (f : 𝓔 ⟶ P.EdgeLabel) : P.DiagramEdgeProp F f ↔
+    ∀ v, ∃ (κ : (P.edgeLabelMap (f v)).left → ((P.preimageEdge v).obj F).left),
+    Function.Bijective κ
+    ∧ ((P.preimageEdge v).obj F).hom ∘ κ = (P.edgeLabelMap (f v)).hom := by
+  refine Iff.intro (fun h v => ?_) (fun h v => ?_)
+  · obtain ⟨κ, κm1, h1, h2⟩ := h v
+    let f := (Over.forget P.HalfEdgeLabel).mapIso ⟨κ, κm1, h1, h2⟩
+    exact ⟨f.hom, (isIso_iff_bijective f.hom).mp $ Iso.isIso_hom f, κ.w⟩
+  · obtain ⟨κ, h1, h2⟩ := h v
+    let f : (P.edgeLabelMap (f v)) ⟶ ((P.preimageEdge v).obj F) := Over.homMk κ h2
+    have ft : IsIso ((Over.forget P.HalfEdgeLabel).map f) := (isIso_iff_bijective κ).mpr h1
+    obtain ⟨fm, hf1, hf2⟩ := (isIso_of_reflects_iso _ (Over.forget P.HalfEdgeLabel) : IsIso f)
+    exact ⟨f, fm, hf1, hf2⟩
+
+/-- The proposition `DiagramVertexProp` is decidable given various decidablity and finite
+  conditions. -/
+instance diagramVertexPropDecidable
+    [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓥] [DecidableEq 𝓥]
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
+    (f : 𝓥 ⟶ P.VertexLabel) : Decidable (P.DiagramVertexProp F f) :=
+  @decidable_of_decidable_of_iff _ _
+    (@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
+    (fun _ => @instDecidableAnd _ _ _ (@Fintype.decidablePiFintype _ _
+    (fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _) _)
+    (P.diagramVertexProp_iff F f).symm
+
+/-- The proposition `DiagramEdgeProp` is decidable given various decidablity and finite
+  conditions. -/
+instance diagramEdgePropDecidable
+    [IsFinitePreFeynmanRule P] {𝓔 𝓥 : Type} [Fintype 𝓔] [DecidableEq 𝓔]
+    (F : Over (P.HalfEdgeLabel × 𝓔 × 𝓥)) [DecidableEq F.left] [Fintype F.left]
+    (f : 𝓔 ⟶ P.EdgeLabel) : Decidable (P.DiagramEdgeProp F f) :=
+  @decidable_of_decidable_of_iff _ _
+    (@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
+    (fun _ => @instDecidableAnd _ _ _ (@Fintype.decidablePiFintype _ _
+    (fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _) _)
+    (P.diagramEdgeProp_iff F f).symm
+
+end PreFeynmanRule
+
+/-!
+
+## The definition of Feynman diagrams
+
+We now define the type of Feynman diagrams for a given pre-Feynman rule.
+
+-/
+
+open PreFeynmanRule
+
+/-- The type of Feynman diagrams given a `PreFeynmanRule`. -/
+structure FeynmanDiagram (P : PreFeynmanRule) where
+  /-- The type of edges in the Feynman diagram, labelled by their type. -/
+  𝓔𝓞 : Over P.EdgeLabel
+  /-- The type of vertices in the Feynman diagram, labelled by their type. -/
+  𝓥𝓞 : Over P.VertexLabel
+  /-- The type of half-edges in the Feynman diagram, labelled by their type, the edge it
+  belongs to, and the vertex they belong to. -/
+  𝓱𝓔To𝓔𝓥 : Over (P.HalfEdgeLabel × 𝓔𝓞.left × 𝓥𝓞.left)
+  /-- Each edge has the correct type of half edges. -/
+  𝓔Cond : P.DiagramEdgeProp 𝓱𝓔To𝓔𝓥 𝓔𝓞.hom
+  /-- Each vertex has the correct sort of half edges. -/
+  𝓥Cond : P.DiagramVertexProp 𝓱𝓔To𝓔𝓥 𝓥𝓞.hom
+
+namespace FeynmanDiagram
+
+variable {P : PreFeynmanRule} (F : FeynmanDiagram P)
+
+/-- The type of edges. -/
+def 𝓔 : Type := F.𝓔𝓞.left
+
+/-- The type of vertices. -/
+def 𝓥 : Type := F.𝓥𝓞.left
+
+/-- The type of half-edges. -/
+def 𝓱𝓔 : Type := F.𝓱𝓔To𝓔𝓥.left
+
+/-- The object in Over P.HalfEdgeLabel generated by a Feynman diagram. -/
+def 𝓱𝓔𝓞 : Over P.HalfEdgeLabel := P.toHalfEdge.obj F.𝓱𝓔To𝓔𝓥
+
+/-- The map `F.𝓱𝓔 → F.𝓔` as an object in `Over F.𝓔 `. -/
+def 𝓱𝓔To𝓔 : Over F.𝓔 := P.toEdge.obj F.𝓱𝓔To𝓔𝓥
+
+/-- The map `F.𝓱𝓔 → F.𝓥` as an object in `Over F.𝓥 `. -/
+def 𝓱𝓔To𝓥 : Over F.𝓥 := P.toVertex.obj F.𝓱𝓔To𝓔𝓥
+
+/-!
+
+## Making a Feynman diagram
+
+-/
+
+/-- The condition which must be satisfied by maps to form a Feynman diagram. -/
+def Cond {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) : Prop :=
+  P.DiagramEdgeProp (Over.mk 𝓱𝓔To𝓔𝓥) 𝓔𝓞 ∧
+  P.DiagramVertexProp (Over.mk 𝓱𝓔To𝓔𝓥) 𝓥𝓞
+
+lemma cond_self : Cond F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom :=
+  ⟨F.𝓔Cond, F.𝓥Cond⟩
+
+/-- `Cond` is decidable. -/
+instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel)
+    (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
+    [Fintype 𝓥] [DecidableEq 𝓥] [Fintype 𝓔] [DecidableEq 𝓔] [h : Fintype 𝓱𝓔] [DecidableEq 𝓱𝓔] :
+    Decidable (Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) :=
+  @instDecidableAnd _ _
+    (@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞)
+    (@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞)
+
+/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
+def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
+    (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) : FeynmanDiagram P where
+  𝓔𝓞 := Over.mk 𝓔𝓞
+  𝓥𝓞 := Over.mk 𝓥𝓞
+  𝓱𝓔To𝓔𝓥 := Over.mk 𝓱𝓔To𝓔𝓥
+  𝓔Cond := C.1
+  𝓥Cond := C.2
+
+lemma mk'_self : mk' F.𝓔𝓞.hom F.𝓥𝓞.hom F.𝓱𝓔To𝓔𝓥.hom F.cond_self = F := rfl
+
+/-!
+
+## Finitness of Feynman diagrams
+
+As defined above our Feynman diagrams can have non-finite Types of half-edges etc.
+We define the class of those Feynman diagrams which are `finite` in the appropriate sense.
+In practice, every Feynman diagram considered in the physics literature is `finite`.
+
+This finiteness condition will be used to prove certain `Types` are `Fintype`, and prove
+that certain propositions are decidable.
+
+-/
+
+/-- A set of conditions on a Feynman diagram for it to be considered finite. -/
+class IsFiniteDiagram (F : FeynmanDiagram P) where
+  /-- The type of edges is finite. -/
+  𝓔Fintype : Fintype F.𝓔
+  /-- The type of edges is decidable. -/
+  𝓔DecidableEq : DecidableEq F.𝓔
+  /-- The type of vertices is finite. -/
+  𝓥Fintype : Fintype F.𝓥
+  /-- The type of vertices is decidable. -/
+  𝓥DecidableEq : DecidableEq F.𝓥
+  /-- The type of half-edges is finite. -/
+  𝓱𝓔Fintype : Fintype F.𝓱𝓔
+  /-- The type of half-edges is decidable. -/
+  𝓱𝓔DecidableEq : DecidableEq F.𝓱𝓔
+
+/-- The instance of a finite diagram given explicit finiteness and decidable conditions
+  on the various maps making it up. -/
+instance {𝓔 𝓥 𝓱𝓔 : Type} [h1 : Fintype 𝓔] [h2 : DecidableEq 𝓔]
+    [h3 : Fintype 𝓥] [h4 : DecidableEq 𝓥] [h5 : Fintype 𝓱𝓔] [h6 : DecidableEq 𝓱𝓔]
+    (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
+    (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) (C : Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) :
+    IsFiniteDiagram (mk' 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥 C) :=
+  ⟨h1, h2, h3, h4, h5, h6⟩
+
+/-- If `F` is a finite Feynman diagram, then its edges are finite. -/
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓔 :=
+  IsFiniteDiagram.𝓔Fintype
+
+/-- If `F` is a finite Feynman diagram, then its edges are decidable. -/
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓔 :=
+  IsFiniteDiagram.𝓔DecidableEq
+
+/-- If `F` is a finite Feynman diagram, then its vertices are finite. -/
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓥 :=
+  IsFiniteDiagram.𝓥Fintype
+
+/-- If `F` is a finite Feynman diagram, then its vertices are decidable. -/
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓥 :=
+  IsFiniteDiagram.𝓥DecidableEq
+
+/-- If `F` is a finite Feynman diagram, then its half-edges are finite. -/
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : Fintype F.𝓱𝓔 :=
+  IsFiniteDiagram.𝓱𝓔Fintype
+
+/-- If `F` is a finite Feynman diagram, then its half-edges are decidable. -/
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] : DecidableEq F.𝓱𝓔 :=
+  IsFiniteDiagram.𝓱𝓔DecidableEq
+
+/-- The proposition of whether the given an half-edge and an edge,
+  the edge corresponding to the half edges is the given edge is decidable. -/
+instance {F : FeynmanDiagram P} [IsFiniteDiagram F] (i : F.𝓱𝓔) (j : F.𝓔) :
+    Decidable (F.𝓱𝓔To𝓔.hom i = j) := IsFiniteDiagram.𝓔DecidableEq (F.𝓱𝓔To𝓔.hom i) j
+
+/-- For a finite feynman diagram, the type of half edge lables, edges and vertices
+  is decidable. -/
+instance fintypeProdHalfEdgeLabel𝓔𝓥 {F : FeynmanDiagram P} [IsFinitePreFeynmanRule P]
+    [IsFiniteDiagram F] : DecidableEq (P.HalfEdgeLabel × F.𝓔 × F.𝓥) :=
+  instDecidableEqProd
+
+/-!
+
+## Morphisms of Feynman diagrams
+
+We define a morphism between Feynman diagrams, and properties thereof.
+This will be used to define the category of Feynman diagrams.
+
+-/
+
+/-- Given two maps `F.𝓔 ⟶ G.𝓔` and `F.𝓥 ⟶ G.𝓥` the corresponding map
+  `P.HalfEdgeLabel × F.𝓔 × F.𝓥 → P.HalfEdgeLabel × G.𝓔 × G.𝓥`. -/
+@[simps!]
+def edgeVertexMap {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
+    P.HalfEdgeLabel × F.𝓔 × F.𝓥 → P.HalfEdgeLabel × G.𝓔 × G.𝓥 :=
+  fun x => ⟨x.1, 𝓔 x.2.1, 𝓥 x.2.2⟩
+
+/-- Given equivalences `F.𝓔 ≃ G.𝓔` and `F.𝓥 ≃ G.𝓥`, the induced equivalence between
+  `P.HalfEdgeLabel × F.𝓔 × F.𝓥` and `P.HalfEdgeLabel × G.𝓔 × G.𝓥 ` -/
+def edgeVertexEquiv {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) :
+    P.HalfEdgeLabel × F.𝓔 × F.𝓥 ≃ P.HalfEdgeLabel × G.𝓔 × G.𝓥 where
+  toFun := edgeVertexMap 𝓔.toFun 𝓥.toFun
+  invFun := edgeVertexMap 𝓔.invFun 𝓥.invFun
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
+
+/-- The functor of over-categories generated by `edgeVertexMap`. -/
+@[simps! obj_left obj_hom map_left map_right]
+def edgeVertexFunc {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ⟶ G.𝓔) (𝓥 : F.𝓥 ⟶ G.𝓥) :
+    Over (P.HalfEdgeLabel × F.𝓔 × F.𝓥) ⥤ Over (P.HalfEdgeLabel × G.𝓔 × G.𝓥) :=
+  Over.map <| edgeVertexMap 𝓔 𝓥
+
+/-- A morphism of Feynman diagrams. -/
+structure Hom (F G : FeynmanDiagram P) where
+  /-- The morphism of edge objects. -/
+  𝓔𝓞 : F.𝓔𝓞 ⟶ G.𝓔𝓞
+  /-- The morphism of vertex objects. -/
+  𝓥𝓞 : F.𝓥𝓞 ⟶ G.𝓥𝓞
+  /-- The morphism of half-edge objects. -/
+  𝓱𝓔To𝓔𝓥 : (edgeVertexFunc 𝓔𝓞.left 𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
+
+namespace Hom
+variable {F G : FeynmanDiagram P}
+variable (f : Hom F G)
+
+/-- The map `F.𝓔 → G.𝓔` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓔 : F.𝓔 → G.𝓔 := f.𝓔𝓞.left
+
+/-- The map `F.𝓥 → G.𝓥` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓥 : F.𝓥 → G.𝓥 := f.𝓥𝓞.left
+
+/-- The map `F.𝓱𝓔 → G.𝓱𝓔` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔 := f.𝓱𝓔To𝓔𝓥.left
+
+/-- The morphism `F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞` induced by a homomorphism of Feynman diagrams. -/
+@[simp]
+def 𝓱𝓔𝓞 : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 := P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥
+
+/-- The identity morphism for a Feynman diagram. -/
+def id (F : FeynmanDiagram P) : Hom F F where
+  𝓔𝓞 := 𝟙 F.𝓔𝓞
+  𝓥𝓞 := 𝟙 F.𝓥𝓞
+  𝓱𝓔To𝓔𝓥 := 𝟙 F.𝓱𝓔To𝓔𝓥
+
+/-- The composition of two morphisms of Feynman diagrams. -/
+@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
+def comp {F G H : FeynmanDiagram P} (f : Hom F G) (g : Hom G H) : Hom F H where
+  𝓔𝓞 := f.𝓔𝓞 ≫ g.𝓔𝓞
+  𝓥𝓞 := f.𝓥𝓞 ≫ g.𝓥𝓞
+  𝓱𝓔To𝓔𝓥 := (edgeVertexFunc g.𝓔 g.𝓥).map f.𝓱𝓔To𝓔𝓥 ≫ g.𝓱𝓔To𝓔𝓥
+
+lemma ext' {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔𝓞 = g.𝓔𝓞)
+    (h𝓥 : f.𝓥𝓞 = g.𝓥𝓞) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g := by
+  cases f
+  cases g
+  subst h𝓔 h𝓥
+  simp_all only [mk.injEq, heq_eq_eq, true_and]
+  ext a : 2
+  simp only [𝓱𝓔] at h𝓱𝓔
+  exact congrFun h𝓱𝓔 a
+
+lemma ext {F G : FeynmanDiagram P} {f g : Hom F G} (h𝓔 : f.𝓔 = g.𝓔)
+    (h𝓥 : f.𝓥 = g.𝓥) (h𝓱𝓔 : f.𝓱𝓔 = g.𝓱𝓔) : f = g :=
+  ext' (Over.OverMorphism.ext h𝓔) (Over.OverMorphism.ext h𝓥) h𝓱𝓔
+
+/-- The condition on maps of edges, vertices and half-edges for it to be lifted to a
+  morphism of Feynman diagrams. -/
+def Cond {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Prop :=
+  (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) ∧
+  (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) ∧
+  (∀ x, G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) = edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x))
+
+lemma cond_satisfied {F G : FeynmanDiagram P} (f : Hom F G) :
+    Cond f.𝓔 f.𝓥 f.𝓱𝓔 :=
+  ⟨fun x => congrFun f.𝓔𝓞.w x, fun x => congrFun f.𝓥𝓞.w x, fun x => congrFun f.𝓱𝓔To𝓔𝓥.w x⟩
+
+lemma cond_symm {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔)
+    (h : Cond 𝓔 𝓥 𝓱𝓔) : Cond 𝓔.symm 𝓥.symm 𝓱𝓔.symm := by
+  refine ⟨?_, ?_, fun x => ?_⟩
+  · simpa using fun x => (h.1 (𝓔.symm x)).symm
+  · simpa using fun x => (h.2.1 (𝓥.symm x)).symm
+  · have h1 := h.2.2 (𝓱𝓔.symm x)
+    simp only [Functor.const_obj_obj, Equiv.apply_symm_apply] at h1
+    exact (edgeVertexEquiv 𝓔 𝓥).apply_eq_iff_eq_symm_apply.mp (h1).symm
+
+/-- If `𝓔` is a map between the edges of one finite Feynman diagram and another Feynman diagram,
+  then deciding whether `𝓔` froms a morphism in `Over P.EdgeLabel` between the edge
+  maps is decidable. -/
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
+    (𝓔 : F.𝓔 → G.𝓔) : Decidable (∀ x, G.𝓔𝓞.hom (𝓔 x) = F.𝓔𝓞.hom x) :=
+  @Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓔 P _ _) _
+
+/-- If `𝓥` is a map between the vertices of one finite Feynman diagram and another Feynman diagram,
+  then deciding whether `𝓥` froms a morphism in `Over P.VertexLabel` between the vertex
+  maps is decidable. -/
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFinitePreFeynmanRule P]
+    (𝓥 : F.𝓥 → G.𝓥) : Decidable (∀ x, G.𝓥𝓞.hom (𝓥 x) = F.𝓥𝓞.hom x) :=
+  @Fintype.decidableForallFintype _ _ (fun _ => preFeynmanRuleDecEq𝓥 P _ _) _
+
+/-- Given maps between parts of two Feynman diagrams, it is decidable to determine
+  whether on mapping half-edges, the corresponding half-edge labels, edges and vertices
+  are consistent. -/
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
+    (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) :
+    Decidable (∀ x, G.𝓱𝓔To𝓔𝓥.hom (𝓱𝓔 x) = edgeVertexMap 𝓔 𝓥 (F.𝓱𝓔To𝓔𝓥.hom x)) :=
+  @Fintype.decidableForallFintype _ _ (fun _ => fintypeProdHalfEdgeLabel𝓔𝓥 _ _) _
+
+/-- The condition on whether a map of maps of edges, vertices and half-edges can be
+    lifted to a morphism of Feynman diagrams is decidable. -/
+instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
+    (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
+  instDecidableAnd
+
+/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
+@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
+def mk' {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔)
+    (C : Cond 𝓔 𝓥 𝓱𝓔) : Hom F G where
+  𝓔𝓞 := Over.homMk 𝓔 $ funext C.1
+  𝓥𝓞 := Over.homMk 𝓥 $ funext C.2.1
+  𝓱𝓔To𝓔𝓥 := Over.homMk 𝓱𝓔 $ funext C.2.2
+
+lemma mk'_self {F G : FeynmanDiagram P} (f : Hom F G) :
+    mk' f.𝓔 f.𝓥 f.𝓱𝓔 f.cond_satisfied = f := rfl
+
+end Hom
+
+/-!
+
+## The Category of Feynman diagrams
+
+Feynman diagrams, as defined above, form a category.
+We will be able to use this category to define the symmetry factor of a Feynman diagram,
+and the condition on whether a diagram is connected.
+-/
+
+/-- Feynman diagrams form a category. -/
+@[simps! id_𝓔𝓞_left id_𝓥𝓞_left id_𝓱𝓔To𝓔𝓥_left comp_𝓔𝓞_left comp_𝓥𝓞_left comp_𝓱𝓔To𝓔𝓥_left]
+instance : Category (FeynmanDiagram P) where
+  Hom := Hom
+  id := Hom.id
+  comp := Hom.comp
+
+/-- An isomorphism of Feynman diagrams from isomorphisms of edges, vertices and half-edges. -/
+def mkIso {F G : FeynmanDiagram P} (𝓔 : F.𝓔 ≃ G.𝓔) (𝓥 : F.𝓥 ≃ G.𝓥) (𝓱𝓔 : F.𝓱𝓔 ≃ G.𝓱𝓔)
+    (C : Hom.Cond 𝓔 𝓥 𝓱𝓔) : F ≅ G where
+  hom := Hom.mk' 𝓔 𝓥 𝓱𝓔 C
+  inv := Hom.mk' 𝓔.symm 𝓥.symm 𝓱𝓔.symm (Hom.cond_symm 𝓔 𝓥 𝓱𝓔 C)
+  hom_inv_id := by
+    apply Hom.ext
+    all_goals
+      aesop_cat
+  inv_hom_id := by
+    apply Hom.ext
+    all_goals
+      aesop_cat
+
+/-- The functor from Feynman diagrams to category over edge labels. -/
+def func𝓔𝓞 : FeynmanDiagram P ⥤ Over P.EdgeLabel where
+  obj F := F.𝓔𝓞
+  map f := f.𝓔𝓞
+
+/-- The functor from Feynman diagrams to category over vertex labels. -/
+def func𝓥𝓞 : FeynmanDiagram P ⥤ Over P.VertexLabel where
+  obj F := F.𝓥𝓞
+  map f := f.𝓥𝓞
+
+/-- The functor from Feynman diagrams to category over half-edge labels. -/
+def func𝓱𝓔𝓞 : FeynmanDiagram P ⥤ Over P.HalfEdgeLabel where
+  obj F := F.𝓱𝓔𝓞
+  map f := f.𝓱𝓔𝓞
+
+/-- The functor from Feynman diagrams to `Type` landing on edges. -/
+def func𝓔 : FeynmanDiagram P ⥤ Type where
+  obj F := F.𝓔
+  map f := f.𝓔
+
+/-- The functor from Feynman diagrams to `Type` landing on vertices. -/
+def func𝓥 : FeynmanDiagram P ⥤ Type where
+  obj F := F.𝓥
+  map f := f.𝓥
+
+/-- The functor from Feynman diagrams to `Type` landing on half-edges. -/
+def func𝓱𝓔 : FeynmanDiagram P ⥤ Type where
+  obj F := F.𝓱𝓔
+  map f := f.𝓱𝓔
+
+section symmetryFactor
+/-!
+## Symmetry factors
+
+The symmetry factor of a Feynman diagram is the cardinality of the group of automorphisms of that
+diagram.
+
+We show that the symmetry factor for a finite Feynman diagram is finite.
+
+-/
+
+/-- The type of isomorphisms of a Feynman diagram. -/
+def SymmetryType : Type := F ≅ F
+
+/-- An equivalence between `SymmetryType` and permutation of edges, vertices and half-edges
+  satisfying `Hom.Cond`. -/
+def symmetryTypeEquiv :
+    F.SymmetryType ≃ {S : Equiv.Perm F.𝓔 × Equiv.Perm F.𝓥 × Equiv.Perm F.𝓱𝓔 //
+      Hom.Cond S.1 S.2.1 S.2.2} where
+  toFun f := ⟨⟨(func𝓔.mapIso f).toEquiv, (func𝓥.mapIso f).toEquiv,
+    (func𝓱𝓔.mapIso f).toEquiv⟩, f.1.cond_satisfied⟩
+  invFun S := mkIso S.1.1 S.1.2.1 S.1.2.2 S.2
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- For a finite Feynman diagram, the type of automorphisms of that Feynman diagram is finite. -/
+instance [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : Fintype F.SymmetryType :=
+  Fintype.ofEquiv _ F.symmetryTypeEquiv.symm
+
+/-- The symmetry factor can be defined as the cardinal of the symmetry type.
+  In general this is not a finite number. -/
+@[simp]
+def cardSymmetryFactor : Cardinal := Cardinal.mk (F.SymmetryType)
+
+/-- The symmetry factor of a Finite Feynman diagram, as a natural number. -/
+@[simp]
+def symmetryFactor [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] : ℕ :=
+  (Fintype.card F.SymmetryType)
+
+@[simp]
+lemma symmetryFactor_eq_cardSymmetryFactor [IsFinitePreFeynmanRule P] [IsFiniteDiagram F] :
+    F.symmetryFactor = F.cardSymmetryFactor := by
+  simp only [symmetryFactor, cardSymmetryFactor, Cardinal.mk_fintype]
+
+end symmetryFactor
+
+section connectedness
+/-!
+
+## Connectedness
+
+Given a Feynman diagram we can create a simple graph based on the obvious adjacency relation.
+A feynman diagram is connected if its simple graph is connected.
+
+## TODO
+
+- Complete this section.
+
+-/
+
+/-- A relation on the vertices of Feynman diagrams. The proposition is true if the two
+  vertices are not equal and are connected by a single edge.
+  This is the adjacency relation. -/
+@[simp]
+def AdjRelation : F.𝓥 → F.𝓥 → Prop := fun x y =>
+  x ≠ y ∧
+  ∃ (a b : F.𝓱𝓔), ((F.𝓱𝓔To𝓔𝓥.hom a).2.1 = (F.𝓱𝓔To𝓔𝓥.hom b).2.1
+  ∧ (F.𝓱𝓔To𝓔𝓥.hom a).2.2 = x ∧ (F.𝓱𝓔To𝓔𝓥.hom b).2.2 = y)
+
+/-- The condition on whether two vertices are adjacent is deciable. -/
+instance [IsFiniteDiagram F] : DecidableRel F.AdjRelation := fun _ _ =>
+  @instDecidableAnd _ _ _ $
+  @Fintype.decidableExistsFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
+  (fun _ => @instDecidableAnd _ _ (instDecidableEq𝓔OfIsFiniteDiagram _ _) $
+    @instDecidableAnd _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
+    (instDecidableEq𝓥OfIsFiniteDiagram _ _)) _) _
+
+/-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
+def toSimpleGraph : SimpleGraph F.𝓥 where
+  Adj := AdjRelation F
+  symm := by
+    intro x y h
+    apply And.intro (Ne.symm h.1)
+    obtain ⟨a, b, hab⟩ := h.2
+    use b, a
+    simp_all only [AdjRelation, ne_eq, and_self]
+  loopless := by
+    intro x h
+    simp at h
+
+/-- The adjacency relation for a simple graph created by a finite Feynman diagram
+  is a decidable relation. -/
+instance [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj :=
+  instDecidableRel𝓥AdjRelationOfIsFiniteDiagram F
+
+/-- For a finite feynman diagram it is deciable whether it is preconnected and has
+  the Feynman diagram has a non-empty type of vertices. -/
+instance [IsFiniteDiagram F] :
+  Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) :=
+  @instDecidableAnd _ _ _ $ decidable_of_iff _ Finset.univ_nonempty_iff
+
+/-- For a finite Feynman diagram it is decidable whether the simple graph corresponding to it
+  is connected. -/
+instance [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
+  decidable_of_iff _ (SimpleGraph.connected_iff F.toSimpleGraph).symm
+
+/-- A Feynman diagram is connected if its simple graph is connected. -/
+def Connected : Prop := F.toSimpleGraph.Connected
+
+/-- For a finite Feynman diagram it is decidable whether or not it is connected. -/
+instance [IsFiniteDiagram F] : Decidable (Connected F) :=
+  instDecidableConnected𝓥ToSimpleGraphOfIsFiniteDiagram F
+
+end connectedness
+
+end FeynmanDiagram

HepLean/PerturbationTheory/FeynmanDiagrams/Instances/ComplexScalar.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
+/-!
+# Feynman diagrams in a complex scalar field theory
+
+-/
+
+namespace PhiFour
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+/-- The pre-Feynman rules for a complex scalar theory. -/
+@[simps!]
+def complexScalarFeynmanRules : PreFeynmanRule where
+  /- There is 2 types of `half-edge`. -/
+  HalfEdgeLabel := Fin 2
+  /- There is only 1 type of `edge`. -/
+  EdgeLabel := Fin 1
+  /- There are two types of `vertex`, two external `0` and internal `1`. -/
+  VertexLabel := Fin 3
+  edgeLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0, 1]
+  vertexLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0]
+    | 1 => Over.mk ![1]
+    | 2 => Over.mk ![0, 0, 1, 1]
+
+/-- An instance allowing us to use integers for edge labels for complex scalar theory. -/
+instance (a : ℕ) : OfNat complexScalarFeynmanRules.EdgeLabel a where
+  ofNat := (a : Fin _)
+
+/-- An instance allowing us to use integers for half-edge labels for complex scalar theory. -/
+instance (a : ℕ) : OfNat complexScalarFeynmanRules.HalfEdgeLabel a where
+  ofNat := (a : Fin _)
+
+/-- An instance allowing us to use integers for vertex labels for complex scalar theory. -/
+instance (a : ℕ) : OfNat complexScalarFeynmanRules.VertexLabel a where
+  ofNat := (a : Fin _)
+
+/-- The pre feynman rules for complex scalars are finite. -/
+instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
+  edgeLabelDecidable := instDecidableEqFin _
+  vertexLabelDecidable := instDecidableEqFin _
+  halfEdgeLabelDecidable := instDecidableEqFin _
+  vertexMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+    | 1 => Fin.fintype _
+    | 2 => Fin.fintype _
+  edgeMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+  vertexMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+    | 1 => instDecidableEqFin _
+    | 2 => instDecidableEqFin _
+  edgeMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+
+end PhiFour

HepLean/PerturbationTheory/FeynmanDiagrams/Instances/Phi4.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
+/-!
+# Feynman diagrams in Phi^4 theory
+
+The aim of this file is to start building up the theory of Feynman diagrams in the context of
+Phi^4 theory.
+
+-/
+
+namespace PhiFour
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+/-- The pre-Feynman rules for `Phi^4` theory. -/
+@[simps!]
+def phi4PreFeynmanRules : PreFeynmanRule where
+  /- There is only 1 type of `half-edge`. -/
+  HalfEdgeLabel := Fin 1
+  /- There is only 1 type of `edge`. -/
+  EdgeLabel := Fin 1
+  /- There are two types of `vertex`, external `0` and internal `1`. -/
+  VertexLabel := Fin 2
+  edgeLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0, 0]
+  vertexLabelMap x :=
+    match x with
+    | 0 => Over.mk ![0]
+    | 1 => Over.mk ![0, 0, 0, 0]
+
+/-- An instance allowing us to use integers for edge labels for Phi-4. -/
+instance (a : ℕ) : OfNat phi4PreFeynmanRules.EdgeLabel a where
+  ofNat := (a : Fin _)
+
+/-- An instance allowing us to use integers for half edge labels for Phi-4. -/
+instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
+  ofNat := (a : Fin _)
+
+/-- An instance allowing us to use integers for vertex labels for Phi-4. -/
+instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
+  ofNat := (a : Fin _)
+
+/-- The pre feynman rules for Phi-4 are finite. -/
+instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
+  edgeLabelDecidable := instDecidableEqFin _
+  vertexLabelDecidable := instDecidableEqFin _
+  halfEdgeLabelDecidable := instDecidableEqFin _
+  vertexMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+    | 1 => Fin.fintype _
+  edgeMapFintype := fun v =>
+    match v with
+    | 0 => Fin.fintype _
+  vertexMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+    | 1 => instDecidableEqFin _
+  edgeMapDecidable := fun v =>
+    match v with
+    | 0 => instDecidableEqFin _
+
+/-!
+
+## The figure eight diagram
+
+This section provides an example of the use of Feynman diagrams in HepLean.
+
+-/
+section Example
+
+/-- The figure eight Feynman diagram. -/
+abbrev figureEight : FeynmanDiagram phi4PreFeynmanRules :=
+  mk'
+    ![0, 0] -- edges
+    ![1] -- one internal vertex
+    ![⟨0, 0, 0⟩, ⟨0, 0, 0⟩, ⟨0, 1, 0⟩, ⟨0, 1, 0⟩] -- four half-edges
+    (by decide) -- the condition to form a Feynman diagram.
+
+/-- `figureEight` is connected. We can get this from
+  `#eval Connected figureEight`. -/
+lemma figureEight_connected : Connected figureEight := by decide
+
+/-- The symmetry factor of `figureEight` is 8. We can get this from
+  `#eval symmetryFactor figureEight`. -/
+lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by rfl
+
+end Example
+
+end PhiFour

HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
+import Mathlib.Data.Real.Basic
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.LinearAlgebra.SesquilinearForm
+import Mathlib.LinearAlgebra.Dimension.Finrank
+/-!
+# Momentum in Feynman diagrams
+
+The aim of this file is to associate with each half-edge of a Feynman diagram a momentum,
+and constrain the momentums based conservation at each vertex and edge.
+
+The number of loops of a Feynman diagram is related to the dimension of the resulting
+vector space.
+
+## TODO
+
+- Prove lemmas that make the calculation of the number of loops of a Feynman diagram easier.
+
+## Note
+
+This section is non-computable as we depend on the norm on `F.HalfEdgeMomenta`.
+-/
+
+namespace FeynmanDiagram
+
+open CategoryTheory
+open PreFeynmanRule
+
+variable {P : PreFeynmanRule} (F : FeynmanDiagram P) [IsFiniteDiagram F]
+
+/-!
+
+## Vector spaces associated with momenta in Feynman diagrams.
+
+We define the vector space associated with momenta carried by half-edges,
+outflowing momenta of edges, and inflowing momenta of vertices.
+
+We define the direct sum of the edge and vertex momentum spaces.
+
+-/
+
+/-- The type which assocaites to each half-edge a `1`-dimensional vector space.
+  Corresponding to that spanned by its momentum. -/
+def HalfEdgeMomenta : Type := F.𝓱𝓔 → ℝ
+
+/-- The half momenta carries the structure of an addative commutative group. -/
+instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
+
+/-- The half momenta carries the structure of a module over `ℝ`. Defined via its target. -/
+instance : Module ℝ F.HalfEdgeMomenta := Pi.module _ _ _
+
+/-- An auxiliary function used to define the Euclidean inner product on `F.HalfEdgeMomenta`. -/
+def euclidInnerAux (x : F.HalfEdgeMomenta) : F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
+  toFun y := ∑ i, (x i) * (y i)
+  map_add' z y :=
+    show (∑ i, (x i) * (z i + y i)) = (∑ i, x i * z i) + ∑ i, x i * (y i) by
+      simp only [mul_add, Finset.sum_add_distrib]
+  map_smul' c y :=
+    show (∑ i, x i * (c * y i)) = c * ∑ i, x i * y i by
+      rw [Finset.mul_sum]
+      refine Finset.sum_congr rfl (fun _ _ => by ring)
+
+lemma euclidInnerAux_symm (x y : F.HalfEdgeMomenta) :
+    F.euclidInnerAux x y = F.euclidInnerAux y x := Finset.sum_congr rfl (fun _ _ => by ring)
+
+/-- The Euclidean inner product on `F.HalfEdgeMomenta`. -/
+def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] ℝ where
+  toFun x := F.euclidInnerAux x
+  map_add' x y := by
+    refine LinearMap.ext (fun z => ?_)
+    simp only [euclidInnerAux_symm, map_add, LinearMap.add_apply]
+  map_smul' c x := by
+    refine LinearMap.ext (fun z => ?_)
+    simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply,
+      LinearMap.smul_apply]
+
+/-- The type which associates to each edge a `1`-dimensional vector space.
+  Corresponding to that spanned by its total outflowing momentum. -/
+def EdgeMomenta : Type := F.𝓔 → ℝ
+
+/-- The edge momenta form an addative commuative group. -/
+instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
+
+/-- The edge momenta form a module over `ℝ`. -/
+instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
+
+/-- The type which assocaites to each ege a `1`-dimensional vector space.
+  Corresponding to that spanned by its total inflowing momentum. -/
+def VertexMomenta : Type := F.𝓥 → ℝ
+
+/-- The vertex momenta carries the structure of an addative commuative group. -/
+instance : AddCommGroup F.VertexMomenta := Pi.addCommGroup
+
+/-- The vertex momenta carries the structure of a module over `ℝ`. -/
+instance : Module ℝ F.VertexMomenta := Pi.module _ _ _
+
+/-- The map from `Fin 2` to `Type` landing on `EdgeMomenta` and `VertexMomenta`. -/
+def EdgeVertexMomentaMap : Fin 2 → Type := fun i =>
+  match i with
+  | 0 => F.EdgeMomenta
+  | 1 => F.VertexMomenta
+
+/-- The target of the map `EdgeVertexMomentaMap` is either the type of edge momenta
+  or vertex momenta and thus carries the structure of an addative commuative group. -/
+instance (i : Fin 2) : AddCommGroup (EdgeVertexMomentaMap F i) :=
+  match i with
+  | 0 => instAddCommGroupEdgeMomenta F
+  | 1 => instAddCommGroupVertexMomenta F
+
+/-- The target of the map `EdgeVertexMomentaMap` is either the type of edge momenta
+  or vertex momenta and thus carries the structure of a module over `ℝ`. -/
+instance (i : Fin 2) : Module ℝ (EdgeVertexMomentaMap F i) :=
+  match i with
+  | 0 => instModuleRealEdgeMomenta F
+  | 1 => instModuleRealVertexMomenta F
+
+/-- The direct sum of `EdgeMomenta` and `VertexMomenta`. -/
+def EdgeVertexMomenta : Type := DirectSum (Fin 2) (EdgeVertexMomentaMap F)
+
+/-- The structure of a addative commutative group on `EdgeVertexMomenta` for a
+  Feynman diagram `F`. -/
+instance : AddCommGroup F.EdgeVertexMomenta := DirectSum.instAddCommGroup _
+
+/-- The structure of a module over `ℝ` on `EdgeVertexMomenta` for a Feynman diagram `F`. -/
+instance : Module ℝ F.EdgeVertexMomenta := DirectSum.instModule
+
+/-!
+
+## Linear maps between the vector spaces.
+
+We define various maps into `F.HalfEdgeMomenta`.
+
+In particular, we define a map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta`. This
+map represents the space orthogonal (with respect to the standard Euclidean inner product)
+to the allowed momenta of half-edges (up-to an offset determined by the
+external momenta).
+
+The number of loops of a diagram is defined as the number of half-edges minus
+the rank of this matrix.
+
+-/
+
+/-- The linear map from `F.EdgeMomenta` to `F.HalfEdgeMomenta` induced by
+  the map `F.𝓱𝓔To𝓔.hom`. -/
+def edgeToHalfEdgeMomenta : F.EdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta where
+  toFun x := x ∘ F.𝓱𝓔To𝓔.hom
+  map_add' _ _ := by rfl
+  map_smul' _ _ := by rfl
+
+/-- The linear map from `F.VertexMomenta` to `F.HalfEdgeMomenta` induced by
+  the map `F.𝓱𝓔To𝓥.hom`. -/
+def vertexToHalfEdgeMomenta : F.VertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta where
+  toFun x := x ∘ F.𝓱𝓔To𝓥.hom
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+/-- The linear map from `F.EdgeVertexMomenta` to `F.HalfEdgeMomenta` induced by
+  `F.edgeToHalfEdgeMomenta` and `F.vertexToHalfEdgeMomenta`. -/
+def edgeVertexToHalfEdgeMomenta : F.EdgeVertexMomenta →ₗ[ℝ] F.HalfEdgeMomenta :=
+  DirectSum.toModule ℝ (Fin 2) F.HalfEdgeMomenta
+    (fun i => match i with | 0 => F.edgeToHalfEdgeMomenta | 1 => F.vertexToHalfEdgeMomenta)
+
+/-!
+
+## Submodules
+
+We define submodules of `F.HalfEdgeMomenta` which correspond to
+the orthogonal space to allowed momenta (up-to an offset), and the space of
+allowed momenta.
+
+-/
+
+/-- The submodule of `F.HalfEdgeMomenta` corresponding to the range of
+  `F.edgeVertexToHalfEdgeMomenta`. -/
+def orthogHalfEdgeMomenta : Submodule ℝ F.HalfEdgeMomenta :=
+  LinearMap.range F.edgeVertexToHalfEdgeMomenta
+
+/-- The submodule of `F.HalfEdgeMomenta` corresponding to the allowed momenta. -/
+def allowedHalfEdgeMomenta : Submodule ℝ F.HalfEdgeMomenta :=
+  Submodule.orthogonalBilin F.orthogHalfEdgeMomenta F.euclidInner
+
+/-!
+
+## Number of loops
+
+We define the number of loops of a Feynman diagram as the dimension of the
+allowed space of half-edge momenta.
+
+-/
+
+/-- The number of loops of a Feynman diagram. Defined as the dimension
+  of the space of allowed Half-loop momenta. -/
+noncomputable def numberOfLoops : ℕ := Module.finrank ℝ F.allowedHalfEdgeMomenta
+
+/-!
+
+## Lemmas regarding `numberOfLoops`
+
+We now give a series of lemmas which be used to help calculate the number of loops
+for specific Feynman diagrams.
+
+### TODO
+
+- Complete this section.
+
+-/
+
+/-!
+
+## Category theory
+
+### TODO
+
+- Complete this section.
+
+-/
+
+end FeynmanDiagram

HepLean/PerturbationTheory/Wick/Algebra.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.Wick.Species
+/-!
+
+# Operator algebra
+
+Currently this file is only for an example of Wick strings, correpsonding to a
+theory with two complex scalar fields. The concepts will however generalize.
+
+This file is currently a stub.
+
+We will formally define the operator ring, in terms of the fields present in the theory.
+
+## Futher reading
+
+- https://physics.stackexchange.com/questions/258718/ and links therein
+- Ryan Thorngren (https://physics.stackexchange.com/users/10336/ryan-thorngren), Fermions,
+  different species and (anti-)commutation rules, URL (version: 2019-02-20) :
+  https://physics.stackexchange.com/q/461929
+-/
+
+namespace Wick
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+informal_definition WickAlgebra where
+  math :≈ "
+    Modifications of this may be needed.
+    A structure with the following data:
+    - A ℤ₂-graded algebra A.
+    - A map from `ψ : 𝓔 × SpaceTime → A` where 𝓔 are field colors.
+    - A map `ψc : 𝓔 × SpaceTime → A`.
+    - A map `ψd : 𝓔 × SpaceTime → A`.
+    Subject to the conditions:
+    - The sum of `ψc` and `ψd` is `ψ`.
+    - Two fields super-commute if there colors are not dual to each other.
+    - The super-commutator of two fields is always in the
+      center of the algebra. "
+  physics :≈ "This is defined to be an
+    abstraction of the notion of an operator algebra."
+  ref :≈ "https://physics.stackexchange.com/questions/24157/"
+
+informal_definition WickMonomial where
+  math :≈ "The type of elements of the Wick algebra which is a product of fields."
+  deps :≈ [``WickAlgebra]
+
+namespace WickMonomial
+
+informal_definition toWickAlgebra where
+  math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
+    returns the product of the fields in the monomial."
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+informal_definition timeOrder where
+  math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
+    returns the monomial with the fields time ordered, with the correct sign
+    determined by the Koszul sign factor.
+
+    If two fields have the same time, then their order is preserved e.g.
+    T(ψ₁(t)ψ₂(t)) = ψ₁(t)ψ₂(t)
+    and
+    T(ψ₂(t)ψ₁(t)) = ψ₂(t)ψ₁(t).
+    This allows us to make sense of the construction in e.g.
+    https://www.physics.purdue.edu/~clarkt/Courses/Physics662/ps/qftch32.pdf
+    which permits normal-ordering within time-ordering.
+    "
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+informal_definition normalOrder where
+  math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
+    returns the element in `WickAlgebra` defined as follows
+    - The ψd fields are move to the right.
+    - The ψc fields are moved to the left.
+    - Othewise the order of the fields is preserved."
+  ref :≈ "https://www.imperial.ac.uk/media/imperial-college/research-centres-and-groups/theoretical-physics/msc/current/qft/handouts/qftwickstheorem.pdf"
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+end WickMonomial
+
+informal_definition contraction where
+  math :≈ "Given two `i j : 𝓔 × SpaceTime`, the element of WickAlgebra
+    defined by subtracting the normal ordering of `ψ i ψ j` from the time-ordering of
+    `ψ i ψ j`."
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+informal_lemma contraction_in_center where
+  math :≈ "The contraction of two fields is in the center of the algebra."
+  deps :≈ [``WickAlgebra, ``contraction]
+
+informal_lemma contraction_non_dual_is_zero where
+  math :≈ "The contraction of two fields is zero if the fields are not dual to each other."
+  deps :≈ [``WickAlgebra, ``contraction]
+
+informal_lemma timeOrder_single where
+  math :≈ "The time ordering of a single field is the normal ordering of that field."
+  proof :≈ "Follows from the definitions."
+  deps :≈ [``WickAlgebra, ``WickMonomial.timeOrder, ``WickMonomial.normalOrder]
+
+informal_lemma timeOrder_pair where
+  math :≈ "The time ordering of two fields is the normal ordering of the fields plus the
+    contraction of the fields."
+  proof :≈ "Follows from the definition of contraction."
+  deps :≈ [``WickAlgebra, ``WickMonomial.timeOrder, ``WickMonomial.normalOrder,
+    ``contraction]
+
+informal_definition WickMap where
+  math :≈ "A linear map `vev` from the Wick algebra `A` to the underlying field such that
+   `vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
+  physics :≈ "An abstraction of the notion of a vacuum expectation value, containing
+    the necessary properties for lots of theorems to hold."
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+informal_lemma normalOrder_wickMap where
+  math :≈ "Any normal ordering maps to zero under a Wick map."
+  deps :≈ [``WickMap, ``WickMonomial.normalOrder]
+
+end Wick

HepLean/PerturbationTheory/Wick/Contract.lean

@@ -0,0 +1,662 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.Wick.String
+/-!
+
+# Wick Contract
+
+Currently this file is only for an example of Wick contracts, correpsonding to a
+theory with two complex scalar fields. The concepts will however generalize.
+
+## Further reading
+
+- https://www.imperial.ac.uk/media/imperial-college/research-centres-and-groups/theoretical-physics/msc/current/qft/handouts/qftwickstheorem.pdf
+
+-/
+
+namespace TwoComplexScalar
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+/-- A Wick contraction for a Wick string is a series of pairs `i` and `j` of indices
+  to be contracted, subject to ordering and subject to the condition that they can
+  be contracted. -/
+inductive WickContract : {ni : ℕ} → {i : Fin ni → 𝓔} → {n : ℕ} → {c : Fin n → 𝓔} →
+    {no : ℕ} → {o : Fin no → 𝓔} →
+    (str : WickString i c o final) →
+    {k : ℕ} → (b1 : Fin k → Fin n) → (b2 : Fin k → Fin n) → Type where
+  | string {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} : WickContract str Fin.elim0 Fin.elim0
+  | contr {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} {k : ℕ}
+    {b1 : Fin k → Fin n} {b2 : Fin k → Fin n} : (i : Fin n) →
+    (j : Fin n) → (h : c j = ξ (c i)) →
+    (hilej : i < j) → (hb1 : ∀ r, b1 r < i) → (hb2i : ∀ r, b2 r ≠ i) → (hb2j : ∀ r, b2 r ≠ j) →
+    (w : WickContract str b1 b2) →
+    WickContract str (Fin.snoc b1 i) (Fin.snoc b2 j)
+
+namespace WickContract
+
+/-- The number of nodes of a Wick contraction. -/
+def size {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    WickContract str b1 b2 → ℕ := fun
+  | string => 0
+  | contr _ _ _ _ _ _ _ w => w.size + 1
+
+/-- The number of nodes in a wick contraction tree is the same as `k`. -/
+lemma size_eq_k {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    (w : WickContract str b1 b2) → w.size = k := fun
+  | string => rfl
+  | contr _ _ _ _ _ _ _ w => by
+    simpa [size] using w.size_eq_k
+
+/-- The map giving the vertices on the left-hand-side of a contraction. -/
+@[nolint unusedArguments]
+def boundFst {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    WickContract str b1 b2 → Fin k → Fin n := fun _ => b1
+
+@[simp]
+lemma boundFst_contr_castSucc {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    (h : c j = ξ (c i))
+    (hilej : i < j)
+    (hb1 : ∀ r, b1 r < i)
+    (hb2i : ∀ r, b2 r ≠ i)
+    (hb2j : ∀ r, b2 r ≠ j)
+    (w : WickContract str b1 b2) (r : Fin k) :
+    (contr i j h hilej hb1 hb2i hb2j w).boundFst r.castSucc = w.boundFst r := by
+  simp only [boundFst, Fin.snoc_castSucc]
+
+@[simp]
+lemma boundFst_contr_last {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    (h : c j = ξ (c i))
+    (hilej : i < j)
+    (hb1 : ∀ r, b1 r < i)
+    (hb2i : ∀ r, b2 r ≠ i)
+    (hb2j : ∀ r, b2 r ≠ j)
+    (w : WickContract str b1 b2) :
+    (contr i j h hilej hb1 hb2i hb2j w).boundFst (Fin.last k) = i := by
+  simp only [boundFst, Fin.snoc_last]
+
+lemma boundFst_strictMono {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → StrictMono w.boundFst := fun
+  | string => fun k => Fin.elim0 k
+  | contr i j _ _ hb1 _ _ w => by
+    intro r s hrs
+    rcases Fin.eq_castSucc_or_eq_last r with hr | hr
+    · obtain ⟨r, hr⟩ := hr
+      subst hr
+      rcases Fin.eq_castSucc_or_eq_last s with hs | hs
+      · obtain ⟨s, hs⟩ := hs
+        subst hs
+        simp only [boundFst_contr_castSucc]
+        apply w.boundFst_strictMono _
+        simpa using hrs
+      · subst hs
+        simp only [boundFst_contr_castSucc, boundFst_contr_last]
+        exact hb1 r
+    · subst hr
+      rcases Fin.eq_castSucc_or_eq_last s with hs | hs
+      · obtain ⟨s, hs⟩ := hs
+        subst hs
+        rw [Fin.lt_def] at hrs
+        simp only [Fin.val_last, Fin.coe_castSucc] at hrs
+        omega
+      · subst hs
+        simp at hrs
+
+/-- The map giving the vertices on the right-hand-side of a contraction. -/
+@[nolint unusedArguments]
+def boundSnd {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    WickContract str b1 b2 → Fin k → Fin n := fun _ => b2
+
+@[simp]
+lemma boundSnd_contr_castSucc {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    (h : c j = ξ (c i))
+    (hilej : i < j)
+    (hb1 : ∀ r, b1 r < i)
+    (hb2i : ∀ r, b2 r ≠ i)
+    (hb2j : ∀ r, b2 r ≠ j)
+    (w : WickContract str b1 b2) (r : Fin k) :
+    (contr i j h hilej hb1 hb2i hb2j w).boundSnd r.castSucc = w.boundSnd r := by
+  simp only [boundSnd, Fin.snoc_castSucc]
+
+@[simp]
+lemma boundSnd_contr_last {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    (h : c j = ξ (c i))
+    (hilej : i < j)
+    (hb1 : ∀ r, b1 r < i)
+    (hb2i : ∀ r, b2 r ≠ i)
+    (hb2j : ∀ r, b2 r ≠ j)
+    (w : WickContract str b1 b2) :
+    (contr i j h hilej hb1 hb2i hb2j w).boundSnd (Fin.last k) = j := by
+  simp only [boundSnd, Fin.snoc_last]
+
+lemma boundSnd_injective {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    (w : WickContract str b1 b2) → Function.Injective w.boundSnd := fun
+  | string => by
+    intro i j _
+    exact Fin.elim0 i
+  | contr i j hij hilej hi h2i h2j w => by
+    intro r s hrs
+    rcases Fin.eq_castSucc_or_eq_last r with hr | hr
+    · obtain ⟨r, hr⟩ := hr
+      subst hr
+      rcases Fin.eq_castSucc_or_eq_last s with hs | hs
+      · obtain ⟨s, hs⟩ := hs
+        subst hs
+        simp only [boundSnd_contr_castSucc] at hrs
+        simpa using w.boundSnd_injective hrs
+      · subst hs
+        simp only [boundSnd_contr_castSucc, boundSnd_contr_last] at hrs
+        exact False.elim (h2j r hrs)
+    · subst hr
+      rcases Fin.eq_castSucc_or_eq_last s with hs | hs
+      · obtain ⟨s, hs⟩ := hs
+        subst hs
+        simp only [boundSnd_contr_last, boundSnd_contr_castSucc] at hrs
+        exact False.elim (h2j s hrs.symm)
+      · subst hs
+        rfl
+
+lemma color_boundSnd_eq_dual_boundFst {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    (w : WickContract str b1 b2) → (i : Fin k) → c (w.boundSnd i) = ξ (c (w.boundFst i)) := fun
+  | string => fun i => Fin.elim0 i
+  | contr i j hij hilej hi _ _ w => fun r => by
+    rcases Fin.eq_castSucc_or_eq_last r with hr | hr
+    · obtain ⟨r, hr⟩ := hr
+      subst hr
+      simpa using w.color_boundSnd_eq_dual_boundFst r
+    · subst hr
+      simpa using hij
+
+lemma boundFst_lt_boundSnd {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → (i : Fin k) →
+    w.boundFst i < w.boundSnd i := fun
+  | string => fun i => Fin.elim0 i
+  | contr i j hij hilej hi _ _ w => fun r => by
+    rcases Fin.eq_castSucc_or_eq_last r with hr | hr
+    · obtain ⟨r, hr⟩ := hr
+      subst hr
+      simpa using w.boundFst_lt_boundSnd r
+    · subst hr
+      simp only [boundFst_contr_last, boundSnd_contr_last]
+      exact hilej
+
+lemma boundFst_neq_boundSnd {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    (w : WickContract str b1 b2) → (r1 r2 : Fin k) → b1 r1 ≠ b2 r2 := fun
+  | string => fun i => Fin.elim0 i
+  | contr i j _ hilej h1 h2i h2j w => fun r s => by
+    rcases Fin.eq_castSucc_or_eq_last r with hr | hr
+      <;> rcases Fin.eq_castSucc_or_eq_last s with hs | hs
+    · obtain ⟨r, hr⟩ := hr
+      obtain ⟨s, hs⟩ := hs
+      subst hr hs
+      simpa using w.boundFst_neq_boundSnd r s
+    · obtain ⟨r, hr⟩ := hr
+      subst hr hs
+      simp only [Fin.snoc_castSucc, Fin.snoc_last, ne_eq]
+      have hn := h1 r
+      omega
+    · obtain ⟨s, hs⟩ := hs
+      subst hr hs
+      simp only [Fin.snoc_last, Fin.snoc_castSucc, ne_eq]
+      exact (h2i s).symm
+    · subst hr hs
+      simp only [Fin.snoc_last, ne_eq]
+      omega
+
+/-- Casts a Wick contraction from `WickContract str b1 b2` to `WickContract str b1' b2'` with a
+  proof that `b1 = b1'` and `b2 = b2'`, and that they are defined from the same `k = k'`. -/
+def castMaps {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k k' : ℕ} {b1 b2 : Fin k → Fin n} {b1' b2' : Fin k' → Fin n}
+    (hk : k = k')
+    (hb1 : b1 = b1' ∘ Fin.cast hk) (hb2 : b2 = b2' ∘ Fin.cast hk) (w : WickContract str b1 b2) :
+    WickContract str b1' b2' :=
+  cast (by subst hk; rfl) (hb2 ▸ hb1 ▸ w)
+
+@[simp]
+lemma castMaps_rfl {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+    castMaps rfl rfl rfl w = w := rfl
+
+lemma mem_snoc' {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1' b2' : Fin k → Fin n} :
+    (w : WickContract str b1' b2') →
+    {k' : ℕ} → (hk' : k'.succ = k) →
+    (b1 b2 : Fin k' → Fin n) → (i j : Fin n) → (h : c j = ξ (c i)) →
+    (hilej : i < j) → (hb1 : ∀ r, b1 r < i) → (hb2i : ∀ r, b2 r ≠ i) → (hb2j : ∀ r, b2 r ≠ j) →
+    (hb1' : Fin.snoc b1 i = b1' ∘ Fin.cast hk') →
+    (hb2' : Fin.snoc b2 j = b2' ∘ Fin.cast hk') →
+    ∃ (w' : WickContract str b1 b2), w = castMaps hk' hb1' hb2' (
+      contr i j h hilej hb1 hb2i hb2j w') := fun
+  | string => fun hk' => by
+    simp at hk'
+  | contr i' j' h' hilej' hb1' hb2i' hb2j' w' => by
+    intro hk b1 b2 i j h hilej hb1 hb2i hb2j hb1' hb2'
+    rename_i k' k b1' b2' f
+    have hk2 : k' = k := Nat.succ_inj'.mp hk
+    subst hk2
+    simp_all
+    have hb2'' : b2 = b2' := by
+      funext k
+      trans (@Fin.snoc k' (fun _ => Fin n) b2 j) (Fin.castSucc k)
+      · simp
+      · rw [hb2']
+        simp
+    have hb1'' : b1 = b1' := by
+      funext k
+      trans (@Fin.snoc k' (fun _ => Fin n) b1 i) (Fin.castSucc k)
+      · simp
+      · rw [hb1']
+        simp
+    have hi : i = i' := by
+      trans (@Fin.snoc k' (fun _ => Fin n) b1 i) (Fin.last k')
+      · simp
+      · rw [hb1']
+        simp
+    have hj : j = j' := by
+      trans (@Fin.snoc k' (fun _ => Fin n) b2 j) (Fin.last k')
+      · simp
+      · rw [hb2']
+        simp
+    subst hb1'' hb2'' hi hj
+    simp
+
+lemma mem_snoc {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (i j : Fin n) (h : c j = ξ (c i)) (hilej : i < j) (hb1 : ∀ r, b1 r < i)
+    (hb2i : ∀ r, b2 r ≠ i) (hb2j : ∀ r, b2 r ≠ j)
+    (w : WickContract str (Fin.snoc b1 i) (Fin.snoc b2 j)) :
+    ∃ (w' : WickContract str b1 b2), w = contr i j h hilej hb1 hb2i hb2j w' := by
+  exact mem_snoc' w rfl b1 b2 i j h hilej hb1 hb2i hb2j rfl rfl
+
+lemma is_subsingleton {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    Subsingleton (WickContract str b1 b2) := Subsingleton.intro fun w1 w2 => by
+  induction k with
+  | zero =>
+    have hb1 : b1 = Fin.elim0 := Subsingleton.elim _ _
+    have hb2 : b2 = Fin.elim0 := Subsingleton.elim _ _
+    subst hb1 hb2
+    match w1, w2 with
+    | string, string => rfl
+  | succ k hI =>
+    match w1, w2 with
+    | contr i j h hilej hb1 hb2i hb2j w, w2 =>
+      let ⟨w', hw'⟩ := mem_snoc i j h hilej hb1 hb2i hb2j w2
+      rw [hw']
+      apply congrArg (contr i j _ _ _ _ _) (hI w w')
+
+lemma eq_snoc_castSucc {k n : ℕ} (b1 : Fin k.succ → Fin n) :
+    b1 = Fin.snoc (b1 ∘ Fin.castSucc) (b1 (Fin.last k)) := by
+  funext i
+  rcases Fin.eq_castSucc_or_eq_last i with h1 | h1
+  · obtain ⟨i, rfl⟩ := h1
+    simp
+  · subst h1
+    simp
+
+/-- The construction of a Wick contraction from maps `b1 b2 : Fin k → Fin n`, with the former
+  giving the first index to be contracted, and the latter the second index. These
+  maps must satisfy a series of conditions. -/
+def fromMaps {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} (b1 b2 : Fin k → Fin n)
+    (hi : ∀ i, c (b2 i) = ξ (c (b1 i)))
+    (hb1ltb2 : ∀ i, b1 i < b2 i)
+    (hb1 : StrictMono b1)
+    (hb1neb2 : ∀ r1 r2, b1 r1 ≠ b2 r2)
+    (hb2 : Function.Injective b2) :
+    WickContract str b1 b2 := by
+  match k with
+  | 0 =>
+    refine castMaps ?_ ?_ ?_ string
+    · rfl
+    · exact funext (fun i => Fin.elim0 i)
+    · exact funext (fun i => Fin.elim0 i)
+  | Nat.succ k =>
+    refine castMaps rfl (eq_snoc_castSucc b1).symm (eq_snoc_castSucc b2).symm
+      (contr (b1 (Fin.last k)) (b2 (Fin.last k))
+        (hi (Fin.last k))
+        (hb1ltb2 (Fin.last k))
+        (fun r => hb1 (Fin.castSucc_lt_last r))
+        (fun r a => hb1neb2 (Fin.last k) r.castSucc a.symm)
+        (fun r => hb2.eq_iff.mp.mt (Fin.ne_last_of_lt (Fin.castSucc_lt_last r)))
+      (fromMaps (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc) (fun i => hi (Fin.castSucc i))
+        (fun i => hb1ltb2 (Fin.castSucc i)) (StrictMono.comp hb1 Fin.strictMono_castSucc)
+        ?_ ?_))
+    · exact fun r1 r2 => hb1neb2 r1.castSucc r2.castSucc
+    · exact Function.Injective.comp hb2 (Fin.castSucc_injective k)
+
+/-- Given a Wick contraction with `k.succ` contractions, returns the Wick contraction with
+  `k` contractions by dropping the last contraction (defined by the first index contracted). -/
+def dropLast {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k.succ → Fin n}
+    (w : WickContract str b1 b2) : WickContract str (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc) :=
+  fromMaps (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc)
+    (fun i => color_boundSnd_eq_dual_boundFst w i.castSucc)
+    (fun i => boundFst_lt_boundSnd w i.castSucc)
+    (StrictMono.comp w.boundFst_strictMono Fin.strictMono_castSucc)
+    (fun r1 r2 => boundFst_neq_boundSnd w r1.castSucc r2.castSucc)
+    (Function.Injective.comp w.boundSnd_injective (Fin.castSucc_injective k))
+
+lemma eq_from_maps {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) :
+    w = fromMaps w.boundFst w.boundSnd w.color_boundSnd_eq_dual_boundFst
+      w.boundFst_lt_boundSnd w.boundFst_strictMono w.boundFst_neq_boundSnd
+      w.boundSnd_injective := is_subsingleton.allEq w _
+
+lemma eq_dropLast_contr {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k.succ → Fin n} (w : WickContract str b1 b2) :
+  w = castMaps rfl (eq_snoc_castSucc b1).symm (eq_snoc_castSucc b2).symm
+    (contr (b1 (Fin.last k)) (b2 (Fin.last k))
+      (w.color_boundSnd_eq_dual_boundFst (Fin.last k))
+      (w.boundFst_lt_boundSnd (Fin.last k))
+      (fun r => w.boundFst_strictMono (Fin.castSucc_lt_last r))
+      (fun r a => w.boundFst_neq_boundSnd (Fin.last k) r.castSucc a.symm)
+      (fun r => w.boundSnd_injective.eq_iff.mp.mt (Fin.ne_last_of_lt (Fin.castSucc_lt_last r)))
+    (dropLast w)) := by
+  rw [eq_from_maps w]
+  rfl
+
+/-- Wick contractions of a given Wick string with `k` different contractions. -/
+def Level {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} (str : WickString i c o final) (k : ℕ) : Type :=
+  Σ (b1 : Fin k → Fin n) (b2 : Fin k → Fin n), WickContract str b1 b2
+
+/-- There is a finite number of Wick contractions with no contractions. In particular,
+  this is just the original Wick string. -/
+instance levelZeroFintype {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} (str : WickString i c o final) :
+    Fintype (Level str 0) where
+  elems := {⟨Fin.elim0, Fin.elim0, WickContract.string⟩}
+  complete := by
+    intro x
+    match x with
+    | ⟨b1, b2, w⟩ =>
+      have hb1 : b1 = Fin.elim0 := Subsingleton.elim _ _
+      have hb2 : b2 = Fin.elim0 := Subsingleton.elim _ _
+      subst hb1 hb2
+      simp only [Finset.mem_singleton]
+      rw [is_subsingleton.allEq w string]
+
+/-- The pairs of additional indices which can be contracted given a Wick contraction. -/
+structure ContrPair {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) where
+  /-- The first index in the contraction pair. -/
+  i : Fin n
+  /-- The second index in the contraction pair. -/
+  j : Fin n
+  h : c j = ξ (c i)
+  hilej : i < j
+  hb1 : ∀ r, b1 r < i
+  hb2i : ∀ r, b2 r ≠ i
+  hb2j : ∀ r, b2 r ≠ j
+
+/-- The pairs of additional indices which can be contracted, given an existing wick contraction,
+  is equivalent to the a subtype of `Fin n × Fin n` defined by certain conditions equivalent
+  to the conditions appearing in `ContrPair`. -/
+def contrPairEquivSubtype {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+    ContrPair w ≃ {x : Fin n × Fin n // c x.2 = ξ (c x.1) ∧ x.1 < x.2 ∧
+      (∀ r, b1 r < x.1) ∧ (∀ r, b2 r ≠ x.1) ∧ (∀ r, b2 r ≠ x.2)} where
+  toFun cp := ⟨⟨cp.i, cp.j⟩, ⟨cp.h, cp.hilej, cp.hb1, cp.hb2i, cp.hb2j⟩⟩
+  invFun x :=
+    match x with
+    | ⟨⟨i, j⟩, ⟨h, hilej, hb1, hb2i, hb2j⟩⟩ => ⟨i, j, h, hilej, hb1, hb2i, hb2j⟩
+  left_inv x := by rfl
+  right_inv x := by
+    simp_all only [ne_eq]
+    obtain ⟨val, property⟩ := x
+    obtain ⟨fst, snd⟩ := val
+    obtain ⟨left, right⟩ := property
+    obtain ⟨left_1, right⟩ := right
+    obtain ⟨left_2, right⟩ := right
+    obtain ⟨left_3, right⟩ := right
+    simp_all only [ne_eq]
+
+lemma heq_eq {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 b1' b2' : Fin k → Fin n}
+    (w : WickContract str b1 b2)
+    (w' : WickContract str b1' b2') (h1 : b1 = b1') (h2 : b2 = b2') : HEq w w':= by
+  subst h1 h2
+  simp only [heq_eq_eq]
+  exact is_subsingleton.allEq w w'
+
+/-- The equivalence between Wick contractions consisting of `k.succ` contractions and
+  those with `k` contractions paired with a suitable contraction pair. -/
+def levelSuccEquiv {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} (str : WickString i c o final) (k : ℕ) :
+    Level str k.succ ≃ (w : Level str k) × ContrPair w.2.2 where
+  toFun w :=
+    match w with
+    | ⟨b1, b2, w⟩ =>
+    ⟨⟨b1 ∘ Fin.castSucc, b2 ∘ Fin.castSucc, dropLast w⟩,
+      ⟨b1 (Fin.last k), b2 (Fin.last k),
+      w.color_boundSnd_eq_dual_boundFst (Fin.last k),
+      w.boundFst_lt_boundSnd (Fin.last k),
+      fun r => w.boundFst_strictMono (Fin.castSucc_lt_last r),
+      fun r a => w.boundFst_neq_boundSnd (Fin.last k) r.castSucc a.symm,
+      fun r => w.boundSnd_injective.eq_iff.mp.mt (Fin.ne_last_of_lt (Fin.castSucc_lt_last r))⟩⟩
+  invFun w :=
+    match w with
+    | ⟨⟨b1, b2, w⟩, cp⟩ => ⟨Fin.snoc b1 cp.i, Fin.snoc b2 cp.j,
+      contr cp.i cp.j cp.h cp.hilej cp.hb1 cp.hb2i cp.hb2j w⟩
+  left_inv w := by
+    match w with
+    | ⟨b1, b2, w⟩ =>
+      simp only [Nat.succ_eq_add_one, Function.comp_apply]
+      congr
+      · exact Eq.symm (eq_snoc_castSucc b1)
+      · funext b2
+        congr
+        exact Eq.symm (eq_snoc_castSucc b1)
+      · exact Eq.symm (eq_snoc_castSucc b2)
+      · rw [eq_dropLast_contr w]
+        simp only [castMaps, Nat.succ_eq_add_one, cast_eq, heq_eqRec_iff_heq, heq_eq_eq,
+          contr.injEq]
+        rfl
+  right_inv w := by
+    match w with
+    | ⟨⟨b1, b2, w⟩, cp⟩ =>
+      simp only [Nat.succ_eq_add_one, Fin.snoc_last, Sigma.mk.inj_iff]
+      apply And.intro
+      · congr
+        · exact Fin.snoc_comp_castSucc
+        · funext b2
+          congr
+          exact Fin.snoc_comp_castSucc
+        · exact Fin.snoc_comp_castSucc
+        · exact heq_eq _ _ Fin.snoc_comp_castSucc Fin.snoc_comp_castSucc
+      · congr
+        · exact Fin.snoc_comp_castSucc
+        · exact Fin.snoc_comp_castSucc
+        · exact heq_eq _ _ Fin.snoc_comp_castSucc Fin.snoc_comp_castSucc
+        · simp
+        · simp
+        · simp
+
+/-- The sum of `boundFst` and `boundSnd`, giving on `Sum.inl k` the first index
+  in the `k`th contraction, and on `Sum.inr k` the second index in the `k`th contraction. -/
+def bound {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) : Fin k ⊕ Fin k → Fin n :=
+  Sum.elim w.boundFst w.boundSnd
+
+/-- On `Sum.inl k` the map `bound` acts via `boundFst`. -/
+@[simp]
+lemma bound_inl {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) (i : Fin k) : w.bound (Sum.inl i) = w.boundFst i := rfl
+
+/-- On `Sum.inr k` the map `bound` acts via `boundSnd`. -/
+@[simp]
+lemma bound_inr {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) (i : Fin k) : w.bound (Sum.inr i) = w.boundSnd i := rfl
+
+lemma bound_injection {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) : Function.Injective w.bound := by
+  intro x y h
+  match x, y with
+  | Sum.inl x, Sum.inl y =>
+    simp only [bound_inl] at h
+    simpa using (StrictMono.injective w.boundFst_strictMono).eq_iff.mp h
+  | Sum.inr x, Sum.inr y =>
+    simp only [bound_inr] at h
+    simpa using w.boundSnd_injective h
+  | Sum.inl x, Sum.inr y =>
+    simp only [bound_inl, bound_inr] at h
+    exact False.elim (w.boundFst_neq_boundSnd x y h)
+  | Sum.inr x, Sum.inl y =>
+    simp only [bound_inr, bound_inl] at h
+    exact False.elim (w.boundFst_neq_boundSnd y x h.symm)
+
+lemma bound_le_total {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) : 2 * k ≤ n := by
+  refine Fin.nonempty_embedding_iff.mp ⟨w.bound ∘ finSumFinEquiv.symm ∘ Fin.cast (Nat.two_mul k),
+    ?_⟩
+  apply Function.Injective.comp (Function.Injective.comp _ finSumFinEquiv.symm.injective)
+  · exact Fin.cast_injective (Nat.two_mul k)
+  · exact bound_injection w
+
+/-- The list of fields (indexed by `Fin n`) in a Wick contraction which are not bound,
+  i.e. which do not appear in any contraction. -/
+def unboundList {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) : List (Fin n) :=
+  List.filter (fun i => decide (∀ r, w.bound r ≠ i)) (List.finRange n)
+
+/-- THe list of field positions which are not contracted has no duplicates. -/
+lemma unboundList_nodup {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) : (w.unboundList).Nodup :=
+    List.Nodup.filter _ (List.nodup_finRange n)
+
+/-- The length of the `unboundList` is equal to `n - 2 * k`. That is
+  the total number of fields minus the number of contracted fields. -/
+lemma unboundList_length {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+    w.unboundList.length = n - 2 * k := by
+  rw [← List.Nodup.dedup w.unboundList_nodup]
+  rw [← List.card_toFinset, unboundList]
+  rw [List.toFinset_filter, List.toFinset_finRange]
+  have hn := Finset.filter_card_add_filter_neg_card_eq_card (s := Finset.univ)
+    (fun (i : Fin n) => i ∈ Finset.image w.bound Finset.univ)
+  have hn' :(Finset.filter (fun i => i ∈ Finset.image w.bound Finset.univ) Finset.univ).card =
+      (Finset.image w.bound Finset.univ).card := by
+    refine Finset.card_equiv (Equiv.refl _) fun i => ?_
+    simp
+  rw [hn'] at hn
+  rw [Finset.card_image_of_injective] at hn
+  simp only [Finset.card_univ, Fintype.card_sum, Fintype.card_fin,
+    Finset.mem_univ, true_and, Sum.exists, bound_inl, bound_inr, not_or, not_exists] at hn
+  have hn'' : (Finset.filter (fun a => a ∉ Finset.image w.bound Finset.univ) Finset.univ).card =
+      n - 2 * k := by
+    omega
+  rw [← hn'']
+  congr
+  funext x
+  simp only [ne_eq, Sum.forall, bound_inl, bound_inr, Bool.decide_and, Bool.and_eq_true,
+    decide_eq_true_eq, Finset.mem_image, Finset.mem_univ, true_and, Sum.exists, not_or, not_exists]
+  exact bound_injection w
+
+lemma unboundList_sorted {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+    List.Sorted (fun i j => i < j) w.unboundList :=
+  List.Pairwise.sublist (List.filter_sublist (List.finRange n)) (List.pairwise_lt_finRange n)
+
+/-- The ordered embedding giving the fields which are not bound in a contraction. These
+  are the fields that will appear in a normal operator in Wick's theorem. -/
+def unbound {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
+    (w : WickContract str b1 b2) : Fin (n - 2 * k) ↪o Fin n where
+  toFun := w.unboundList.get ∘ Fin.cast w.unboundList_length.symm
+  inj' := by
+    apply Function.Injective.comp
+    · rw [← List.nodup_iff_injective_get]
+      exact w.unboundList_nodup
+    · exact Fin.cast_injective _
+  map_rel_iff' := by
+    refine fun {a b} => StrictMono.le_iff_le ?_
+    rw [Function.Embedding.coeFn_mk]
+    apply StrictMono.comp
+    · exact List.Sorted.get_strictMono w.unboundList_sorted
+    · exact fun ⦃a b⦄ a => a
+
+informal_lemma level_fintype where
+  math :≈ "Level is a finite type, as there are only finitely many ways to contract a Wick string."
+  deps :≈ [``Level]
+
+informal_definition HasEqualTimeContractions where
+  math :≈ "The condition for a Wick contraction to have two fields contracted
+    which are of equal time, i.e. come from the same vertex."
+  deps :≈ [``WickContract]
+
+informal_definition IsConnected where
+  math :≈ "The condition for a full Wick contraction that for any two vertices
+    (including external vertices) are connected by contractions."
+  deps :≈ [``WickContract]
+
+informal_definition HasVacuumContributions where
+  math :≈ "The condition for a full Wick contraction to have a vacuum contribution."
+  deps :≈ [``WickContract]
+
+informal_definition IsOneParticleIrreducible where
+  math :≈ "The condition for a full Wick contraction to be one-particle irreducible."
+  deps :≈ [``WickContract]
+
+end WickContract
+
+end TwoComplexScalar

HepLean/PerturbationTheory/Wick/MomentumSpace.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.Wick.Contract
+/-!
+
+# Wick contraction in momentum space
+
+Every complete Wick contraction leads to a function on momenta, following
+the Feynman rules.
+
+-/
+
+namespace Wick
+
+informal_definition toMomentumTensorTree where
+  math :≈ "A function which takes a Wick contraction,
+    and corresponding momenta, and outputs the corresponding
+    tensor tree associated with that contraction. The rules for how this is done
+    is given by the `Feynman rules`.
+    The appropriate ring to consider here is a ring permitting the abstract notion of a
+    Dirac delta function. "
+  ref :≈ "
+    Some references for Feynman rules are:
+    - QED Feynman rules: http://hitoshi.berkeley.edu/public_html/129A/point.pdf,
+    - Weyl Fermions: http://scipp.ucsc.edu/~haber/susybook/feyn115.pdf."
+
+informal_definition toMomentumTensor where
+  math :≈ "The tensor associated to `toMomentumTensorTree` associated with a Wick contraction,
+    and corresponding internal momenta, and external momenta."
+  deps :≈ [``toMomentumTensorTree]
+
+end Wick

HepLean/PerturbationTheory/Wick/PositionSpace.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
+import HepLean.Meta.Informal
+/-!
+
+# Wick contraction in position space
+
+Every complete Wick contraction leads to a function on positions, following
+the Feynman rules.
+
+## Further reading
+
+The following reference provides a good resource for Wick contractions of external fields.
+- http://www.dylanjtemples.com:82/solutions/QFT_Solution_I-6.pdf
+
+-/
+
+namespace Wick
+
+
+end Wick

HepLean/PerturbationTheory/Wick/Species.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
+import HepLean.Meta.Informal
+/-!
+
+# Wick Species
+
+Note: There is very likely a much better name for what we here call a Wick Species.
+
+A Wick Species is a structure containing the basic information needed to write wick contractions
+for a theory, and calculate their corresponding Feynman diagrams.
+
+-/
+
+/-! TODO: There should be some sort of notion of a group action on a Wick Species. -/
+namespace Wick
+
+/-- The basic structure needed to write down Wick contractions for a theory and
+  calculate the corresponding Feynman diagrams.
+
+  WARNING: This definition is not yet complete.
+   -/
+structure Species where
+  /-- The color of Field operators which appear in a theory. -/
+  𝓕 : Type
+  /-- The map taking a field operator to its dual operator. -/
+  ξ : 𝓕 → 𝓕
+  /-- The condition that `ξ` is an involution. -/
+  ξ_involutive : Function.Involutive ξ
+  /-- The color of vertices which appear in a theory. -/
+  𝓥 : Type
+  /-- The edges each vertex corresponds to. -/
+  𝓥Fields : 𝓥 → Σ n, Fin n → 𝓕
+
+end Wick

HepLean/PerturbationTheory/Wick/String.lean

@@ -0,0 +1,196 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.Wick.Species
+/-!
+# Wick strings
+
+Currently this file is only for an example of Wick strings, correpsonding to a
+theory with two complex scalar fields. The concepts will however generalize.
+
+A wick string is defined to be a sequence of input fields,
+followed by a squence of vertices, followed by a sequence of output fields.
+
+A wick string can be combined with an appropriate map to spacetime to produce a specific
+term in the ring of operators. This has yet to be implemented.
+
+-/
+
+namespace TwoComplexScalar
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+/-- The colors of edges which one can associate with a vertex for a theory
+  with two complex scalar fields. -/
+inductive 𝓔 where
+  /-- Corresponds to the first complex scalar field flowing out of a vertex. -/
+  | complexScalarOut₁ : 𝓔
+  /-- Corresponds to the first complex scalar field flowing into a vertex. -/
+  | complexScalarIn₁ : 𝓔
+  /-- Corresponds to the second complex scalar field flowing out of a vertex. -/
+  | complexScalarOut₂ : 𝓔
+  /-- Corresponds to the second complex scalar field flowing into a vertex. -/
+  | complexScalarIn₂ : 𝓔
+
+/-- The map taking each color to it's dual, specifying how we can contract edges. -/
+def ξ : 𝓔 → 𝓔
+  | 𝓔.complexScalarOut₁ => 𝓔.complexScalarIn₁
+  | 𝓔.complexScalarIn₁ => 𝓔.complexScalarOut₁
+  | 𝓔.complexScalarOut₂ => 𝓔.complexScalarIn₂
+  | 𝓔.complexScalarIn₂ => 𝓔.complexScalarOut₂
+
+/-- The function `ξ` is an involution. -/
+lemma ξ_involutive : Function.Involutive ξ := by
+  intro x
+  match x with
+  | 𝓔.complexScalarOut₁ => rfl
+  | 𝓔.complexScalarIn₁ => rfl
+  | 𝓔.complexScalarOut₂ => rfl
+  | 𝓔.complexScalarIn₂ => rfl
+
+/-- The vertices associated with two complex scalars.
+  We call this type, the type of vertex colors. -/
+inductive 𝓥 where
+  | φ₁φ₁φ₂φ₂ : 𝓥
+  | φ₁φ₁φ₁φ₁ : 𝓥
+  | φ₂φ₂φ₂φ₂ : 𝓥
+
+/-- To each vertex, the association of the number of edges. -/
+@[nolint unusedArguments]
+def 𝓥NoEdges : 𝓥 → ℕ := fun _ => 4
+
+/-- To each vertex, associates the indexing map of half-edges associated with that edge. -/
+def 𝓥Edges (v : 𝓥) : Fin (𝓥NoEdges v) → 𝓔 :=
+  match v with
+  | 𝓥.φ₁φ₁φ₂φ₂ => fun i =>
+    match i with
+    | (0 : Fin 4)=> 𝓔.complexScalarOut₁
+    | (1 : Fin 4) => 𝓔.complexScalarIn₁
+    | (2 : Fin 4) => 𝓔.complexScalarOut₂
+    | (3 : Fin 4) => 𝓔.complexScalarIn₂
+  | 𝓥.φ₁φ₁φ₁φ₁ => fun i =>
+    match i with
+    | (0 : Fin 4)=> 𝓔.complexScalarOut₁
+    | (1 : Fin 4) => 𝓔.complexScalarIn₁
+    | (2 : Fin 4) => 𝓔.complexScalarOut₁
+    | (3 : Fin 4) => 𝓔.complexScalarIn₁
+  | 𝓥.φ₂φ₂φ₂φ₂ => fun i =>
+    match i with
+    | (0 : Fin 4)=> 𝓔.complexScalarOut₂
+    | (1 : Fin 4) => 𝓔.complexScalarIn₂
+    | (2 : Fin 4) => 𝓔.complexScalarOut₂
+    | (3 : Fin 4) => 𝓔.complexScalarIn₂
+
+/-- A helper function for `WickString`. It is used to seperate incoming, vertex, and
+  outgoing nodes. -/
+inductive WickStringLast where
+  | incoming : WickStringLast
+  | vertex : WickStringLast
+  | outgoing : WickStringLast
+  | final : WickStringLast
+
+open WickStringLast
+
+/-- A wick string is a representation of a string of fields from a theory.
+  The use of vertices in the Wick string
+  allows us to identify which fields have the same space-time coordinate.
+
+  Note: Fields are added to `c` from right to left - matching how we would write this on
+  pen and paper.
+
+  The incoming and outgoing fields should be viewed as asymptotic fields.
+  While the internal fields associated with vertices are fields at fixed space-time points.
+  -/
+inductive WickString : {ni : ℕ} → (i : Fin ni → 𝓔) → {n : ℕ} → (c : Fin n → 𝓔) →
+  {no : ℕ} → (o : Fin no → 𝓔) → WickStringLast → Type where
+  | empty : WickString Fin.elim0 Fin.elim0 Fin.elim0 incoming
+  | incoming {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+      {o : Fin no → 𝓔} (w : WickString i c o incoming) (e : 𝓔) :
+      WickString (Fin.cons e i) (Fin.cons e c) o incoming
+  | endIncoming {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+      {o : Fin no → 𝓔} (w : WickString i c o incoming) : WickString i c o vertex
+  | vertex {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+      {o : Fin no → 𝓔} (w : WickString i c o vertex) (v : 𝓥) :
+      WickString i (Fin.append (𝓥Edges v) c) o vertex
+  | endVertex {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+      {o : Fin no → 𝓔} (w : WickString i c o vertex) : WickString i c o outgoing
+  | outgoing {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+      {o : Fin no → 𝓔} (w : WickString i c o outgoing) (e : 𝓔) :
+      WickString i (Fin.cons e c) (Fin.cons e o) outgoing
+  | endOutgoing {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+      {o : Fin no → 𝓔} (w : WickString i c o outgoing) : WickString i c o final
+
+namespace WickString
+
+/-- The number of nodes in a Wick string. This is used to help prove termination. -/
+def size {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
+    {f : WickStringLast} : WickString i c o f → ℕ := fun
+  | empty => 0
+  | incoming w e => size w + 1
+  | endIncoming w => size w + 1
+  | vertex w v => size w + 1
+  | endVertex w => size w + 1
+  | outgoing w e => size w + 1
+  | endOutgoing w => size w + 1
+
+/-- The number of vertices in a Wick string. This does NOT include external vertices. -/
+def numIntVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
+    {f : WickStringLast} : WickString i c o f → ℕ := fun
+  | empty => 0
+  | incoming w e => numIntVertex w
+  | endIncoming w => numIntVertex w
+  | vertex w v => numIntVertex w + 1
+  | endVertex w => numIntVertex w
+  | outgoing w e => numIntVertex w
+  | endOutgoing w => numIntVertex w
+
+/-- The vertices present in a Wick string. This does NOT include external vertices. -/
+def intVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
+    {f : WickStringLast} : (w : WickString i c o f) → Fin w.numIntVertex → 𝓥 := fun
+  | empty => Fin.elim0
+  | incoming w e => intVertex w
+  | endIncoming w => intVertex w
+  | vertex w v => Fin.cons v (intVertex w)
+  | endVertex w => intVertex w
+  | outgoing w e => intVertex w
+  | endOutgoing w => intVertex w
+
+informal_definition intExtVertex where
+  math :≈ "The vertices present in a Wick string, including external vertices."
+  deps :≈ [``WickString]
+
+informal_definition fieldToIntExtVertex where
+  math :≈ "A function which takes a field and returns the internal or
+    external vertex it is associated with."
+  deps :≈ [``WickString]
+
+informal_definition exponentialPrefactor where
+  math :≈ "The combinatorical prefactor from the expansion of the
+    exponential associated with a Wick string."
+  deps :≈ [``intVertex, ``WickString]
+
+informal_definition vertexPrefactor where
+  math :≈ "The prefactor arising from the coefficent of vertices in the
+    Lagrangian. This should not take account of the exponential prefactor."
+  deps :≈ [``intVertex, ``WickString]
+
+informal_definition minNoLoops where
+  math :≈ "The minimum number of loops a Feynman diagram based on a given Wick string can have.
+    There should be a lemma proving this statement."
+  deps :≈ [``WickString]
+
+informal_definition LoopLevel where
+  math :≈ "The type of Wick strings for fixed input and output which may permit a Feynman diagram
+    which have a number of loops less than or equal to some number."
+  deps :≈ [``minNoLoops, ``WickString]
+
+informal_lemma loopLevel_fintype where
+  math :≈ "The instance of a finite type on `LoopLevel`."
+  deps :≈ [``LoopLevel]
+
+end WickString
+
+end TwoComplexScalar

HepLean/PerturbationTheory/Wick/Theorem.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.PerturbationTheory.Wick.Species
+/-!
+
+# Wick's theorem
+
+Wick's theorem is related to a result in probability theory called Isserlis' theorem.
+
+-/
+
+namespace Wick
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+informal_lemma wicks_theorem where
+  math :≈ "Wick's theorem for fields which are not normally ordered."
+
+informal_lemma wicks_theorem_normal_order where
+  math :≈ "Wick's theorem for which fields at the same space-time point are normally ordered."
+  ref :≈ "https://www.physics.purdue.edu/~clarkt/Courses/Physics662/ps/qftch32.pdf"
+
+end Wick