ew_scale_implies_phi_ne_one
plain-language theorem explainer
Electroweak-scale structure requires the self-similar ratio phi to satisfy 1 < phi < 2, excluding the degenerate fixed point at phi = 1. Researchers deriving SM masses from the phi-ladder or resolving the hierarchy problem cite this to rule out trivial endpoints. The proof is a one-line linear arithmetic reduction from the first conjunct of the scale_from_ledger hypothesis.
Claim. If the electroweak scale arises from ledger structure with $1 < phi < 2$, then $phi ≠ 1$.
background
The module E-004 treats the electroweak scale v ≈ 246 GeV as set by the phi-ladder rather than a separate hierarchy problem. The hypothesis scale_from_ledger encodes two parts: the interval 1 < phi < 2 together with uniformity of masses across rungs. This rests on the upstream definition scale(k) := phi^k from the cosmology module, which supplies the rung-based mass formula.
proof idea
One-line wrapper that applies linarith to the first conjunct of scale_from_ledger, which asserts the strict inequality 1 < phi.
why it matters
The result excludes the degenerate endpoint phi = 1 inside the electroweak derivation, feeding downstream claims such as ew_scale_implies_phi_window and no_fine_tuning. It aligns with the framework forcing of phi as self-similar fixed point (T6) and the Recognition Composition Law. The module records that full v derivation from the ledger remains blocked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.