vev_from_ledger
plain-language theorem explainer
vev_from_ledger is defined to coincide exactly with scale_from_ledger, linking the electroweak vacuum expectation value to the ledger-fixed phi-ladder hierarchy rather than treating it as an independent input. Researchers working on the electroweak scale or hierarchy problem in Recognition Science would cite this structural alias when dissolving naturalness as a tuning issue. The construction is a direct one-line alias with no additional lemmas or tactics.
Claim. The electroweak vacuum expectation value belongs to the ledger-fixed scale hierarchy: $(1 < phi < 2) land (forall r in Z, mass on rung r equals mass on rung r)$, where masses arise from the phi-ladder rather than from an unconstrained Higgs VEV times Yukawa coupling.
background
Recognition Science places mass scales on a phi-ladder with the form yardstick times phi to the power (rung minus 8 plus gap(Z)). The upstream scale definition supplies noncomputable scale(k) as phi^k. The scale_from_ledger proposition asserts that phi lies in (1,2) and that mass assignment is uniform across all integer rungs, dissolving the electroweak scale problem by removing any separate fine-tuning step. Module C-020 records that full numeric extraction of v approximately 246 GeV remains blocked while the structural placement is started.
proof idea
The declaration is a direct alias that sets vev_from_ledger equal to the proposition scale_from_ledger imported from ElectroweakScaleStructure. No tactics, reductions, or lemmas are invoked; the body is the single identifier scale_from_ledger.
why it matters
This definition supplies the hypothesis type for the downstream theorems vev_structure, vev_implies_scale, and vev_implies_phi_ne_one. It advances registry item C-020 by embedding the VEV inside the same ledger-fixed hierarchy that follows from T5 J-uniqueness and T6 phi fixed point. The module documentation notes that the full laboratory value extraction is still blocked, leaving the numeric rung position open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.