phi_gt_one'
plain-language theorem explainer
The lemma asserts that the golden ratio exceeds unity, serving as a basic inequality in Recognition Science models of quantum field theory running couplings. Physicists deriving scale hierarchies or symmetry breaking from φ-ladders cite this to establish positive exponents in energy scaling. A single linear arithmetic tactic discharges the claim from the stronger bound φ > 1.5.
Claim. The golden ratio satisfies $φ > 1$.
background
The module derives running couplings from φ-ladder scaling, where different rungs correspond to energy scales and J-cost optimization varies accordingly. The golden ratio φ is the self-similar fixed point from the forcing chain. The upstream lemma phi_gt_onePointFive supplies the tighter bound (1.5 : ℝ) < φ, obtained by showing √5 > 2 and simplifying the closed-form expression.
proof idea
One-line wrapper that applies the linarith tactic directly to the hypothesis phi_gt_onePointFive.
why it matters
This lemma feeds the symmetry-breaking result in the Higgs mechanism and the phi_ladder_hierarchy theorem, which shows φ^n > 1 for n > 0. It supports the Recognition framework step where φ is forced as the fixed point, enabling exponential hierarchies in running couplings and the transition to D = 3 dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.