pith. machine review for the scientific record. sign in
theorem proved term proof

cancellation_of_RS_preservation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 161theorem cancellation_of_RS_preservation
 162    (a_gauge a_scalar_RS : ℝ)
 163    (h : RSPreservesLongitudinalUnitarity a_gauge a_scalar_RS) :
 164    CancellationCondition a_gauge a_scalar_RS :=

proof body

Term-mode proof.

 165  cancellation_of_SM_hypothesis a_gauge a_scalar_RS h
 166
 167/-! ## §5. Master Bridge Certificate -/
 168
 169/-- Master certificate for longitudinal vector-boson scattering. -/

depends on (5)

Lean names referenced from this declaration's body.