vev_pos
plain-language theorem explainer
The vacuum expectation value of the Higgs field is strictly positive. Researchers deriving Standard Model masses within Recognition Science cite this to confirm symmetry breaking at the electroweak scale. The proof is a one-line wrapper that unfolds the numerical definition of the VEV and applies normalization to verify the inequality.
Claim. The vacuum expectation value $v$ of the Higgs field satisfies $0 < v$.
background
The Higgs Rung Assignment module derives Standard Model particle masses from the phi-ladder using Q3 geometry and the Recognition Composition Law. The VEV is defined numerically here as 246 GeV to match the observed electroweak scale. Upstream results establish the VEV as the golden ratio phi in native units, with positivity required for symmetry breaking and proved via the positivity of phi.
proof idea
The proof is a one-line wrapper. It unfolds the definition of the VEV to the constant 246 and invokes norm_num to discharge the positivity claim.
why it matters
This result supports the nonzero vacuum expectation value theorem in the QFT Higgs mechanism section, which concludes the vacuum has a nontrivial field value. It also underpins the positive mass parameter and particle mass theorems there. Within the framework it secures the positive electroweak scale needed for the phi-ladder mass assignments and the Higgs mass interval hypothesis of (120, 130) GeV.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.