vev_higgs_ratio
plain-language theorem explainer
The declaration confirms that the ratio of the observed electroweak vacuum expectation value to the Higgs mass lies strictly between 1.9 and 2.1. A physicist modeling symmetry breaking through J-cost minimization would cite this numerical anchor to link the Mexican-hat minimum to measured scales. The proof is a short tactic sequence that unfolds the constant definitions and discharges the inequality via normalization.
Claim. Let $v$ denote the observed vacuum expectation value and $m_H$ the observed Higgs boson mass. Then $1.9 < v/m_H < 2.1$.
background
In the Recognition Science treatment of electroweak symmetry breaking the Higgs potential is identified with the J-cost functional and the vacuum expectation value is the ledger configuration that minimizes this cost. The module supplies noncomputable definitions for the observed VEV (approximately 246 GeV) and Higgs mass (125 GeV) drawn from the constants and PhiForcing imports. Upstream results on empirical program collision-freeness and spin-statistics value ensure the ledger remains consistent with observed particle properties before the ratio check is applied.
proof idea
The proof unfolds the definitions of the observed VEV and Higgs mass, splits the conjunction with constructor, and normalizes both sides of the inequality with norm_num.
why it matters
This result anchors the electroweak breaking section by verifying the approximate ratio of 2 that the phi-ladder structure suggests for the J-cost minimum. It supports the claim that the symmetry-breaking scale separation arises directly from the Recognition Composition Law without extra parameters. The declaration sits inside the T5-T8 forcing chain where phi is the self-similar fixed point, though it leaves open the exact derivation of the ratio from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.