totalCost_eq_zero_iff
plain-language theorem explainer
The total recognition cost on a coupling graph vanishes exactly when every coupled pair of regions has equal level. Cosmologists and graph-dynamics readers cite it to identify the J-cost ground state with graph consensus. The proof rewrites the sum, uses nonnegativity of each edge cost, and reduces edgewise via the single-edge zero-cost criterion.
Claim. For any finite level field $x : \{0,\ldots,n-1\} \to \mathbb{R}$ and any finite set $E$ of ordered pairs, the total recognition cost $\sum_{(i,j)\in E} J(\varphi^{x_i-x_j})$ equals zero if and only if $x_i = x_j$ for every edge $(i,j)\in E$.
background
The module formalizes Phase-7 forward dynamics: a level field $x$ on $n$ regions evolves by forced pair resolutions that send coupled endpoints to their mean. The Lyapunov quantity is level variance; the ground-state cost is built from the recognition cost $J$.
Each edge $(i,j)$ carries the forced ratio $\varphi^{x_i-x_j}$ (with $\varphi$ the golden ratio). The single-edge cost is $J$ of that ratio. Upstream, jcost_nonneg gives $J\ge 0$ on positive arguments, and cost_phi_eq_zero_iff states that $J(\varphi^{a-b})=0$ exactly when $a=b$: "Two regions carry no forced distinction exactly when their levels are equal."
Total cost is the Finset sum of those edge costs. The module goal is that the zero-cost configuration the descent converges to is precisely consensus on the coupling graph.
proof idea
Unfold total cost to a Finset sum. Apply Finset.sum_eq_zero_iff_of_nonneg, justified because each summand is nonnegative by jcost_nonneg at $\varphi^{\Delta x}>0$ (using positivity of $\varphi$). The sum vanishes iff every summand vanishes. Bidirectionally, each edge term is zero iff the two endpoint levels agree, by cost_phi_eq_zero_iff. The two directions of the biconditional are just .mp and .mpr of that edge lemma.
why it matters
This is the ground-state half of the recognition-equilibrium package. Downstream, recognitionEquilibrium bundles sigma conservation, exact variance drop, nonincreasing spread, cost nonnegativity, and this zero-cost characterization into one structure: the forced dynamics descends strictly until consensus, and the $J$-cost minimum is exactly that consensus.
In the broader RS cosmology chain, pair resolution is the sigma-neutral, $J$-minimal move forced by the recognition composition law and $J$-uniqueness (T5); $\varphi$ is the self-similar fixed point (T6). Identifying zero total cost with graph consensus closes the claim that the forward dynamics' attractor is homogenization on coupled components, which FoamTopology then uses when arguing freeze-out simplification of Euler characteristic across the recognition front.
No sorry remains here; it is a proved building block for the Phase-7 convergence story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.