phi_pos
plain-language theorem explainer
The golden ratio φ satisfies φ > 0. Researchers deriving constants from self-similar closure in the Meta-Principle would cite this bound when placing limits on the phi-ladder. The proof unfolds the explicit definition of φ, invokes positivity of the square root of five, and closes with linear arithmetic.
Claim. $0 < phi$ where $phi = (1 + sqrt(5))/2$ is the golden ratio fixed point forced by self-similar closure.
background
The Meta-Principle module formalizes the statement that nothing cannot recognize itself, which forces a ledger and then self-similar closure. This closure yields the golden ratio φ satisfying φ² = φ + 1, as defined in the sibling declaration phi. Positivity of φ is a prerequisite for subsequent steps that produce constants in RS-native units and the phi-ladder mass formula.
proof idea
The term-mode proof unfolds the definition of phi, applies Real.sqrt_pos.mpr to the fact that 0 < 5, and finishes with linarith.
why it matters
This basic positivity fact supports the derivation chain from the Meta-Principle to the self-similar fixed point (T6). It underpins sibling results such as phi_sq and self_similarity_forces_phi, which in turn enable the eight-tick octave and D = 3. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.