electroweakMassBridgeCert
plain-language theorem explainer
The electroweak mass bridge certificate bundles the tree-level W and Z boson mass relations of the Standard Model, derived from a common recognition scale v together with arbitrary positive gauge couplings g and g'. A physicist matching the recognition substrate to electroweak data would cite it to confirm that m_W² = g²v²/4, m_Z² = (g² + g'²)v²/4, the ratio equals cos²θ_W, and the trigonometric identities close. The definition is a direct record construction that assigns each field of the certificate to an existing lemma on non-negativity, squ
Claim. The certificate asserts that for gauge couplings g, g' and scale v, with m_W²(g, v) := g²v²/4 and m_Z²(g, g', v) := (g² + g'²)v²/4, the following hold unconditionally: ∀g v, 0 ≤ m_W²(g, v); ∀g g' v, 0 ≤ m_Z²(g, g', v); ∀g g' v, m_W²(g, v) ≤ m_Z²(g, g', v); ∀g g' v, g' > 0 → v > 0 → m_W²(g, v) < m_Z²(g, g', v); ∀g g' v, g > 0 → v > 0 → m_W²(g, v)/m_Z²(g, g', v) = g²/(g² + g'²); and cos²θ_W + sin²θ_W = 1 with 0 < cos²θ_W ≤ 1.
background
This module derives the Standard-Model gauge-boson mass relations from the recognition-substrate scale v plus generic positive gauge couplings g, g'. Concretely it formalises m_W² = g² v² / 4, m_Z² = (g² + g'²) v² / 4, m_W / m_Z = cos θ_W = g / √(g² + g'²), sin² θ_W = g'² / (g² + g'²). These are the SM tree-level gauge-mass relations. Their content here is conditional: given the same v from the RS substrate (formalised in HiggsEFTBridge) and any positive g, g', the SM gauge-mass relations hold. The identification of g, g' with their measured numerical values remains an empirical input, just as the φ-ladder numerical match for v is a separate (still open) calibration step.
proof idea
The definition is a direct record construction that populates each field of ElectroweakMassBridgeCert with the corresponding theorem: mW_sq_nn is supplied by mW_sq_nonneg, mZ_sq_nn by mZ_sq_nonneg, mW_le_mZ by mW_sq_le_mZ_sq, mW_lt_mZ by mW_sq_lt_mZ_sq_of_gp_pos, ratio_eq_cos_sq by mW_over_mZ_sq_eq_cos_sq, cos2_plus_sin2 by cos_sq_plus_sin_sq_thetaW, and cos_sq_window by cos_sq_thetaW_in_unit_interval.
why it matters
This certificate is the master bundling object for the gauge-boson mass relations and is consumed by higgsEFTLowEnergyLimitCert to complete the low-energy effective theory certificate. It also feeds electroweakMassBridgeCert_inhabited. It closes the THEOREM part of the module by proving all clauses unconditionally on positive (g, g', v), leaving only the OPEN_NORMALIZATION of numerical g, g' from the RS substrate. In the forcing chain it supplies the D = 3 spatial dimension consistency at the electroweak scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.