jcost_eq_zero_iff
plain-language theorem explainer
The recognition cost of a positive ratio vanishes exactly when that ratio equals one. Cosmology equilibrium arguments and the foundation J-geometry layer cite this as the unique ground-state characterization. The proof is a short biconditional split: off one, strict positivity of the cost contradicts zero; at one, direct evaluation yields zero.
Claim. For every real $x > 0$, the recognition cost $J(x) = \frac{x + x^{-1}}{2} - 1$ satisfies $J(x) = 0$ if and only if $x = 1$.
background
In Recognition Science the cost of a positive ratio is $J(x) = (x + x^{-1})/2 - 1$, the unique functional forced by the Recognition Composition Law (forcing-chain T5). It measures genuine distinction: equal ratios cost nothing, and any other positive ratio costs strictly more.
This module discharges the central convergence facts of the Phase-7 forward dynamics. A field of recognition levels on a coupling graph evolves by resolving one coupled pair per tick to their mean (the sigma-conserving, J-minimal move). Variance is a strict Lyapunov function with exact decrement $(x_i - x_j)^2/2$, so the dynamics descends until every coupled pair is equal.
Upstream, the strict-positivity lemma already shows that any positive ratio other than one has $J > 0$, via the algebraic rewrite $J(x) = (x-1)^2/(2x)$. The present result closes the zero set of that cost.
proof idea
Biconditional by constructor. Forward direction: assume $J(x) = 0$ and $x \neq 1$. The upstream positivity lemma (genuine distinction has strictly positive cost) supplies $0 < J(x)$; rewrite the hypothesis into that inequality to obtain $0 < 0$, contradicting irreflexivity of $<$. Reverse direction: substitute $x = 1$ and evaluate $J(1)$ by direct arithmetic (norm_num on the unfolded definition).
why it matters
Pins the unique J-ground state at ratio one, the T5 fixed point of the recognition cost. Downstream it is applied to the forced phi-ladder ratio: $J(\phi^{a-b}) = 0$ iff the two region levels agree. That step is the bridge from single-edge cost to total recognition cost over the coupling graph, which vanishes exactly at consensus. The module therefore identifies the descent target of the forward dynamics with the recognition equilibrium. The same zero-set fact is restated in the foundation J-cost geometry layer (F1.1.3) and specialized to ordinary ratios $v/n$ (F1.2.1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.