vev_in_range
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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value 246 from the phi-ladder or eight-tick octave.
- Does not complete the full extraction of the laboratory VEV from ledger rungs.
- Does not resolve the hierarchy problem beyond noting its structural dissolution.
Lean usage
have h := vev_in_rangeformal statement (Lean)
154theorem vev_in_range : (244 : ℝ) < vev_canonical ∧ vev_canonical < 248 := by
proof body
Term-mode proof.
155 unfold vev_canonical; constructor <;> norm_num
156
157/-- The VEV is positive. -/