Feynman diagrams in a complex scalar field theory

@[simp]

theorem PhiFour.complexScalarFeynmanRules_edgeLabelMap (x : Fin 1) : PhiFour.complexScalarFeynmanRules.edgeLabelMap x = match x with | 0 => CategoryTheory.Over.mk ![0, 1]

@[simp]

theorem PhiFour.complexScalarFeynmanRules_EdgeLabel : PhiFour.complexScalarFeynmanRules.EdgeLabel = Fin 1

@[simp]

theorem PhiFour.complexScalarFeynmanRules_VertexLabel : PhiFour.complexScalarFeynmanRules.VertexLabel = Fin 3

@[simp]

theorem PhiFour.complexScalarFeynmanRules_HalfEdgeLabel : PhiFour.complexScalarFeynmanRules.HalfEdgeLabel = Fin 2

@[simp]

theorem PhiFour.complexScalarFeynmanRules_vertexLabelMap (x : Fin 3) : PhiFour.complexScalarFeynmanRules.vertexLabelMap x = match x with | 0 => CategoryTheory.Over.mk ![0] | 1 => CategoryTheory.Over.mk ![1] | 2 => CategoryTheory.Over.mk ![0, 0, 1, 1]

def PhiFour.complexScalarFeynmanRules : PreFeynmanRule

The pre-Feynman rules for a complex scalar theory.

Equations

• One or more equations did not get rendered due to their size.

instance PhiFour.instOfNatEdgeLabelComplexScalarFeynmanRules (a : ℕ) : OfNat PhiFour.complexScalarFeynmanRules.EdgeLabel a

An instance allowing us to use integers for edge labels for complex scalar theory.

Equations

• PhiFour.instOfNatEdgeLabelComplexScalarFeynmanRules a = { ofNat := ↑a }

instance PhiFour.instOfNatHalfEdgeLabelComplexScalarFeynmanRules (a : ℕ) : OfNat PhiFour.complexScalarFeynmanRules.HalfEdgeLabel a

An instance allowing us to use integers for half-edge labels for complex scalar theory.

Equations

• PhiFour.instOfNatHalfEdgeLabelComplexScalarFeynmanRules a = { ofNat := ↑a }

instance PhiFour.instOfNatVertexLabelComplexScalarFeynmanRules (a : ℕ) : OfNat PhiFour.complexScalarFeynmanRules.VertexLabel a

An instance allowing us to use integers for vertex labels for complex scalar theory.

Equations

• PhiFour.instOfNatVertexLabelComplexScalarFeynmanRules a = { ofNat := ↑a }

instance PhiFour.instIsFinitePreFeynmanRuleComplexScalarFeynmanRules : PhiFour.complexScalarFeynmanRules.IsFinitePreFeynmanRule

The pre feynman rules for complex scalars are finite.

Equations

• One or more equations did not get rendered due to their size.