phi_pos
plain-language theorem explainer
The golden ratio φ satisfies φ > 0. Researchers constructing the phi-ladder lattice cite this fact to anchor the geometric sequence of complexity levels on the positive reals. The proof unfolds the explicit definition of φ, invokes non-negativity of the square root, and closes via linear arithmetic on the reals.
Claim. $0 < (1 + √5)/2$
background
The phi-ladder lattice formalizes the discrete hierarchy of complexity levels forced by self-similarity. φ denotes the golden ratio (1 + √5)/2, generating the geometric sequence {φ^r : r ∈ ℤ} on ℝ_{>0}. On the log scale this becomes the additive lattice {r · log φ : r ∈ ℤ}, which admits Poisson summation. The module also introduces phiRung x as ⌊log_φ x⌋ and phiLatticePoint r as the corresponding lattice position, together with the reciprocal involution r ↦ -r.
proof idea
The proof unfolds the definition of phi, applies the non-negativity lemma for square roots to obtain 0 ≤ √5, deduces 0 < 1 + √5 by linear arithmetic, and concludes the claim by the same arithmetic tactic.
why it matters
This theorem supplies the foundational positivity of φ required for the phi-ladder lattice. It supports sibling results such as log_phi_pos, phi_gt_one, and cost_phi_ladder_reciprocal that rely on φ > 0 to define the geometric progression and its reciprocal symmetry. The result aligns with T6, where self-similarity forces the golden ratio as the fixed point, and enables the eight-tick octave with D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.