ew_scale_implies_phi_window
plain-language theorem explainer
Electroweak-scale structure derived from the ledger forces the golden ratio to satisfy 1 < phi < 2. Researchers constructing mass ladders in Recognition Science cite this to anchor the electroweak rung without external tuning parameters. The proof is a one-line term projection that extracts the first conjunct of the ledger-scale hypothesis.
Claim. If the electroweak scale is obtained from ledger structure, then $1 < phi < 2$.
background
The module formalizes E-004 on the electroweak scale, placing the vacuum expectation value near 246 GeV as an output of the phi-ladder rather than a radiative correction. Scale is defined as phi raised to an integer rung, with rung assignments supplied by sector-specific maps for leptons, quarks, and bosons. The ledger supplies the structural input that fixes the electroweak rung and thereby constrains phi itself.
proof idea
The proof is a one-line term that projects the first field of the ledger-scale hypothesis, which already encodes the required bounds on phi.
why it matters
The result supplies the phi-window needed for all subsequent electroweak mass calculations inside the Recognition framework. It directly supports the sibling statements on absence of fine-tuning and on phi not equal to one or two. Within the T0-T8 chain it confirms the interval required for the self-similar fixed point at the electroweak rung; the remaining open question is the complete ledger-to-mass derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.