cost_fixed_point_is_phi
plain-language theorem explainer
Any positive real number satisfying the quadratic x squared equals x plus one must equal the golden ratio phi. Recognition Science arguments on ledger uniqueness cite this to fix the cost function value at phi rather than some other ratio. The proof is a direct one-line reduction to the prior uniqueness theorem for the fixed point equation.
Claim. For every positive real number $x$, if $x^2 = x + 1$, then $x = phi$, where $phi$ is the golden ratio.
background
The Meta.LedgerUniqueness module resolves the objection that discreteness alone permits many possible ledgers by proving each structural choice is forced. For the golden ratio component, the cost function fixed point constraint requires J(x) equals J(1/x) with minimal curvature; the only positive solution is the fixed point of the quadratic x squared equals x plus one. The upstream theorem phi_unique_fixed_point states that phi is the unique positive solution to x squared equals x plus one.
proof idea
The proof is a one-line wrapper that applies the theorem phi_unique_fixed_point establishing uniqueness of the positive root.
why it matters
This supplies the phi uniqueness piece inside the ledger uniqueness argument, which concludes that any discrete conservative system is isomorphic to the RS ledger using phi, the three-dimensional cube, and the eight-tick cycle. It aligns with the forcing chain step in which J-uniqueness forces phi as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.