GaugeTreeAmplitudesCert
plain-language theorem explainer
GaugeTreeAmplitudesCert packages the structural certificate for the three canonical gauge tree amplitudes in Recognition Science. It records that exactly three processes exist, the J-cost amplitude vanishes at threshold ratio 1, is reciprocal symmetric, and non-negative for positive ratios. Researchers verifying parameter-free SM gauge interactions at tree level would cite this certificate. The declaration is a pure structure definition whose fields are supplied by sibling results on process count and J-cost properties.
Claim. A structure certifying that the set of canonical gauge tree processes has cardinality three, and that the amplitude function $A(r) := J(r)$ (J-cost on the coupling ratio) satisfies $A(1) = 0$, $A(r) = A(r^{-1})$ for all $r > 0$, and $A(r) > 0$ for $r > 0$ with $A(r) = 0$ only at threshold.
background
Recognition Science encodes gauge tree amplitudes via the J-cost function $J(r) = (r + r^{-1})/2 - 1$, which arises from T5 J-uniqueness in the forcing chain. The module defines three processes: Compton scattering, pair annihilation, and WW to ZZ unitarization. The processAmplitude definition simply applies J-cost to the relevant ratio for each process. This certificate follows the fermion-kinetic cert and forms the gauge tree amplitude triad in the A1 SM Lagrangian Structural Cert layer. Upstream amplitude_nonneg follows directly from Jcost_nonneg.
proof idea
This is a structure definition. Its four fields are instantiated by the downstream constructor gaugeTreeAmplitudesCert, which applies gauge_tree_process_count for the cardinality, amplitude_zero_at_threshold for the vanishing condition, amplitude_reciprocal_symm for the symmetry, and amplitude_nonneg for the inequality. No tactics or reductions occur inside the structure itself.
why it matters
This structure supplies the structural certificate for the gauge tree amplitude triad, feeding directly into the gaugeTreeAmplitudesCert definition. It advances the A1 SM Lagrangian Structural Cert by encoding the three processes and their J-cost properties without free parameters, consistent with T5 J-uniqueness and the eight-tick octave. The module notes that full derivation awaits the Wightman/OS continuum limit (S1 in progress) and touches the open question of matching SM leading-order results in the canonical sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.