ew_scale_implies_phi_ne_one
plain-language theorem explainer
Electroweak-scale structure excludes the degenerate endpoint phi equals 1. A researcher studying the hierarchy problem in the Recognition Science framework would cite this result to confirm that the phi-ladder forces phi strictly between 1 and 2. The proof applies linear arithmetic directly to the lower bound in the scale_from_ledger hypothesis.
Claim. If the electroweak scale arises from the ledger via the phi-ladder (i.e., $1 < phi < 2$ and mass equality on all rungs), then $phi neq 1$.
background
The module E-004 formalizes the RS structural framework for the electroweak scale, stating that v approximately 246 GeV sets all SM masses with no hierarchy problem because masses come from the phi-ladder rather than radiative corrections. The hypothesis scale_from_ledger encodes this as the conjunction (1 < phi and phi < 2) together with mass equality across rungs. The upstream definition scale (k : Nat) : Real := phi ^ k supplies the explicit power-law form of the ladder.
proof idea
One-line wrapper that applies linarith to the first conjunct of scale_from_ledger.
why it matters
This theorem closes the lower endpoint of the allowed interval for phi in the electroweak sector and supports the module claim that the hierarchy problem dissolves because masses arise from the phi-ladder. It aligns with T6 forcing of phi as the self-similar fixed point and the requirement that phi lie in (1,2) to match observed scales without fine-tuning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.