electroweakMassBridgeCert_inhabited
plain-language theorem explainer
The declaration proves that the ElectroweakMassBridgeCert structure is nonempty by exhibiting an explicit witness. A researcher working on recognition-derived electroweak relations would cite this to confirm that the gauge-boson mass relations hold unconditionally for positive couplings g, g' and scale v. The proof is a one-line term that directly instantiates the certificate assembled from the nonnegativity and ordering lemmas.
Claim. The structure ElectroweakMassBridgeCert is inhabited: there exists a certificate asserting that for all positive gauge couplings $g, g'$ and positive scale $v$, one has $m_W^2 = g^2 v^2/4$, $m_Z^2 = (g^2 + g'^2) v^2/4$, $m_W^2$ and $m_Z^2$ are nonnegative, $m_W^2$ is at most $m_Z^2$, the inequality is strict when $g' > 0$, and the squared mass ratio equals $g^2/(g^2 + g'^2) = $cos$^2$ of the Weinberg angle.
background
The module derives the Standard Model gauge-boson mass relations from the recognition-substrate scale $v$ together with arbitrary positive gauge couplings $g, g'$. It formalizes the tree-level expressions $m_W^2 = g^2 v^2/4$ and $m_Z^2 = (g^2 + g'^2) v^2/4$, together with the Weinberg-angle identities $m_W/m_Z = $cos$ theta_W$ and sin$^2 theta_W = g'^2/(g^2 + g'^2)$. These relations are conditional on the same $v$ supplied by the HiggsEFTBridge and on positivity of the couplings; numerical calibration of $g, g'$ remains a separate open step.
proof idea
The proof is a one-line term that applies the Nonempty constructor directly to the witness electroweakMassBridgeCert. That witness is the structure definition which packages the four lemmas mW_sq_nonneg, mZ_sq_nonneg, mW_sq_le_mZ_sq, mW_sq_lt_mZ_sq_of_gp_pos and the ratio equality mW_over_mZ_sq_eq_cos_sq.
why it matters
This result closes the ElectroweakMassBridgeCert structure by proving it is inhabited, thereby confirming that the gauge-boson mass relations are realized unconditionally once a positive substrate scale $v$ and positive couplings are given. It supplies the existence statement required by any downstream formalization of the Standard Model sector inside the recognition framework. The companion module Masses/ElectroweakMasses already supplies the recognition-Weinberg-angle prediction sin$^2 theta_W = (3 - phi)/6$; the present certificate keeps the gauge relations independent of that numerical choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.