Crossing symmetry for topology graphs

This module collects crossing-symmetry theorems for the generic topology enumeration layer. The graph data and permutation action live in TopologyEnumeration; this module provides the named invariant theorem surface.

theorem EpsilonEridani.QFT.PerturbationTheory.FeynmanDiagrams.candidateOfGraph_permuteExternalLegs (graph : TopologyGraph) (σ : ExternalLegPerm graph.externalNodeCount) (h : graph.hasWellFormedExternalLegs) : candidateOfGraph (graph.permuteExternalLegs σ h) = candidateOfGraph graph

candidateOfGraph is invariant under external-leg permutations.

theorem EpsilonEridani.QFT.PerturbationTheory.FeynmanDiagrams.candidateOfGraph_eq_of_isCrossingEquivalent {graph other : TopologyGraph} (h : graph.IsCrossingEquivalent other) : candidateOfGraph graph = candidateOfGraph other

Crossing-equivalent graphs define the same generic topology candidate.

theorem EpsilonEridani.QFT.PerturbationTheory.FeynmanDiagrams.candidateOfGraph_crossingInvariant {graph other : TopologyGraph} (h : graph.IsCrossingEquivalent other) : candidateOfGraph graph = candidateOfGraph other

Named crossing-symmetry theorem for the generic topology classifier.