phi
plain-language theorem explainer
Defines the golden ratio φ = (1 + √5)/2 as a real constant. Dimension and counting arguments in the Verification layer cite it whenever the self-similar scale or the 45-gap arithmetic needs an explicit algebraic number. The body is a one-line closed-form assignment; no proof obligations.
Claim. Let $\varphi := (1 + \sqrt{5})/2 \in \mathbb{R}$. Equivalently, $\varphi$ is the unique positive root of $x^2 = x + 1$.
background
The Verification.Dimension module shows that RSCounting together with 45-gap synchronization forces spatial dimension $D = 3$, via an iff characterization that $D = 3$ is the only value satisfying the absolute counting-and-gap condition. The argument stays lightweight: it uses only lcm arithmetic and the RecogSpec layer.
In Recognition Science the same algebraic number $\varphi$ appears as the self-similar fixed point of the cost functional (forcing step T6). It is the unique positive solution of $\varphi^2 = \varphi + 1$, equivalently $\varphi = 1 + 1/\varphi$. Downstream mass ladders, tick periods, and coupling constants are written as powers of $\varphi$.
This definition simply pins that constant in Lean as a noncomputable real, so later lemmas (fixed-point identities, hopf-linking penalties, dimension witnesses) can refer to a single name.
proof idea
Pure definition: assign the closed form $(1 + \sqrt{5})/2$. No tactics, no lemmas. The companion statement that this value satisfies $\varphi^2 = \varphi + 1$ lives in the sibling phi_fixed_point.
why it matters
Supplies the concrete real used throughout the dimension-rigidity development in this module (counting gaps, linking uniqueness, $D = 3$ witnesses). In the broader framework it is the T6 fixed point: once the J-cost is forced unique, self-similarity selects $\varphi$, which then sets the eight-tick octave scale, the $\varphi$-ladder for masses, and the native units $c = 1$, $\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$. Without an explicit $\varphi$ the absolute RSCounting-plus-gap statements cannot be stated numerically against the golden-ratio arithmetic that distinguishes $D = 3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.