totalCost
plain-language theorem explainer
Total recognition cost of a level field on a coupling graph is the sum, over every edge, of the J-cost of the forced golden-ratio power of the endpoint level difference. Cosmology and RS auditors cite it when identifying the recognition ground state with consensus. It is a plain definition: Finset-sum of J(φ^{x_i−x_j}) over the edge set.
Claim. For a level field $x:\{0,\ldots,n-1\}\to\mathbb{R}$ and a finite edge set $E\subset\{0,\ldots,n-1\}^2$, the total recognition cost is $\sum_{(i,j)\in E} J\bigl(\varphi^{x_i-x_j}\bigr)$, where $J(r)=(r+r^{-1})/2-1$ and $\varphi$ is the golden ratio.
background
Recognition Science measures the cost of a positive ratio $r$ by the unique J-functional $J(r)=(r+r^{-1})/2-1$ (T5; equivalently $\cosh(\log r)-1$). On a discrete coupling graph the forced ratio between two recognition levels is $\varphi^{x_i-x_j}$, with $\varphi$ the self-similar fixed point forced at T6.
This module discharges the Phase-7 forward dynamics: a field of levels on a finite vertex set evolves by resolving one coupled pair per tick to its mean (the $\sigma=0$, J-minimal move). The module states explicitly that total edge demand is not claimed monotone; level variance is the Lyapunov function, with exact decrement $(x_i-x_j)^2/2$ per resolution.
Upstream, the same $J$ appears as the RS recognition cost of a positive ratio in the refine-trigger layer, and $\varphi$ comes from the shared constants bundle. Typical edge sets include the ordered 4-neighbour pairs of a diamond lattice component.
proof idea
Definition only: the body is the Finset sum, over the supplied edge set, of $J$ applied to $\varphi$ raised to the real level difference of the two endpoints. No lemmas are invoked; noncomputable real arithmetic of the sum is all that is required.
why it matters
This is the objective whose nonnegativity and vanishing law the module proves next: total cost is nonnegative and equals zero if and only if the field is constant on every edge (consensus). Those facts identify the recognition ground state with the configuration the variance descent converges to, matching the Python forward-dynamics checks with zero sorry and no new axioms.
Framework landmarks: J from T5 and the Recognition Composition Law, $\varphi$ from T6, and the Phase-7 cosmogenesis setting (closed-system descent plus the open conjugate-birth extension that conserves charge sum). The graph snapshot lists no further used-by edges, but the module doc names the immediate consumers as the nonnegativity and zero-iff theorems for this cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.