Jcost_phi_pos
plain-language theorem explainer
The golden-ratio recognition cost J(φ) is strictly positive. Cosmology ledgers and measure-forcing bounds cite this to guarantee every forced one-rung interface distinction carries a genuine paid cost, not a free bulk edge. The proof rewrites J in squared form and checks that both the nonzero squared numerator and the positive denominator are positive.
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 $J(\varphi) > 0$. Equivalently, $J(\varphi) = \frac{(\varphi-1)^2}{2\varphi} = \frac{\sqrt{5}-2}{2} > 0$.
background
The recognition cost $J(x) = (x + x^{-1})/2 - 1$ is the unique nonnegative solution of the Recognition Composition Law (T5 J-uniqueness). It vanishes only at $x = 1$ and is strictly positive for every other positive real. The golden ratio $\varphi$ is the self-similar fixed point forced at T6, so $\varphi \neq 1$ and $\varphi > 0$.
This module weights the polarized-birth edge ledger from LatticeBallEdges by that cost. Carried monochromatic edges span zero phi-rungs and cost $J(1) = 0$; interface bichromatic edges span exactly one rung (charges differ by $\pm 1$) and cost $J(\varphi^{\pm 1}) = J(\varphi)$ by reciprocal symmetry. The module doc states the north-star compute-watch law in cost units: total cost equals interface count times $J(\varphi)$, with bulk carried free.
Upstream facts used here are $\varphi \neq 0$, $\varphi \neq 1$, and the squared rewrite of $J$ that isolates $(\varphi-1)^2/(2\varphi)$.
proof idea
Rewrite $J(\varphi)$ via the squared identity Cost.Jcost_eq_sq (which needs $\varphi \neq 0$) into $(\varphi-1)^2/(2\varphi)$. Apply div_pos on that quotient. Numerator: $\varphi-1 \neq 0$ follows from $\varphi \neq 1$, so the square is strictly positive by the positivity tactic. Denominator: $2\varphi > 0$ from $\varphi > 0$ and a one-line linarith. That is the whole argument.
why it matters
Closes the positivity conjunct of the Phase 55 2D headline t55_cost_ledger: for a polarized diamond of radius $t \ge 1$, carried bulk costs zero, total cost equals $(8t-4)\cdot J(\varphi)$, and $J(\varphi) > 0$ is a genuine positive unit. The same fact feeds the Phase 56 graded-rung ledger t56_graded_cost_ledger, which generalizes the free-bulk / paid-interface split to any unit-step rung field.
In MeasureForcing it supplies the strict ceiling $\delta w_0(N) < J(\varphi)$ and the near-ceiling saturation $\delta w_0(N) > 0.95, J(\varphi)$ for $N \ge 8$. Framework-wise this is the cost-unit content of the compute-watch law after T5–T6: recognition activity is paid only on the codimension-1 interface, and that payment cannot vanish because $\varphi$ is forced away from $1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.