phi_pos
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 in Recognition Science
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.
scope and limits
- Does not establish uniqueness of φ as the positive root of x² - x - 1 = 0.
- Does not prove irrationality of φ or its continued-fraction properties.
- Does not connect φ to the mass formula or Berry creation threshold.
- Does not address the Poisson summation conjecture stated as a hypothesis structure in the same module.
formal statement (Lean)
57theorem phi_pos : 0 < phi := by
proof body
Tactic-mode proof.
58 unfold phi
59 have h5 : 0 ≤ Real.sqrt 5 := Real.sqrt_nonneg 5
60 have : (0 : ℝ) < 1 + Real.sqrt 5 := by linarith
61 linarith
62
63/-- `φ` is not zero. -/