jcost_phi_closed
plain-language theorem explainer
The recognition cost of the golden ratio equals φ − 3/2 exactly. Cosmology workers bounding the BIT dark-energy amplitude cite this closed form before comparing to 0.12. The proof unfolds J, inserts φ² = φ + 1, and finishes by field simplification plus nonlinear arithmetic.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ be the recognition cost and let $\varphi = (1+\sqrt{5})/2$. Then $J(\varphi) = \varphi - 3/2$.
background
In Recognition Science the cost of a positive ratio is $J(x) = (x + x^{-1})/2 - 1$, the unique nonnegative functional fixed by the Recognition Composition Law (T5). The golden ratio $\varphi$ is the self-similar fixed point forced at T6; it obeys $\varphi^2 = \varphi + 1$ and $\varphi > 0$.
This module forces the redshift kernel $K(z)$ in the dark-energy deviation $w(z) = -1 + \delta w_0 \cdot K(z)$ from rung factorization and single-rung balance $\rho = 1/(1+\rho)$, whose positive solution is $\varphi^{-1}$. The open interval for the today-amplitude is $\delta w_0 \in (0, J(\varphi)]$, so an exact value of $J(\varphi)$ is needed before any numerical ceiling can be stated.
Upstream facts used here are only the elementary constant lemmas $\varphi \neq 0$ and $\varphi^2 = \varphi + 1$.
proof idea
Unfold the definition $J(\varphi) = (\varphi + \varphi^{-1})/2 - 1$. Record $\varphi \neq 0$ and $\varphi^2 = \varphi + 1$. Clear the denominator with field_simp, then finish by nlinarith using positivity of $\varphi^2$ and the quadratic identity, which rewrites the expression as $\varphi - 3/2$.
why it matters
The sole downstream consumer is jcost_phi_lt_012, which rewrites via this identity and applies $\varphi < 1.62$ to obtain the Carnot ceiling $J(\varphi) < 0.12$. That bound pins the admissible today-amplitude band $\delta w_0 \in (0, J(\varphi)]$ appearing in the module's open questions and in the CPL thawing-line consequences ($w_0 \in (-1,-0.88)$, sum rule $w_0 + w_a = -1$).
Within the forcing chain the evaluation sits at the T5/T6 junction: the unique cost $J$ evaluated at the unique self-similar scale $\varphi$. It does not itself force the kernel shape, but it supplies the numerical head of the amplitude interval that every BIT cosmology claim must respect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.