phi
plain-language theorem explainer
Definition of the golden ratio as the concrete real number (1 + sqrt(5))/2. Authors building gap-series coefficients and phi-ladder normalizations in Recognition Science pipelines cite it for rung indexing and mass formulas. It is realized by a direct noncomputable assignment with no lemmas or hypotheses.
Claim. The golden ratio is the positive real number defined by $phi := (1 + sqrt(5))/2$.
background
The Pipelines module supplies auxiliary constructions for gap series that appear in Recognition Science derivations. The supplied definition makes the numerical value of the golden ratio available before the GapSeries namespace, which indexes coefficients via n.succ and references the conventional log(1+x) series at x = z/phi.
proof idea
Direct noncomputable definition that assigns the standard closed-form algebraic expression. No tactics or upstream lemmas are invoked inside the body.
why it matters
Supplies the concrete value of phi that anchors the self-similar fixed point in the forcing chain and the phi-ladder used for mass formulas. It supports sibling constructions such as coeff, partialSum, and f_gap inside the same module, though no explicit used_by edges are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.