jcost_phi_lt_012
plain-language theorem explainer
The recognition cost of the golden ratio satisfies J(φ) < 0.12, so the Carnot ceiling on today's dark-energy amplitude is strictly below twelve percent. Cosmologists citing the forced w₀ band or the equilibrium band use this numerical gate. The proof rewrites J(φ) as φ − 3/2 and applies the certified bound φ < 1.62 with linear arithmetic.
Claim. The recognition cost of the golden ratio obeys $J(\varphi) < 0.12$, where $J(x) = (x + x^{-1})/2 - 1$ and $\varphi = (1+\sqrt{5})/2$. Equivalently, after the closed form $J(\varphi) = \varphi - 3/2$, one has $\varphi - 3/2 < 0.12$.
background
This module forces the BIT redshift kernel from rung factorization and single-rung balance at $\varphi^{-1}$. The dark-energy deviation is written $w(z) = -1 + \delta w_0 \cdot K(z)$; the admissible today-amplitude is capped by the recognition cost of $\varphi$, called the phantom-Carnot ceiling.
The cost functional is $J(x) = (x + x^{-1})/2 - 1$ (T5 J-uniqueness). For $\varphi$ the golden-ratio identity $\varphi^2 = \varphi + 1$ collapses $J(\varphi)$ to the linear form $\varphi - 3/2$ (lemma jcost_phi_closed). Constants supplies the tight decimal gate $\varphi < 1.62$ from $\sqrt{5} < 2.24$.
The local goal is a strict upper bound on that ceiling so the forced CPL thawing line lands in a concrete $w_0$ interval rather than an open half-line.
proof idea
Term-mode, three steps. Rewrite the goal via the private closed form $J(\varphi) = \varphi - 3/2$. Import the certified inequality $\varphi < 1.62$. Finish by linarith: $\varphi - 3/2 < 1.62 - 1.5 = 0.12$. No calculus or field simplification remains after the rewrite.
why it matters
Feeds w0_band directly: any positive amplitude up to the Carnot ceiling forces $w_0 \in (-1, -0.88)$. The same bound is cited inside equilibrium_w0_band in MeasureForcing, which tightens the dated equilibrium prediction to $(-0.896, -0.88)$ for occupancy $N \ge 8$.
In the Forced Redshift Kernel paper this is the numerical half of the phantom-Carnot ceiling. Together with the forced kernel $K(z) = 1/(1+z)$ on the $\varphi$-lattice and the thawing sum rule $w_0 + w_a = -1$, it turns the qualitative no-phantom statement into a sharp observational band. The open question it leaves untouched is the exact today-amplitude $\delta w_0 \in (0, J(\varphi)]$; only the upper edge is pinned here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.