IsSelfSimilarRatio
Defines the predicate IsSelfSimilarRatio r to hold precisely when the real number r obeys the quadratic r² = r + 1. Researchers establishing minimal-cost resonances in the φ-ladder cite this predicate when they need the algebraic condition for scale-invariant ratios. The declaration is a direct equational abbreviation with no further computation or lemmas.
claimA real number $r$ is a self-similar ratio when it satisfies the equation $r^2 = r + 1$.
background
The module Cost.FrequencyLadder introduces the φ-ladder as the minimal-cost bridge between frequencies via the J-cost function J(r) = ½(r + r⁻¹) − 1. Self-similar ratios are those invariant under the recursion r = 1 + 1/r. The module doc states that φ is the unique positive fixed point of this recursion, which rearranges directly to the quadratic r² = r + 1. This definition isolates the algebraic condition used downstream to identify φ as the unique positive root among all r > 1.
proof idea
The declaration is a direct definition that sets IsSelfSimilarRatio r equal to the equation r² = r + 1. No lemmas or tactics are invoked; the body simply introduces the predicate for the quadratic fixed-point condition.
why it matters in Recognition Science
This predicate is the building block for PhiHarmonicForced, which asserts that the first harmonic of any frequency f is f × φ and that the ratio is the unique self-similar ratio. It supplies the algebraic content for the T6 step in the forcing chain where φ is forced as the self-similar fixed point. The downstream theorems phi_is_self_similar and phi_unique_self_similar apply the predicate to conclude that f × φ is the minimal-cost non-trivial resonance above f.
scope and limits
- Does not assert existence of solutions to the equation.
- Does not select which positive root is intended.
- Does not relate the equation to the J-cost function.
- Does not prove uniqueness of any root.
Lean usage
theorem phi_is_self_similar : IsSelfSimilarRatio phi := phi_sq_eqformal statement (Lean)
47def IsSelfSimilarRatio (r : ℝ) : Prop := r ^ 2 = r + 1
proof body
Definition body.
48
49/-- φ is a self-similar ratio. -/