vev_higgs_ratio_not_one
plain-language theorem explainer
The ratio of observed electroweak vacuum expectation value to observed Higgs mass differs from unity. Physicists examining the hierarchy problem would cite the result to exclude a degenerate scale coincidence in the electroweak sector. The proof unfolds the two observed-value definitions then applies numerical normalization to reach the inequality.
Claim. Let $r = v_0 / m_{H,0}$ where $v_0$ is the observed vacuum expectation value and $m_{H,0}$ the observed Higgs mass. Then $r ≠ 1$.
background
Recognition Science treats the Higgs potential as the J-cost functional whose minimum fixes the vacuum expectation value; symmetry breaking arises when the ledger selects one such minimum configuration. The module frames electroweak breaking as SU(2)_L × U(1)_Y → U(1)_EM realized through this J-cost minimum, with the observed VEV approximately 246 GeV. Upstream structures supply the J-cost definition (PhiForcingDerived.of) and the ledger factorization that calibrates J (DAlembert.LedgerFactorization.of).
proof idea
Tactic-mode proof that first unfolds the definitions of vev_observed and higgsMass_observed, then invokes norm_num to discharge the numerical inequality.
why it matters
The declaration closes one degenerate case inside the hierarchy-problem discussion of the SM-009 module, where the VEV remains far below the Planck scale. It sits downstream of the J-cost minimum theorem (vev_minimizes_jcost) and the phi-ladder mass assignments, reinforcing that the observed scales are forced by the eight-tick octave and phi-self-similarity rather than by fine-tuning. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.