ew_scale_implies_phi_ne_one
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not compute a numerical value for phi.
- Does not derive the electroweak scale from first principles.
- Does not address Planck-scale matching or higher rungs.
formal statement (Lean)
60theorem ew_scale_implies_phi_ne_one (h : scale_from_ledger) : phi ≠ 1 := by
proof body
Term-mode proof.
61 linarith [h.1.1]
62
63/-- Electroweak-scale structure excludes the upper endpoint `phi = 2`. -/