phi_unique
plain-language theorem explainer
The declaration shows that the golden ratio φ is the unique positive real root of the equation x² = x + 1. Workers deriving constants from self-similar closure in recognition models cite this to eliminate alternative fixed points. The proof is a one-line wrapper that invokes the self-similarity forcing result.
Claim. The unique positive real number $x$ satisfying $x^2 = x + 1$ equals the golden ratio $φ$.
background
The RRF foundation module treats the meta-principle as a theorem rather than an axiom: nothing cannot recognize itself, which forces a ledger structure whose self-similar closure yields φ. RRF itself is the local non-sealed recognition field interface, an abbreviation for maps from (Fin 4 → ℝ) to ℝ. The upstream lemma self_similarity_forces_phi states that self-similar ledger closure forces φ as the only positive solution to x² = x + 1 and supplies the quadratic-formula argument.
proof idea
The proof is a one-line wrapper that applies the theorem self_similarity_forces_phi, which reduces the quadratic x² - x - 1 = 0, invokes positivity to discard the negative root, and identifies the surviving root with φ.
why it matters
This uniqueness result is invoked by the master theorem concrete_implies_no_alternatives and by the noFreeParameters theorem in InevitabilityEquivalence; together they close the chain from the meta-principle through ledger closure to unique constants. It realizes the T6 forcing step in which φ is fixed as the self-similar point, removing free parameters from the derivation of c, ħ, G and α.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.