phi_is_self_similar
plain-language theorem explainer
φ satisfies the self-similarity equation r² = r + 1. Researchers tracing the Recognition Science forcing chain cite this when establishing that the golden ratio emerges as the fixed point of J-cost minimization. The proof is a direct one-line application of the algebraic identity phi_sq_eq.
Claim. $φ^2 = φ + 1$, where $φ = (1 + √5)/2$ is the golden ratio and self-similarity means the ratio $r$ obeys $r^2 = r + 1$.
background
The PhiEmergence module derives the golden ratio from J-cost minimization in the Recognition Science framework. IsSelfSimilar r is the predicate r² = r + 1. The local setting is the emergence of φ as the unique positive solution under the Recognition Composition Law and the eight-tick octave structure. Upstream, Constants.phi_sq_eq states the key identity φ² = φ + 1 obtained from the quadratic x² - x - 1 = 0 by unfolding the definition of phi and applying the square-root identity for 5. NumberTheory.PhiLadderLattice supplies an equivalent algebraic form of the same identity.
proof idea
This is a one-line wrapper that applies the lemma phi_sq_eq from IndisputableMonolith.Constants. The lemma unfolds the definition of phi, invokes Real.sq_sqrt on the non-negative argument 5, and finishes by ring_nf and linear_combination.
why it matters
The result feeds phi_unique_positive (which proves uniqueness of the positive root), H_StableIffPhiLadder (the hypothesis that stable positions coincide with the φ-ladder), phi_series_sum, and phi_harmonic_forced in Cost.FrequencyLadder. It realizes T6 of the forcing chain, where phi is forced as the self-similar fixed point. It also supplies the ratio needed for the phi-ladder mass formula and the alpha band bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.