phi_unique_fixed_point
plain-language theorem explainer
The golden ratio is the unique positive real satisfying the quadratic x squared equals x plus one. Researchers closing the ledger uniqueness gap in Recognition Science cite this to fix the cost function fixed point. The proof rewrites the equation, factors the quadratic over the reals, and splits cases with the no-zero-divisors lemma before discarding the negative root by positivity.
Claim. Let $x$ be a positive real number. If $x^2 = x + 1$, then $x$ equals the golden ratio.
background
The Meta.LedgerUniqueness module resolves the objection that other discrete conservative structures might exist by proving each component of the RS ledger is the unique solution to its forcing constraint. Here the relevant constraint is the cost fixed point: the J-cost induced by a multiplicative recognizer or observer event must satisfy J(x) = J(1/x) with minimal curvature, which algebraically reduces to the quadratic. Upstream results supply the cost definitions from MultiplicativeRecognizerL4 and ObserverForcing together with the mul_eq_zero fact that LogicInt has no zero divisors.
proof idea
The tactic proof introduces the positive real and the equation, rewrites to x squared minus x minus one equals zero, factors the left side as (x minus phi) times (x minus psi) where psi is the negative root, then applies mul_eq_zero to split into cases. The positive case yields the claim directly; the negative case contradicts x greater than zero after substitution.
why it matters
This supplies the phi leg of the uniqueness argument in Gap 9. It is invoked by cost_fixed_point_is_phi and feeds complete_ledger_uniqueness together with rs_ledger_is_unique, which together show that any discrete conservative system is isomorphic to the RS ledger using phi, Q3, and the eight-tick cycle. The result directly addresses the module's motivating critique that a different ratio than phi might satisfy the same constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.