phi_is_self_similar
plain-language theorem explainer
The golden ratio φ satisfies φ² = φ + 1. Frequency-ladder constructions cite this to identify the minimal-cost resonance above any base frequency f. The proof is a one-line wrapper that applies the algebraic identity phi_sq_eq from the constants module.
Claim. The golden ratio $φ$ satisfies $φ^2 = φ + 1$.
background
The J-cost function is J(r) = ½(r + r^{-1}) − 1. A self-similar ratio r satisfies the fixed-point equation r² = r + 1. The module proves that φ is the unique positive root of this equation and therefore the generator of the minimal-cost φ-ladder harmonics f × φ^n.
proof idea
The proof is a one-line wrapper that applies the lemma phi_sq_eq establishing φ² = φ + 1.
why it matters
This supplies the self-similar property required by phi_harmonic_forced and by H_StableIffPhiLadder. It fills the T6 step of the forcing chain in which φ is forced as the self-similar fixed point. The result anchors the claim that the first φ-harmonic is the minimal-cost resonance above any frequency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.