Electroweak VEV is Not a Free Parameter

1. Setting

The electroweak vacuum expectation value is usually an input. RS places it on the phi-ladder and ties it to the W/Z mass hierarchy and the electron rung.

2. Equations

(E1)

$$ v_{\mathrm{EW}}\approx 246\ \mathrm{GeV},\qquad v\in \varphi\text{-window} $$

Electroweak VEV on the phi-ladder.

3. Prediction or structural target

• electroweak VEV: predicted phi-window near 246 (GeV); empirical 246.21965 GeV. Source: PDG electroweak fit

This entry is one of the marquee derivations. The numerical or formal target is explicit, and the falsifier identifies the failure mode.

4. Formal anchor

The primary anchor is Constants.ElectroweakVEVStructure..vev_not_free_parameter.

/-- The electroweak scale is ledger-determined in RS. -/
theorem vev_not_free_parameter : scale_from_ledger :=
  ew_scale_structure

/-- A minimal structural placeholder for the derived VEV relation. -/
def vev_from_ledger : Prop := scale_from_ledger

/-- **C-020 Structural**: the electroweak VEV belongs to the same
ledger-fixed scale hierarchy rather than being an unconstrained
input parameter. -/

5. What is inside the Lean module

Key theorems:

• vev_not_free_parameter
• vev_structure
• vev_implies_scale
• vev_phi_window
• vev_implies_phi_ne_one
• vev_phi_ladder_position
• vev_wz_mass_hierarchy
• hierarchy_problem_dissolution
• c020_derivation_strategy
• vev_in_range
• vev_canonical_pos
• vev_electron_rung_27_order

Key definitions:

• vev_from_ledger
• vev_canonical

6. Derivation chain

• vev_not_free_parameter - vev not free
• vev_structure - vev structure
• vev_phi_ladder_position - vev phi-ladder position
• hierarchy_problem_dissolution - Hierarchy problem dissolved
• vev_wz_mass_hierarchy - W/Z mass hierarchy
• vev_electron_rung_27_order - Electron rung-27 order

7. Falsifier

A measured VEV or W/Z hierarchy inconsistent with the RS phi-window refutes this derivation.

8. Where this derivation stops

Below this page the chain reduces to the RS forcing sequence: J-cost uniqueness, phi forcing, the eight-tick cycle, and the D=3 recognition substrate. If any upstream theorem changes, this page must be versioned rather than patched silently. The published URL is stable, but the version field is the contract.

10. Audit path

To audit electroweak-vev-derived, start with the primary Lean anchor Constants.ElectroweakVEVStructure.vev_not_free_parameter. Then inspect the theorem names listed in the module-content section. The page is intentionally built so the public explanation is not a substitute for the proof object; it is a map into it. The mathematical dependency is the same in every case: reciprocal cost fixes J, J fixes the phi-ladder, the eight-tick cycle fixes the recognition clock, and the domain theorem listed above supplies the last step. If that last step is empirical, the falsifier section names what observation would break it. If that last step is formal, a Lean-checkable counterexample is the relevant failure mode.