Jcost_phi_gt_011
plain-language theorem explainer
The recognition cost of the golden ratio satisfies J(φ) > 0.11. Cosmologists pinning the T9 equilibrium w₀ band and the δw₀ floor cite this numerical lower bound. Proof is a one-line rewrite to the closed form J(φ) = φ − 3/2, then linear arithmetic from φ > 1.61.
Claim. Let $J(x) = \frac{x + x^{-1}}{2} - 1$ be the recognition cost and $\varphi = \frac{1+\sqrt{5}}{2}$ the golden ratio. Then $0.11 < J(\varphi)$.
background
Module T9 forces the weighting on recognition states left open by the T0–T8 shape chain: any admissible weight is the geometric φ-measure (equivalently Gibbs with rate fixed by the self-similar ledger). The cost that enters that measure is the unique RS cost $J(x) = (x + x^{-1})/2 - 1$ forced at T5.
For the golden ratio itself, the identity $\varphi^2 = \varphi + 1$ collapses $J(\varphi)$ to the closed form $\varphi - 3/2$ (theorem Jcost_phi_closed_form). Constants also supply the tight numerical floor $\varphi > 1.61$. Combining the two yields a concrete lower bound on $J(\varphi)$, which is the input needed when converting saturation fractions into dark-energy deviations $\delta w_0$.
proof idea
Term-mode one-liner. Rewrite the goal by the closed-form identity $J(\varphi) = \varphi - 3/2$. The resulting inequality $0.11 < \varphi - 3/2$ is immediate from the lemma $\varphi > 1.61$ via linarith.
why it matters
Direct input to two parent results in the same module: deltaW0_gt_004 (for any occupancy depth $N$, $\delta w_0(N) > 0.04$, so equilibrium excludes exact ΛCDM) and equilibrium_w0_band (for $N \ge 8$, the equilibrium prediction is $w_0 \in (-0.896,-0.88)$). Both sit inside T9 measure forcing, the step that supplies the missing weighting primitive after T5 J-uniqueness and T6 φ-forcing. The lower bound keeps equilibrium $w_0$ strictly above $-1$ by a falsifiable margin; a confirmed $|w_0+1| < 0.04$ would defeat the equilibrium reading of occupancy, not T9 itself. The H-theorem that would discharge the equilibrium hypothesis remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.