gauge_tree_process_count
plain-language theorem explainer
The Recognition Science gauge tree amplitude triad consists of exactly three canonical processes. Structural QFT certificate authors cite this enumeration to fix the triad dimension at three. The proof is a one-line decision procedure that exhausts the finite inductive type with constructors for Compton scattering, pair annihilation, and WW to ZZ unitarisation.
Claim. The set of gauge tree processes has cardinality three: $|{}$Compton scattering ($γe^- → γe^-$), pair annihilation ($e^+e^- → γγ$), WW to ZZ unitarisation ($W^+W^- → ZZ$)$| = 3$.
background
In the Gauge Tree Amplitudes module the three canonical processes are introduced via the inductive type GaugeTreeProcess whose constructors are comptonScattering, pairAnnihilation, and wwzzUnitarisation. This enumeration supports the structural claim that RS-native amplitudes match SM leading-order results in the canonical sector, with each amplitude given by J-cost on the relevant coupling ratio. Upstream results include the cost definition from MultiplicativeRecognizerL4 (derivedCost on positive ratios) and the amplitude extraction from SMatrixUnitarity (S-matrix element) together with the DoubleSlit amplitude sum.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card of GaugeTreeProcess. The inductive type derives DecidableEq, Repr, BEq and Fintype, so the decision procedure directly computes the cardinality as three.
why it matters
This count is consumed by the gaugeTreeAmplitudesCert definition (which assembles the full structural certificate) and by process_count_equals_3 (which equates the count to configDim D - 2). It fills the module-level claim that the three amplitudes form the gauge tree amplitude triad and aligns with the Recognition framework landmarks of D = 3 spatial dimensions and the eight-tick octave. The module notes that the full derivation still requires the Wightman/OS continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.