vev_not_equal_higgs_mass
plain-language theorem explainer
The electroweak vacuum expectation value differs from the Higgs boson mass in the Recognition Science model. Researchers deriving boson masses from the J-cost minimum and phi-ladder placement would cite this to enforce scale separation. The tactic proof obtains positivity of the W mass, invokes the scale-determination lemma to bound the Higgs mass strictly below the VEV via a 0.6 factor and transitivity, then reaches a contradiction with linarith under the equality hypothesis.
Claim. The electroweak vacuum expectation value $v$ (in GeV) is not equal to the Higgs boson mass $m_H$ (in GeV).
background
The module derives W and Z masses from electroweak symmetry breaking in Recognition Science, where the Higgs field acquires a VEV $v$ corresponding to the J-cost minimum and sits at a specific rung on the phi-ladder. This yields the relations $m_Z = m_W / cos(θ_W)$ and numerical predictions $m_W ≈ 80.38$ GeV, $m_Z ≈ 91.19$ GeV, $v ≈ 246$ GeV. Upstream results supply the ordered Tick structure for discrete time progression and the lt_trans lemma for chaining strict inequalities on LogicNat values.
proof idea
The tactic proof obtains 0 < wBosonMass_GeV from wz_masses_positive, applies vev_determines_scale to produce the bound higgsMass_GeV < vev_GeV via multiplication by 0.6 and lt_trans, then assumes equality and derives an immediate contradiction with linarith.
why it matters
This result secures non-degeneracy of the VEV and Higgs scales inside the four-boson electroweak sector tied to the eight-tick octave. It completes the P-015/P-016 steps of the electroweak derivation in the module, confirming the VEV placement on the phi-ladder remains distinct from the Higgs mass. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.