phi_unique_self_similar
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.
claimLet φ 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 in Recognition Science
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.
scope and limits
- Does not establish uniqueness among negative reals.
- Does not derive a numerical approximation of φ.
- Does not prove J-cost minimality without further lemmas on the ladder.
- Does not address the full eight-tick octave or spatial dimension D = 3.
formal statement (Lean)
56theorem phi_unique_self_similar {r : ℝ} (hr_pos : 0 < r)
57 (hr_ss : IsSelfSimilarRatio r) : r = phi := by
proof body
Tactic-mode proof.
58 unfold IsSelfSimilarRatio at hr_ss
59 have hphi_sq := phi_sq_eq
60 have hphi_pos := phi_pos
61 have hphi_gt1 := one_lt_phi
62 have hdiff : (r - phi) * (r + phi - 1) = 0 := by nlinarith
63 rcases mul_eq_zero.mp hdiff with h | h
64 · linarith
65 · exfalso; nlinarith
66
67/-- φ is the cost fixed point: φ = 1 + 1/φ.
68 Follows directly from φ² = φ + 1. -/