mZ_sq_nonneg
plain-language theorem explainer
mZ_sq_nonneg establishes that the squared Z-boson mass remains nonnegative for arbitrary real gauge couplings g, g' and substrate scale v. It is cited inside the electroweak mass bridge certificate that assembles all positivity and ordering facts for the gauge-boson masses. The proof unfolds the quadratic definition and applies nonnegativity of squares together with linarith and the positivity tactic.
Claim. $0 ≤ (g^2 + g'^2) v^2 / 4$ for all real $g, g', v$.
background
The Electroweak Mass Bridge module derives the tree-level Standard Model gauge-boson mass relations from a common recognition-substrate scale v together with arbitrary positive gauge couplings g and g'. The definition mZ_sq g gp v expands to (g² + g'²) v² / 4. This nonnegativity result is collected by the bridge certificate alongside the corresponding facts for mW_sq and the W/Z ordering relations.
proof idea
The proof unfolds mZ_sq to expose the quadratic expression, introduces three hypotheses asserting nonnegativity of g², gp² and v² via sq_nonneg, combines the first two squares with linarith to obtain nonnegativity of their sum, and finishes with the positivity tactic.
why it matters
This theorem supplies the nonnegativity component mZ_sq_nn inside electroweakMassBridgeCert, which certifies the full set of gauge-boson mass relations on positive g, g', v. It fills the basic positivity requirement for the Z-mass formula in the module that bridges the recognition substrate to Standard Model tree-level masses. The open question of numerical calibration of g and g' from the phi-ladder remains outside this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.