phi
plain-language theorem explainer
The golden ratio is defined as the positive real (1 + sqrt(5))/2. Recognition Science ledger-uniqueness arguments cite this value as the fixed point forced by the J-cost condition. The declaration is a direct noncomputable definition in the reals with no further computation.
Claim. Let $phi$ be the golden ratio defined by $phi := (1 + sqrt(5))/2$.
background
The module treats Gap 9: why any discrete conservative system must be isomorphic to the RS ledger using specifically phi, the 3-cube, and the 8-tick cycle. The local objection is that discreteness permits many ratios; the resolution is that phi is the unique positive solution to the fixed-point equation x^2 = x + 1 arising from the J-cost constraint J(x) = J(1/x) with minimal curvature. The upstream point definition supplies an interval primitive used elsewhere in the module but is not invoked by this declaration.
proof idea
Direct definition that encodes the standard closed-form expression for the golden ratio.
why it matters
This supplies the concrete value of phi required by the ledger-uniqueness theorem. It is referenced by the sibling results phi_unique_fixed_point and cost_fixed_point_is_phi. In the framework it realizes the T6 step that forces phi as the self-similar fixed point of the J-cost (T5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.