phi
The Pipelines module supplies the golden ratio as the explicit real (1 + sqrt(5))/2 for gap-series coefficient work. Researchers constructing phi-ladder mass formulas or recognition-weighted stellar models would import this value to index tiers. The declaration is a direct assignment with no lemmas or reductions.
claimLet $phi = (1 + sqrt(5))/2$ be the golden ratio used as base for gap-series coefficients.
background
Recognition Science obtains phi as the self-similar fixed point satisfying the J-cost equation J(x) = (x + 1/x)/2 - 1. The present definition supplies a concrete real for the GapSeries namespace inside Pipelines, where coefficients are indexed via successor from ArithmeticFromLogic.succ. Upstream structures such as PhiForcingDerived.of record the J-cost scaffolding and DAlembert.LedgerFactorization.of calibrates the underlying ledger from which the fixed point is extracted.
proof idea
The declaration is a direct noncomputable definition that evaluates the closed-form expression using Real.sqrt and division in the reals.
why it matters in Recognition Science
This constant anchors the phi-ladder referenced in T6 of the forcing chain and supplies the numerical base for gap-series expansions that feed NucleosynthesisTiers.of and MassToLight.via. It closes the concrete-real requirement for downstream coefficient definitions without introducing new hypotheses.
scope and limits
- Does not derive phi from the J-uniqueness equation T5.
- Does not attach units or scaling factors.
- Does not prove algebraic properties such as irrationality.
- Does not index any phi-ladder rung.
formal statement (Lean)
9noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
proof body
Definition body.
10
11namespace GapSeries
12
13/-- Gap-series coefficient (1-indexed by design via `n.succ`).
14The conventional closed-form uses the series of `log(1+x)` at `x = z/φ`.
15This definition is dimensionless and self-contained. -/