Pith. sign in
module module moderate

IndisputableMonolith.Constants.ElectroweakVEVStructure

show as:
view Lean formalization →

The electroweak vacuum expectation value is fixed by the Recognition Science ledger, not left as a free Standard Model input. The module packages structural claims that place the VEV on the phi-ladder, tie it to the W/Z mass hierarchy, and treat the hierarchy problem as a free-parameter artifact. Fermi-constant scoring and the unified forcing chain import this layer. Content is structural packaging of the upstream EWSB scale framework.

claimIn Recognition Science the electroweak vacuum expectation value $v$ is ledger-determined: it occupies a definite $\varphi$-ladder position, lies in a fixed numerical window, and is not an independent free parameter. Structural consequences recorded here include $v$ fixing the electroweak scale, the $W/Z$ mass hierarchy, and dissolution of the hierarchy problem once $v$ is no longer free.

background

In the Standard Model the electroweak scale is set by the Higgs vacuum expectation value $v \approx 246$ GeV, entered as a free parameter. Recognition Science replaces free dimensionful inputs with ledger structure: the J-cost, the golden-ratio fixed point $\varphi$, and the phi-ladder organization of masses and scales.

The upstream module ElectroweakScaleStructure (registry E-004) formalizes the question "What determines the electroweak scale?" as an RS structural framework for electroweak symmetry breaking. This Constants module specializes that framework into named VEV claims: not a free parameter, derived from the ledger, confined to a $\varphi$-window, located on the phi-ladder, and linked to the $W/Z$ hierarchy.

Sibling names in the module mark the intended surface: ledger origin, scale implication, $\varphi \neq 1$, ladder position, mass hierarchy, hierarchy-problem dissolution, and canonical/in-range witnesses used by downstream score cards.

proof idea

This is a structure and constants module, not a single theorem with one proof. It re-exports and names the RS electroweak-scale package from the upstream QFT formalization: definitions and structural lemmas asserting that the VEV is ledger-fixed, implies the electroweak scale, sits in a $\varphi$-window on the ladder, and forces the $W/Z$ hierarchy reading. Hierarchy-problem dissolution is the corresponding non-claim that a free $v$ was the source of the apparent tuning. Expect definitional packaging plus short structural implications rather than a long constructive derivation inside this file.

why it matters in Recognition Science

Downstream, FermiConstantScoreCard (Phase 1 row P1-C01) imports this module for the natural-unit electroweak identity needed to score the Fermi constant against ledger structure. UnifiedForcingChain also imports it while proving that T0–T8 are forced from the cost foundation (Recognition Composition Law), so electroweak-scale structure sits inside the same constants layer as the forcing chain.

In framework terms the module answers E-004 at the Constants boundary: once $v$ is ledger-determined on the $\varphi$-ladder, related observables ($G_F$, $W/Z$ hierarchy) become scoreable rather than fitted free inputs, and the hierarchy problem is reclassified as an artifact of treating $v$ as free. It does not by itself close numerical mass formulas; it supplies the structural VEV interface those closures need.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)