GaugeTreeProcess
plain-language theorem explainer
GaugeTreeProcess enumerates the three canonical gauge tree processes in the Recognition Science structural model of SM amplitudes on H_RS. Researchers certifying leading-order gauge amplitudes would cite this type to fix the triad count before deriving J-cost expressions. The definition proceeds by direct enumeration of the constructors for Compton scattering, pair annihilation, and WW to ZZ unitarisation, automatically deriving decidable equality and finiteness.
Claim. The inductive type of gauge tree processes consists of three constructors: Compton scattering ($γe^- → γe^-$), pair annihilation ($e^+e^- → γγ$), and $W^+W^- → ZZ$ unitarisation.
background
The module develops structural predictions for SM gauge tree amplitudes on H_RS as the layer after the fermion-kinetic certification. It records three canonical processes whose amplitudes are expressed via the J-cost on coupling ratios, each vanishing at threshold and satisfying reciprocity and non-negativity. The local setting is the zero-parameter structural claim that RS amplitudes match SM leading-order results in the canonical sector, prior to the Wightman/OS continuum limit.
proof idea
The declaration is a direct inductive definition that enumerates the three constructors with no lemmas or tactics; decidability, representation, and finiteness are obtained automatically from the deriving clause.
why it matters
This type supplies the finite set underlying the GaugeTreeAmplitudesCert structure, which asserts that the process count equals 3 and matches configDim D-2 for D=3. It fills the structural opening for the gauge tree amplitude triad in the A1 SM Lagrangian certification, reproducing the SM unitarity bound without a Higgs at the zero-parameter level. The module notes that the full derivation requires the Wightman continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.