totalCost_eq_sum_deficits
plain-language theorem explainer
On any finite substrate, the total recognition-ledger cost equals the sum of the per-cell deficits. Gravity and vacuum-energy arguments that switch between global action and local bookkeeping cite this identity. The proof is pure definitional equality closed by rfl.
Claim. Let $\Lambda$ be a finite substrate lattice and $\mathcal{L}$ a recognition ledger on $\Lambda$. Then the total ledger cost equals the sum of local deficits: $\mathrm{TotalCost}(\mathcal{L}) = \sum_{i\in\Lambda}\Delta_i(\mathcal{L})$, where $\Delta_i(\mathcal{L})=\sum_j\mathcal{L}(i,j)$.
background
The recognition ledger is the central bookkeeping object of recognition gravity. On a finite substrate $\Lambda$, a ledger is a map $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ that is symmetric, vanishes on the diagonal, and obeys RCL subadditivity: $\mathcal{L}(i,k)\le R(\mathcal{L}(i,j),\mathcal{L}(j,k))$ with gate $R(u,v)=2uv+2u+2v$.
Two derived scalars organize the continuum and thermodynamic limits. Total ledger cost is $\sum_{i,j}\mathcal{L}(i,j)$. The deficit at cell $i$ is the row sum $\Delta_i=\sum_j\mathcal{L}(i,j)$. The module records three uses: continuum limit of hinge-restricted total cost recovers the Regge action; radiation entropy on a horizon partition is a reduced von Neumann entropy; vacuum energy is the ground-state total cost on the full lattice.
A ledger is flat precisely when every pairwise cost vanishes. Because deficits are non-negative row sums, the global-versus-local identity below is the natural bookkeeping step before non-negativity and flatness characterizations.
proof idea
Definitional one-liner. Total cost and the finite sum of per-cell deficits reduce to the same term, so the goal closes by rfl with no lemmas, rewrites, or arithmetic.
why it matters
This identity is the API bridge between global ledger energy and local cell deficits inside recognition gravity. It underwrites the three module-level applications stated in the module doc: Regge action as continuum limit of total cost on codimension-2 hinges, Page-curve entropy from horizon partitions, and vacuum energy as ground-state total cost.
Sibling results build on the same bookkeeping: non-negativity of total cost, and the equivalence of vanishing total cost with flatness. Those characterizations need the total cost to be exactly the sum of non-negative deficits. No downstream theorem currently lists this declaration as a dependency, so it presently serves as a structural convenience lemma in the ledger layer rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.