vev_canonical_pos
plain-language theorem explainer
The canonical electroweak vacuum expectation value is strictly positive in the reals. Researchers deriving the Fermi constant from Recognition Science ledger structure cite this result to guarantee a positive denominator in the G_F expression. The proof is a one-line term-mode wrapper that unfolds the definition of the canonical VEV and applies numerical normalization.
Claim. $0 < v$ where $v = 246$ in GeV units.
background
The module formalizes the RS structural framework for the electroweak VEV under registry item C-020. RS derives mass scales from ledger rung structure rather than parameter tuning, with the full laboratory extraction of the VEV remaining blocked. The canonical VEV is defined directly as the standard electroweak scale of 246 GeV.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of the canonical VEV and applies norm_num to confirm that the constant 246 is positive.
why it matters
This result feeds the positivity arguments in fermi_den_pos and row_fermi_pred_lower within the FermiConstantScoreCard module. It supports C-020 by confirming the VEV as a positive scale on the phi-ladder, dissolving naturalness questions via rung assignments. The framework places this VEV near rung 27 with ratio to the electron mass approximately phi^27.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.