phi_gt_one
plain-language theorem explainer
The golden ratio satisfies φ > 1. Researchers establishing bounds on self-similar scale factors in discrete ledgers cite this when placing φ on the phi-ladder. The proof unfolds the closed-form expression and compares square roots before applying linear arithmetic.
Claim. Let $φ = (1 + √5)/2$. Then $φ > 1$.
background
The PhiForcing module derives φ from self-similarity in a discrete ledger equipped with J-cost. Self-similar scales must obey J(x) = 0 while x ≠ 1, which forces the quadratic x² = x + 1 whose positive root is φ. The module imports J-cost from Cost and discreteness constraints from DiscretenessForcing; the local setting is that non-trivial self-similarity requires a scale ratio cost-equivalent to unity.
proof idea
The tactic proof first unfolds φ via simp, then proves √5 > 2 by comparing √5 > √4 = 2 using the strict monotonicity of the square-root function on positives, and finishes with linarith.
why it matters
This inequality supplies the lower bound needed for the sibling results φ < 2, 1.618 < φ < 1.619 and the full set of phi-ladder bounds in the same module. It anchors the forcing step T6 where φ is identified as the unique self-similar fixed point, and it is presupposed by the mass formula yardstick · φ^(rung - 8 + gap(Z)). No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.