pith. machine review for the scientific record. sign in
def definition def or abbrev high

amplitudeGaugeOnly

show as:
view Lean formalization →

The gauge-only amplitude isolates the contribution from gauge boson exchange and contact terms in longitudinal vector scattering, yielding the quadratic growth a_gauge * s² / v⁴ that violates unitarity at high energies. Electroweak physicists and model builders cite this expression when verifying the necessity of scalar exchange for perturbative consistency above the TeV scale. The definition is a direct algebraic extraction from the relevant Feynman diagrams with no additional lemmas required.

claimThe gauge-only amplitude is defined by $A_g(a_g, v, s) = a_g s^2 / v^4$, where $a_g$ is the gauge-exchange residue, $v$ the electroweak vacuum expectation value, and $s$ the Mandelstam variable.

background

In the Recognition Science treatment of the Standard Model, longitudinal vector-boson scattering $W_L W_L → W_L W_L$ serves as the key test of high-energy unitarity. The module parametrizes the amplitude by separate gauge and scalar residues, with the gauge piece alone producing the dangerous $s^2 / v^4$ growth identified by Lee, Quigg and Thacker. Upstream results supply the general notion of an S-matrix amplitude as the matrix element between initial and final states.

proof idea

The definition is a direct one-line algebraic expression for the gauge-only term. No lemmas are applied; the body simply multiplies the gauge residue by the kinematic factor $s^2 / v^4$.

why it matters in Recognition Science

This definition supplies the gauge piece that enters the additive decomposition theorem and the master certificate for longitudinal scattering. It encodes the structural content of the Lee-Quigg-Thacker cancellation: without an opposing scalar term the amplitude grows unbounded, violating unitarity. In the Recognition framework it supports the claim that the RS scalar coupling, fixed by the J-cost geometry, automatically satisfies the required cancellation, thereby preserving longitudinal unitarity. The open question remains a fully kinematic four-point amplitude with Mandelstam variables and helicity decomposition.

scope and limits

formal statement (Lean)

  72def amplitudeGaugeOnly (a_gauge v s : ℝ) : ℝ :=

proof body

Definition body.

  73  a_gauge * s ^ 2 / v ^ 4
  74
  75/-- Scalar-only amplitude. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.