phi_pos
plain-language theorem explainer
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.
Claim. Let φ = (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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.