phi_pos
The golden ratio φ satisfies φ > 0. Researchers establishing the ordering of the phi-ladder or the Berry creation threshold at φ^{-1} cite this fact when building the mass formula or the T6 self-similar fixed point. The proof unfolds the explicit definition of φ and reduces the claim to the known positivity of sqrt(5) via linear arithmetic.
claimLet φ = (1 + √5)/2 denote the golden ratio. Then φ > 0.
background
In the Algebra.PhiRing module the golden ratio φ is introduced as the positive root of x² - x - 1 = 0, serving as the self-similar fixed point forced at step T6 of the UnifiedForcingChain. The module imports Cost and CostAlgebra to support J-cost calculations and the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The upstream theorem sqrt5_pos states that √5 > 0 and supplies the sole algebraic input required here.
proof idea
The proof unfolds the definition of φ as (1 + √5)/2, invokes the upstream result sqrt5_pos to obtain a positive radicand, and concludes the strict inequality by linear arithmetic.
why it matters in Recognition Science
This positivity anchors the ordering properties of the phi-ladder that appear in the mass formula (yardstick · φ^(rung - 8 + gap(Z))) and the Berry threshold at φ^{-1}. It is a prerequisite for the sibling lemmas phi_gt_one and phi_equation that feed the eight-tick octave (T7) and the derivation of D = 3 spatial dimensions (T8). No direct downstream citations are recorded, yet the result closes a basic algebraic gap in the forcing chain.
scope and limits
- Does not establish any numerical bound on φ beyond strict positivity.
- Does not address the conjugate root ψ = (1 - √5)/2.
- Does not invoke or prove the Recognition Composition Law.
formal statement (Lean)
65theorem phi_pos : 0 < φ := by
proof body
Term-mode proof.
66 unfold φ
67 have h := sqrt5_pos
68 linarith
69
70/-- φ > 1 -/