process_count_equals_3
plain-language theorem explainer
The theorem establishes that the gauge tree amplitude triad consists of exactly three processes. Researchers confirming structural predictions for Compton scattering, pair annihilation, and W boson unitarisation in Recognition Science would cite this cardinality. The proof is a one-line wrapper that invokes the decidable Fintype computation on the inductive enumeration of those processes.
Claim. The set of canonical gauge tree processes has cardinality three: $3 = |P|$, where $P$ enumerates Compton scattering, pair annihilation, and $W^+W^- $ to $ZZ$ unitarisation.
background
The module records structural properties of SM gauge tree amplitudes on the Recognition Science Hilbert space. GaugeTreeProcess is the inductive type with three constructors corresponding to Compton scattering (γe⁻ → γe⁻), pair annihilation (e⁺e⁻ → γγ), and W⁺W⁻ → ZZ unitarisation. Each amplitude is defined via J-cost on the relevant coupling ratio and vanishes at threshold while growing monotonically off threshold.
proof idea
The proof is a one-line wrapper that applies the upstream theorem gauge_tree_process_count. That theorem uses the decide tactic on the Fintype.card expression, which succeeds because the inductive type derives a Fintype instance from its three constructors and decidable equality.
why it matters
This result certifies that the gauge tree amplitude triad contains precisely three processes, matching the module claim that the count equals configDim D - 2. It anchors the GaugeTreeAmplitudesCert module's structural prediction that RS-native amplitudes reproduce SM leading-order features in the canonical sector without a Higgs. The fixed count of three aligns with the framework's eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.