longitudinalVectorScatteringCert_inhabited
plain-language theorem explainer
The theorem asserts that a master certificate encoding the structural cancellation in longitudinal vector-boson scattering exists. High-energy physicists studying perturbative unitarity above the TeV scale would cite it to confirm that gauge and scalar residues cancel exactly. The proof is a one-line term that directly supplies the explicit construction of the certificate as a witness.
Claim. The type of the master certificate for longitudinal vector-boson scattering is inhabited: there exists a structure containing proofs that the two-to-two amplitude decomposes additively into gauge-exchange and scalar-exchange pieces, vanishes exactly when the cancellation condition holds, and is implied by the Standard Model cancellation hypothesis.
background
The module formalizes the high-energy behavior of longitudinal vector-boson scattering such as W_L^+ W_L^- to W_L^+ W_L^-. Without a scalar resonance the gauge diagrams produce an amplitude that grows as s^2 / v^4 and violates unitarity above roughly 1 TeV; the Higgs scalar supplies an opposing residue that cancels the leading term, restoring bounded behavior at infinity. This is the Lee-Quigg-Thacker identity at the schema level. The certificate structure LongitudinalVectorScatteringCert packages three results: additive decomposition of amplitudeS2 into amplitudeGaugeOnly plus amplitudeScalarOnly, vanishing of the total amplitude under the cancellation condition a_g + a_s = 0, and the implication that the Standard Model hypothesis yields this cancellation. The upstream definition longitudinalVectorScatteringCert assembles these pieces from the lemmas amplitude_decomposition, amplitude_vanishes_under_cancellation, and cancellation_of_SM_hypothesis.
proof idea
The proof is a one-line term that supplies the explicit construction longitudinalVectorScatteringCert as the inhabitant of the Nonempty type.
why it matters
This theorem confirms that the master certificate for longitudinal vector-boson scattering is inhabited, thereby establishing the structural content of the Lee-Quigg-Thacker cancellation inside the Recognition Science framework. It directly supports the module's claim that the RS scalar-exchange residue equals the gauge-exchange residue with opposite sign under the normalization hypothesis, which is the content of RS preserving longitudinal unitarity. The open question left explicit in the module is the full kinematic four-point amplitude with Mandelstam variables and helicity decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.