phi_gt_one
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 in Recognition Science
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)).
scope and limits
- Does not compute a decimal approximation of φ.
- Does not prove the quadratic equation satisfied by φ.
- Does not relate φ to the conjugate ψ or to the product φψ = -1.
- Does not connect the inequality to physical constants such as α or G.
formal statement (Lean)
71theorem phi_gt_one : 1 < φ := by
proof body
Tactic-mode proof.
72 unfold φ
73 have h := sqrt5_pos
74 have h2 : Real.sqrt 5 > 1 := by
75 rw [show (1:ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
76 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
77 linarith
78
79/-- **THEOREM: φ² = φ + 1** (the defining equation). -/