phi
plain-language theorem explainer
The declaration supplies the golden ratio φ as the explicit real number (1 + √5)/2. Number theorists and Recognition Science modelers cite it when building the multiplicative phi-ladder {φ^r} for rung indices and reciprocal cost symmetry. The definition is a direct closed-form assignment with no auxiliary lemmas or reductions.
Claim. Let $φ = (1 + √5)/2$, the unique positive real solution of the quadratic equation $x^2 = x + 1$ (equivalently $x = 1 + 1/x$).
background
The module formalizes the phi-ladder lattice forced by RS theorem T6: self-similarity on the positive reals selects the golden ratio as fixed point. On ℝ>0 the ladder is the geometric sequence {φ^r : r ∈ ℤ}; under t = log x it becomes the additive lattice {r · log φ}. The definition phi supplies the base constant for all subsequent rung and lattice constructions in the file.
proof idea
Direct definition: the body is the closed-form algebraic expression for the positive root of x² - x - 1 = 0. No tactics or upstream lemmas are invoked; the assignment is immediate.
why it matters
This definition anchors the entire phi-ladder lattice module and therefore the discrete hierarchy used for mass formulas and J-cost reciprocity. It realizes the self-similar fixed point required by T6 and supplies the generator for the eight-tick octave structure downstream. The module lists it as the first of the zero-sorry facts that enable phiRung, phiLatticePoint, and cost_phi_ladder_reciprocal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.