Pith. sign in
module module high

IndisputableMonolith.Masses.VEVConsistency

show as:
view Lean formalization →

Module certifies tree-level Higgs VEV consistency in RS: with sin²θ_W=(3-φ)/6 one gets sin²θ_W cos²θ_W=(8-φ)/36, hence v²=m_Z²(8-φ)α⁻¹/(36π). Supplies closed forms, numerical bounds against PDG, and a VEVConsistencyCert. Cited by Fermi-constant and electroweak scorecard modules. Argument is algebraic identities plus interval arithmetic on α and the running ratio.

claimWith $\sin^2\theta_W=(3-\varphi)/6$ one has $\sin^2\theta_W\cos^2\theta_W=(8-\varphi)/36$. Tree-level VEV satisfies $v^2=m_Z^2\cdot(8-\varphi)\cdot\alpha^{-1}/(36\pi)$. The module bounds the $\alpha$ running ratio $\alpha^{-1}(M_Z)/\alpha^{-1}(0)$ and packages a certificate that the RS $v$ matches the PDG scale within those bounds.

background

Recognition Science fixes the electroweak mixing angle from gauge-embedding geometry: $\sin^2\theta_W=(3-\varphi)/6$ (WeinbergAngle / SM-004), with $\varphi$ the golden ratio forced at T6. Cosine follows as $\cos^2\theta_W=(3+\varphi)/6$. The Z mass sits on the phi-ladder in the electroweak sector: $m_Z=2\varphi^{51}/10^6$ MeV (ElectroweakMasses).

Standard Model tree-level matching gives $v^2=m_Z^2\sin^2\theta_W\cos^2\theta_W,\alpha^{-1}/\pi$. Substituting the RS product $\sin^2\cos^2=(8-\varphi)/36$ yields a closed RS expression for $v^2$ in terms of $m_Z$ and $\alpha^{-1}$ only. AlphaBounds supplies rigorous interval control on $\alpha^{-1}$; the module also tracks the QED running ratio from $q^2=0$ to $M_Z^2$, the dominant radiative correction to absolute electroweak mass predictions.

Sibling objects include the exact product identity, strict numerical inequalities for that product, closed-form and PDG-scale VEV squares, and the certificate VEVConsistencyCert discharged by vevConsistencyCert_holds.

proof idea

Core algebraic step: expand $((3-\varphi)/6)\cdot((3+\varphi)/6)=(9-\varphi^2)/36$. Use $\varphi^2=\varphi+1$ to rewrite as $(9-(\varphi+1))/36=(8-\varphi)/36$. That identity is sin2_cos2_product; companion lemmas give strict lower/upper bounds.

Tree-level $v^2$ is then the SM rearrangement $v^2=m_Z^2\sin^2\cos^2,\alpha^{-1}/\pi$ with the product substituted, producing vev_tree_sq_closed_form. Running-ratio bounds come from interval comparison of RS $\alpha^{-1}(0)\in(137.030,137.039)$ against PDG $\alpha^{-1}(M_Z)$. The certificate folds these equalities and inequalities into a single Prop discharged by the named holds lemma.

why it matters in Recognition Science

This is the P5a VEV-consistency block in the electroweak zero-parameter program. Downstream, FermiFromRSInputs chains $(m_Z,\sin^2\theta_W,\alpha_{\mathrm{EM}})\to v^2\to G_F=1/(\sqrt{2},v^2)$, quoting that VEVConsistency proves $v^2=z^2\cdot(8-\varphi)/36\cdot\alpha^{-1}/\pi$ with all inputs RS-derived.

ElectroweakZeroParamScoreCard and WBosonAbsoluteScoreCard import it to close the zero-fit claim: $\alpha^{-1}$ from T5/T6/T7, $\sin^2\theta_W=(3-\varphi)/6$ from geometry, $m_Z$ from the phi-ladder, and $v$ from this identity. AlphaRunningCorrectionScoreCard uses the running-ratio bounds as the leading radiative correction scorecard entry. Without the product identity, the Fermi and W-mass absolute predictions would retain a free electroweak angle.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (11)