self_similarity_forces_phi
plain-language theorem explainer
The theorem proves that the only positive real number satisfying x squared equals x plus one is the golden ratio phi. Researchers deriving constants from the meta-principle in recognition frameworks cite this to close the self-similarity step. The proof reduces the input equation to a quadratic, factors the polynomial over the reals, and discards the negative root by case analysis on the product being zero together with the positivity hypothesis.
Claim. Let $x$ be a positive real number satisfying $x^2 = x + 1$. Then $x$ equals the golden ratio $phi$.
background
The module encodes the Meta-Principle that empty recognition is impossible, which forces a ledger structure for any recognition process. Self-similarity on that ledger then imposes the fixed-point equation $x^2 = x + 1$. The upstream Chain structure supplies the minimal sequence model with a recognition relation R, while the MP definition directly states the foundational negation of self-recognition on the empty structure. The mul_eq_zero result from the integers-from-logic layer supplies the zero-divisor-free property used for case splitting.
proof idea
The tactic proof rewrites the hypothesis as $x^2 - x - 1 = 0$, introduces the square root of five via norm_num and sq_sqrt, then factors the quadratic into a product of linear terms by ring_nf. It applies mul_eq_zero to obtain two cases. The first case matches the definition of phi by linarith; the second produces a negative value that contradicts positivity via sqrt_lt_sqrt and linarith.
why it matters
This declaration supplies the self-similarity step inside the DerivationChain structure, which records the path from MP through ledger closure to phi. It is invoked verbatim by the phi_unique wrapper. In the Recognition Science framework it realizes the forcing of phi as the self-similar fixed point (T6) after the J-uniqueness relation (T5). No scaffolding remains; the result is fully proved and feeds directly into the constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.