mW_sq_nonneg
plain-language theorem explainer
The declaration proves that the squared W-boson mass remains non-negative for arbitrary real gauge coupling g and vacuum expectation value v. It would be cited whenever positivity of electroweak masses must be secured inside the Recognition Science bridge to the Standard Model. The proof is a short term-mode reduction that unfolds the explicit formula and invokes non-negativity of squares.
Claim. For all real numbers $g, v$, $m_W^2 = g^2 v^2 / 4$ satisfies $m_W^2(g, v) ≥ 0$.
background
The Electroweak Mass Bridge module derives the tree-level Standard Model gauge-boson mass relations from the recognition-substrate scale v together with arbitrary positive gauge couplings g and g'. The upstream definition mW_sq supplies the concrete expression m_W² = g² v² / 4. The module documentation states that these relations hold conditionally on the same v taken from the RS substrate (formalised in HiggsEFTBridge) while leaving numerical calibration of g and g' as an empirical input.
proof idea
The proof unfolds the definition of mW_sq to g² v² / 4. It applies sq_nonneg to obtain g² ≥ 0 and v² ≥ 0, then invokes the positivity tactic to conclude that the scaled product is non-negative.
why it matters
This theorem supplies the non-negativity field mW_sq_nn inside the ElectroweakMassBridgeCert record that aggregates all gauge-mass positivity and ordering facts. It completes the basic positivity step required for the unconditional gauge relations on positive (g, g', v) described in the module. The parent result electroweakMassBridgeCert collects these certificates for downstream mass-bridge use. It touches the open numerical calibration of g and g' from the RS phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.