phi_unique_pos
plain-language theorem explainer
The golden ratio is the unique positive real satisfying the quadratic x squared equals x plus one. Researchers formalizing the inevitability theorem in Recognition Science cite this result to pin down the fixed point of the J-cost structure. The term proof exhibits the candidate (1 plus square root of 5) over 2, verifies positivity and the equation with sqrt_pos, linarith, ring_nf and ring, then rules out alternatives via nlinarith on non-negative squares.
Claim. There exists a unique positive real number $x$ such that $x^2 = x + 1$.
background
The InevitabilityEquivalence module equates abstract inevitability slogans with concrete CPM and cost conditions. The upstream inevitability theorem asserts that any alternative zero-parameter framework deriving observables must either match the RS cost and selection or violate at least one necessity gate. The present result supplies the unique positive root required for the concrete formulation of inevitability.
proof idea
The term proof begins by using the explicit witness (1 + sqrt 5)/2. Constructor splits the goal into positivity (discharged by sqrt_pos.mpr and linarith) and the quadratic identity (discharged by sq_sqrt, ring_nf, rw and ring). Uniqueness is handled by nlinarith applied to the non-negative squares of the differences from both roots together with auxiliary non-negative terms.
why it matters
This theorem is invoked directly by the concrete_inevitability definition and by the summary theorem in the same module. It supplies the uniqueness clause that converts the abstract inevitability claim into a concrete statement about the J-minimizer. In the forcing chain it realizes the self-similar fixed point required for the eight-tick octave and the derivation of spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.