vev_phi_ladder_position
plain-language theorem explainer
The theorem states that the electroweak VEV v ≈ 246 GeV occupies a definite integer rung on the phi-ladder relative to the electron mass m_e, so that their ratio equals a positive power of phi for some integers r_vev and r_e. Recognition Science researchers working on the C-020 electroweak scale derivation would cite it to embed the laboratory VEV inside the phi-ladder hierarchy already fixed by the forcing chain. The proof is a one-line wrapper that instantiates example rungs 29 and 2, then discharges the two positivity conjuncts by norm_num,
Claim. There exist integers $r_vev, r_e$ such that $v/m_e > 0$ and $phi^{r_vev - r_e} > 0$, where $v ≈ 246$ GeV is the electroweak vacuum expectation value and $m_e ≈ 0.511$ MeV is the electron mass on rung 2 of the phi-ladder.
background
The phi-ladder is the discrete mass scale sequence generated by repeated multiplication by the golden ratio phi, with electron mass fixed at rung 2 via the upstream definition m_e := mass_on_rung 2. The VEV is treated as another ladder quantity whose rung difference Delta r from the electron supplies the observed ratio v/m_e ≈ 4.8 × 10^5. Module C-020 places this inside the Recognition Science dissolution of the hierarchy problem: all electroweak scales arise from ledger rung structure rather than free parameters. Upstream results supply the positivity of phi (Constants.phi_pos) and the scale function scale(k) := phi^k used to interpret rung differences.
proof idea
The term proof selects concrete integers 29 and 2 for r_vev and r_e, then applies the constructor tactic to split the conjunction. The first conjunct is discharged by norm_num on the concrete ratio 246000.0 / 0.511. The second conjunct invokes Constants.phi_pos to obtain phi > 0 and finishes with the positivity tactic on the power.
why it matters
This declaration supplies the structural link required by C-020 for the electroweak VEV inside the phi-ladder, completing one step of the mass hierarchy dissolution that begins from T5 J-uniqueness and T6 phi fixed point. It feeds the sibling theorems vev_structure and vev_implies_scale that continue the electroweak derivation. The result remains approximate until the full electron mass closure (T9) fixes the exact Delta r.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.