Jcost_phi_closed_form
plain-language theorem explainer
The recognition cost of the golden ratio equals φ − 3/2. Anyone converting J(φ) into a numerical bound, or comparing it to a saturation threshold, cites this identity. The proof unfolds the cost definition, inserts the golden-ratio relation φ² = φ + 1, and closes by field simplification plus nonlinear arithmetic.
Claim. With $J(x) = \frac{x + x^{-1}}{2} - 1$ and $\varphi$ the unique positive self-similar scale, one has $J(\varphi) = \varphi - \tfrac{3}{2}$.
background
The J-cost is the unique admissible recognition cost forced by the Recognition Composition Law: $J(x) = \frac{x+x^{-1}}{2}-1$ for $x>0$. It vanishes only at ratio one and is strictly positive on genuine distinctions. The golden ratio $\varphi$ is the unique positive fixed point of the self-similar reciprocal shift (T6), satisfying $\varphi^2 = \varphi+1$ and $\varphi\neq 0$.
This module (T9) forces the measure on recognition states once the T0–T8 shape chain is in place. The lattice layer derives weights $w(n)=\varphi^{-n}$ from factorization and per-step self-similar balance; the continuum layer recovers the Gibbs rule with rate pinned by $\ln\varphi$. Evaluating $J$ at $\varphi$ itself is a concrete arithmetic checkpoint used when comparing cost scales to numerical cutoffs.
Upstream, phi_ne_zero and phi_squared supply the two algebraic facts needed to clear denominators and reduce powers of $\varphi$.
proof idea
Term-mode proof. Unfold $J$ to $\frac{\varphi+\varphi^{-1}}{2}-1$. Record $\varphi\neq 0$ and the quadratic $\varphi^2=\varphi+1$. field_simp clears the inverse; nlinarith finishes with the positivity of $\varphi^2$ and the quadratic identity, yielding $\varphi-3/2$.
why it matters
Feeds the immediate numerical bound $J(\varphi)>0.11$, which sits on the path from closed form to saturation and rung-occupancy estimates inside MeasureForcing. In the T9 story the geometric $\varphi$-measure is forced by the same self-similarity that pins $\varphi$; knowing $J(\varphi)$ exactly lets cost thresholds be rewritten as pure $\varphi$-arithmetic rather than floating-point comparisons. Ties directly to T5 (J-uniqueness) and T6 ($\varphi$ as the unique scale). No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.