phi_gt_one
plain-language theorem explainer
The golden ratio exceeds one, permitting geometric growth in mass hierarchies on the phi-ladder. Physicists modeling electroweak symmetry breaking in Recognition Science cite the result to remove fine-tuning from the Higgs vacuum expectation value near 246 GeV. The proof is a one-line term that directly applies the pre-established inequality for phi from the constants module.
Claim. The golden ratio satisfies $1 < phi$, where $phi = (1 + sqrt(5))/2$.
background
The module E-004 formalizes the Recognition Science structural account of the electroweak scale. It treats the Higgs vacuum expectation value v ≈ 246 GeV as setting all Standard Model masses through the phi-ladder, eliminating the hierarchy problem by replacing radiative corrections with geometric scaling. Upstream lemmas establish the inequality via explicit real-arithmetic bounds on sqrt(5), confirming phi > 1 from its closed-form definition.
proof idea
The proof is a term-mode one-liner that directly invokes the lemma one_lt_phi from the Constants module.
why it matters
The result supplies the geometric-growth premise required by sibling declarations such as no_fine_tuning and ew_scale_implies_phi_window. It instantiates the T6 self-similar fixed point of the forcing chain, ensuring mass ratios appear as powers of phi. The module records that a complete ledger-boundary derivation of the scale remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.