phi_unique_positive
plain-language theorem explainer
The theorem proves that the golden ratio φ is the unique positive real satisfying the self-similarity equation r² = r + 1. Researchers deriving the phi-ladder of stable positions from J-cost minimization would cite this uniqueness result when closing the algebraic characterization of fixed points. The proof subtracts the defining equations for r and φ, factors the difference, applies the zero-product property, and discards the negative root by positivity together with φ > 1.
Claim. Let $φ$ denote the golden ratio. For every real number $r > 0$, if $r^2 = r + 1$ then $r = φ$.
background
The module Φ-Emergence derives the golden ratio from J-cost minimization. The predicate IsSelfSimilar(r) is defined by the equation r² = r + 1. An upstream theorem establishes that φ itself satisfies this equation. The local setting is the emergence of discrete structure from the Recognition Composition Law and the self-similar fixed-point condition.
proof idea
The proof unfolds IsSelfSimilar for both r and φ. It subtracts the equations to obtain r² - φ² = r - φ, factors the left side as (r - φ)(r + φ), and rearranges to (r - φ)(r + φ - 1) = 0. The zero-product theorem mul_eq_zero produces two cases. The first yields r = φ by linarith. The second produces r = 1 - φ, which is contradicted by r > 0 and the fact that φ > 1.
why it matters
This uniqueness result is required by the downstream hypothesis H_StableIffPhiLadder, which asserts that stable positions coincide exactly with the phi-ladder. It fills step T6 of the UnifiedForcingChain, where phi is forced as the self-similar fixed point. The lemma supplies the algebraic closure needed before constructing the discrete ladder of mass and energy levels in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.