PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FeynmanDiagrams.Instances.Phi4

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.

source
def PhiFour.phi4PreFeynmanRules :
PreFeynmanRule

The pre-Feynman rules for Phi^4 theory.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem PhiFour.phi4PreFeynmanRules_HalfEdgeLabel :
    phi4PreFeynmanRules.HalfEdgeLabel = Fin 1
    source
    @[simp]
    theorem PhiFour.phi4PreFeynmanRules_EdgeLabel :
    phi4PreFeynmanRules.EdgeLabel = Fin 1
    source
    @[simp]
    theorem PhiFour.phi4PreFeynmanRules_vertexLabelMap (x : Fin 2) :
    phi4PreFeynmanRules.vertexLabelMap x = match x with | 0 => CategoryTheory.Over.mk ![0] | 1 => CategoryTheory.Over.mk ![0, 0, 0, 0]
    source
    @[simp]
    theorem PhiFour.phi4PreFeynmanRules_edgeLabelMap (x : Fin 1) :
    phi4PreFeynmanRules.edgeLabelMap x = match x with | 0 => CategoryTheory.Over.mk ![0, 0]
    source
    @[simp]
    theorem PhiFour.phi4PreFeynmanRules_VertexLabel :
    phi4PreFeynmanRules.VertexLabel = Fin 2
    source
    instance PhiFour.instOfNatEdgeLabelPhi4PreFeynmanRules (a : ℕ) :
    OfNat phi4PreFeynmanRules.EdgeLabel a

    An instance allowing us to use integers for edge labels for Phi-4.

    Equations
    source
    instance PhiFour.instOfNatHalfEdgeLabelPhi4PreFeynmanRules (a : ℕ) :
    OfNat phi4PreFeynmanRules.HalfEdgeLabel a

    An instance allowing us to use integers for half edge labels for Phi-4.

    Equations
    source
    instance PhiFour.instOfNatVertexLabelPhi4PreFeynmanRules (a : ℕ) :
    OfNat phi4PreFeynmanRules.VertexLabel a

    An instance allowing us to use integers for vertex labels for Phi-4.

    Equations
    source
    instance PhiFour.instIsFinitePreFeynmanRulePhi4PreFeynmanRules :
    phi4PreFeynmanRules.IsFinitePreFeynmanRule

    The pre feynman rules for Phi-4 are finite.

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

    The figure eight diagram #

    This section provides an example of the use of Feynman diagrams in PhysLean.

    source
    @[reducible, inline]
    abbrev PhiFour.figureEight :
    FeynmanDiagram phi4PreFeynmanRules

    The figure eight Feynman diagram.

    Equations
    Instances For
      source
      theorem PhiFour.figureEight_connected :
      figureEight.Connected

      figureEight is connected. We can get this from #eval Connected figureEight.

      source
      theorem PhiFour.figureEight_symmetryFactor :
      figureEight.symmetryFactor = 8

      The symmetry factor of figureEight is 8. We can get this from #eval symmetryFactor figureEight.