vev_in_range
plain-language theorem explainer
The declaration proves that the canonical electroweak vacuum expectation value lies strictly between 244 and 248 GeV. Physicists deriving mass scales from Recognition Science ledger structures cite it to anchor the RS VEV against laboratory data. The proof reduces to unfolding the definition of vev_canonical as 246 and discharging the two numerical inequalities with normalization tactics.
Claim. $244 < v < 248$ where $v$ is the canonical Recognition Science electroweak vacuum expectation value in GeV.
background
The module formalizes C-020 on the electroweak VEV near 246 GeV inside the Recognition Science framework. It treats mass scales as outputs of ledger rung structure rather than free parameters, consistent with the forcing chain that yields D=3 and the phi-ladder. vev_canonical is the noncomputable definition that sets this scale equal to the standard electroweak value of 246 GeV. Upstream results supply the definition itself together with structural isomorphisms from simplicial ledger edge lengths and mechanism design that underwrite the overall scale extraction.
proof idea
The proof is a one-line wrapper. It unfolds vev_canonical to the literal constant 246, splits the conjunction with constructor, and applies norm_num to both sides of the resulting inequalities.
why it matters
This result supplies the numeric window required by the Fermi constant scorecard certification, which packages the range alongside fermi bracket and codata checks. It advances the C-020 registry item by confirming consistency with observation while the full ledger-rung derivation of the VEV remains blocked. The parent theorem fermiConstantScoreCardCert_holds directly invokes the range to close its certificate structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.