IsSelfSimilar
plain-language theorem explainer
A real number r is self-similar precisely when it satisfies the quadratic equation r squared equals r plus one. Researchers working on phi emergence in Recognition Science cite this definition when characterizing the golden ratio as the fixed point of J-cost minimization and when proving alignment between stable positions and the phi-ladder. The declaration is a direct definitional equality with no lemmas, tactics, or additional proof obligations.
Claim. A real number $r$ is self-similar if it satisfies the equation $r^2 = r + 1$.
background
The PhiEmergence module derives the golden ratio from J-cost minimization under the heading of φ-Emergence. Self-similarity is introduced as the algebraic fixed-point condition that forces phi as the unique positive solution. The phi-ladder is the discrete set of powers generated from this condition, appearing in downstream statements such as H_StableIffPhiLadder which equates stable positions exactly with membership in PhiLadder.
proof idea
The declaration is a definition whose body is the direct equality r^2 = r + 1. No lemmas from upstream results are applied and no tactics are used; it functions as a pure abbreviation for unfolding in later theorems such as phi_is_self_similar and phi_unique_positive.
why it matters
This definition supplies the core equation for T6 in the unified forcing chain, where phi is forced as the self-similar fixed point. It feeds directly into phi_is_self_similar, phi_unique_positive, phi_series_sum, and H_StableIffPhiLadder, the last of which asserts that stable positions coincide with the phi-ladder. The placement closes the algebraic step between J-cost minimization and discrete quantization on the ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.