phi_unique_self_similar
plain-language theorem explainer
The golden ratio φ is the unique positive real satisfying the self-similarity equation r² = r + 1. Researchers constructing the φ-ladder in Recognition Science cite this to select the minimal-cost resonance above any given frequency. The proof subtracts the quadratic for φ from that for r, factors the difference via nlinarith, and discards the extraneous root using positivity of r and φ together with mul_eq_zero.
Claim. Let φ be the golden ratio. If r > 0 and r² = r + 1, then r = φ.
background
The module proves that φ is the minimal-cost non-trivial ratio on the frequency ladder. The J-cost function J(r) = ½(r + r⁻¹) − 1 evaluates the cost of any positive ratio r. A self-similar ratio satisfies the fixed-point equation r² = r + 1, which is the defining relation for φ. Upstream lemmas supply phi_sq_eq (φ² = φ + 1) and one_lt_phi (1 < φ) to control signs; mul_eq_zero from the integers logic supplies the zero-divisor property used in the case split.
proof idea
Unfold IsSelfSimilarRatio to obtain r² = r + 1. Invoke phi_sq_eq, phi_pos and one_lt_phi, then apply nlinarith to reach (r − φ)(r + φ − 1) = 0. Apply mul_eq_zero to split into cases. The first case is ruled out by linarith; the second is ruled out by exfalso with nlinarith, using that r + φ − 1 > 0.
why it matters
This uniqueness is invoked by phi_harmonic_forced to guarantee that the ratio of the φ-harmonic equals φ and satisfies self-similarity. It fills the T6 step of the forcing chain where φ is forced as the self-similar fixed point. The module doc states that the result justifies defining f_phi_rung1 := Mode1 × φ as the first minimal-cost resonance above any frequency f.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.