phi_conjugate_self_similar
plain-language theorem explainer
The theorem verifies that the conjugate root of the golden-ratio equation satisfies the self-similarity relation r² = r + 1. Workers on the phi-ladder and J-cost minimization in Recognition Science cite it to treat both roots symmetrically before selecting the positive one. The proof is a direct algebraic expansion that normalizes the square of sqrt(5) and cancels terms via ring tactics.
Claim. Let φ' = (1 - √5)/2. Then (φ')² = φ' + 1.
background
The PhiEmergence module derives the golden ratio from J-cost minimization. The predicate IsSelfSimilar(r) is defined to hold exactly when r² = r + 1; this encodes the fixed-point property under the Recognition Composition Law. The theorem applies the predicate to the conjugate root, the second solution of the characteristic equation x² - x - 1 = 0.
proof idea
The term proof unfolds IsSelfSimilar on φ_conjugate, introduces the non-negativity of √5 and the identity (√5)² = 5, then applies ring_nf followed by a targeted rewrite and a final ring normalization to obtain the required equality.
why it matters
The result supplies the algebraic symmetry needed for the phi-emergence step (T6) that forces the self-similar fixed point. It completes the pair of roots inside the PhiEmergence module before downstream selection of the positive root for the phi-ladder and mass formulas. No downstream uses are recorded yet, leaving open how the negative conjugate interacts with positive-definite quantities in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.