IsSelfSimilarRatio
plain-language theorem explainer
A positive real number r satisfies the self-similar ratio condition precisely when its square equals itself plus one. Frequency ladder constructions cite this predicate to single out the golden ratio as the lowest-cost scale-invariant resonance. The definition appears in proofs that the first phi-harmonic above any base frequency is unique. It is introduced as a direct equational definition with no additional proof steps required.
Claim. A positive real number $r$ is said to be a self-similar ratio if $r^2 = r + 1$.
background
The FrequencyLadder module defines the J-cost of a positive ratio r by the formula one-half times (r plus its reciprocal) minus one. Self-similar ratios are those fixed by the map sending r to one plus one over r. The module documentation explains that the golden ratio is the unique positive solution to this fixed-point equation and therefore supplies the minimal-cost non-trivial resonance for any oscillating system at frequency f. This local setting supports the step that defines the first phi-ladder harmonic as the base frequency multiplied by phi.
proof idea
The declaration consists of a direct definition that equates the predicate to the quadratic equation r squared equals r plus one. No lemmas are invoked and the body contains only the equational abbreviation.
why it matters
This predicate is required by the structure PhiHarmonicForced to record that the harmonic ratio equals phi and is self-similar. It is also the hypothesis in the uniqueness theorem for positive self-similar ratios. In the broader framework it realizes the forcing of phi as the self-similar fixed point in the T6 step of the unified chain. The module documentation ties it to the justification for phi-harmonics in resonance calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.