totalCost_nonneg
plain-language theorem explainer
The total recognition cost of a level field on any finite coupling graph is nonnegative. Anyone citing recognition equilibrium, the recognition ledger, or the SM-Lagrangian skeleton uses this as the ground-state lower bound. The proof is a one-line sum-of-nonnegatives argument: each edge contributes a J-cost of a positive phi-power ratio.
Claim. For any $n$, any level field $x:\{0,\ldots,n-1\}\to\mathbb{R}$, and any finite edge set $E\subseteq\{0,\ldots,n-1\}^2$, the total recognition cost satisfies $0\le\sum_{(i,j)\in E} J(\varphi^{x_i-x_j})$, where $J$ is the recognition cost and $\varphi$ is the golden ratio.
background
The module formalizes Phase-7 forward dynamics: a field of recognition levels on a coupling graph evolves by forced pair resolutions that send both endpoints to their mean (the $\sigma=0$, $J$-minimal move). The recognition cost on a positive ratio is $J(r)=(r+r^{-1})/2-1$ (equivalently $\cosh(\log r)-1$), forced unique by the T5 step of the unified forcing chain and the Recognition Composition Law.
On an edge $(i,j)$ the forced ratio is $\varphi^{x_i-x_j}$ with $\varphi>1$ the self-similar fixed point (T6). The total cost is the sum of those edge costs. Upstream, jcost_nonneg already shows $0\le J(r)$ for every $r>0$, with equality only at $r=1$. The present result lifts that pointwise bound to the graph sum.
Local setting (module doc): closed-system descent is a strict Lyapunov drop in level variance until every coupled pair agrees; the zero of total cost is exactly that consensus configuration.
proof idea
One-line term proof. Apply Finset.sum_nonneg to the edge sum that defines total cost. Each summand is a $J$-cost of $\varphi$ raised to a real power; positivity of that base follows from Constants.phi_pos via Real.rpow_pos_of_pos, so the upstream lemma jcost_nonneg supplies $0\le J(\varphi^{\Delta x})$ on every edge. No case split and no graph structure beyond the sum is used.
why it matters
This is the cost half of the recognition ground-state package. Downstream, recognitionEquilibrium packages it as the cost_nonneg field of the equilibrium certificate for every level field and coupling graph, alongside sigma conservation and the exact variance drop. The companion zero-characterization (total cost vanishes iff the field is constant on every edge) then identifies the descent limit with graph consensus.
The same nonnegativity is re-used as a certificate atom in the recognition ledger one-statement (total cost nonnegative, zero iff flat/Minkowski) and in the SM-Lagrangian skeleton certificate (total_nonneg). In framework terms it is the graph-level shadow of T5 $J$-uniqueness: the unique nonnegative cost that vanishes only at ratio one, summed over couplings, forces the cosmogenesis ground state to be consensus rather than some other critical point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.