phi_gt_one
plain-language theorem explainer
The golden ratio φ satisfies 1 < φ. Researchers building the phi-ladder or invoking the self-similar fixed point in Recognition Science cite this ordering when establishing rung heights and mass formulas. The proof unfolds the definition of φ, invokes sqrt5_pos, shows sqrt(5) > 1 by comparing square roots to sqrt(1), and finishes with linarith.
Claim. $1 < φ$ where $φ = (1 + √5)/2$.
background
The PhiRing module introduces the golden ratio φ as the positive root of the quadratic x² - x - 1 = 0, placed inside the algebraic layer that supports Recognition Composition Law and the phi-ladder. It imports Cost and CostAlgebra to keep J-cost and defectDist operations available for later mass formulas. The immediate upstream result sqrt5_pos supplies 0 < √5, while the PrimitiveDistinction.from theorem supplies the seven-axiom origin of the structural conditions that justify introducing φ at all.
proof idea
The tactic proof unfolds φ, applies the theorem sqrt5_pos, proves √5 > 1 by rewriting 1 as √1 and invoking Real.sqrt_lt_sqrt, then closes with linarith.
why it matters
This ordering is a prerequisite for the phi-ladder rung indexing and the T6 self-similar fixed-point step in the forcing chain. It sits immediately before phi_equation and the phi_psi identities in the same module, enabling later claims about the eight-tick octave and D = 3. No downstream uses are recorded yet, but the result closes a basic positivity gap required by any mass formula of the form yardstick · φ^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.