amplitude_zero_at_threshold
plain-language theorem explainer
The declaration establishes that the gauge tree amplitude vanishes at the threshold coupling ratio of unity. Researchers deriving structural predictions for Standard Model tree amplitudes from the Recognition Science J-cost would reference this as the zero-threshold base case in the gauge triad. The proof reduces directly to the unit lemma for the J-cost function via a single application.
Claim. The gauge tree amplitude at the threshold coupling ratio is zero: $A(1) = 0$, where the amplitude function is defined by $A(r) = J(r)$ and $J$ denotes the J-cost function satisfying $J(1) = 0$.
background
The J-cost function is defined as $J(x) = (x-1)^2/(2x)$, which quantifies deviation from unity in coupling ratios. In this module the per-process amplitude is obtained by evaluating J-cost on the relevant photon-electron or lepton-photon ratio for each canonical gauge tree process. The local setting is the structural certificate for SM gauge tree amplitudes on H_RS, covering Compton scattering, pair annihilation, and WW to ZZ unitarisation, each required to vanish at threshold.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma, which states Jcost 1 = 0 by direct simplification of the J-cost definition.
why it matters
This supplies the threshold_zero field inside the GaugeTreeAmplitudesCert structural certificate. It completes one leg of the gauge tree amplitude triad in the A1 SM Lagrangian structural cert, confirming that RS-native amplitudes match SM leading-order results at threshold without free parameters. 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.