totalCost
plain-language theorem explainer
The total ledger cost of a recognition ledger is the double sum of all pairwise cell-comparison costs. Gravity and vacuum-energy arguments treat this scalar as the discrete action whose continuum restriction to codimension-2 hinges is the Regge action, and whose ground-state value is vacuum energy. The body is the plain Finset double sum of the ledger cost map; no further algebra is involved.
Claim. Let $\Lambda$ be a finite substrate lattice and let $\mathcal{L}$ be a recognition ledger on $\Lambda$ (symmetric, diagonal-zero, nonnegative pairwise costs obeying RCL subadditivity). The total ledger cost is $\sum_{i\in\Lambda}\sum_{j\in\Lambda}\mathcal{L}(i,j)\in\mathbb{R}$.
background
The module builds the recognition ledger as the central bookkeeping object of recognition gravity. On a finite substrate lattice $\Lambda$ (a Fintype), a ledger is a map $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ giving the accumulated recognition cost of comparing cells $i$ and $j$. The structure packages four axioms: symmetry $\mathcal{L}(i,j)=\mathcal{L}(j,i)$, diagonal zero $\mathcal{L}(i,i)=0$, nonnegativity, and RCL subadditivity $\mathcal{L}(i,k)\le R(\mathcal{L}(i,j),\mathcal{L}(j,k))$ with gate $R(u,v)=2uv+2u+2v$.
Pairwise costs are instances of the J-cost that appears throughout the foundation stack (observer events, multiplicative recognizers, PRC ratios). The module lists three uses of the ledger: gravitational action (continuum limit of total cost on codimension-2 hinges equals the Regge action), Page-curve entropy from reduced states across a horizon cut, and vacuum energy as the ground-state total cost on the full lattice.
Derived scalars named in the module doc are the total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$, the deficit $\Delta_i=\sum_j\mathcal{L}(i,j)$ at a cell, and flatness ($\mathcal{L}\equiv 0$).
proof idea
Pure definition: evaluate the double Finset sum $\sum_i\sum_j L.\mathrm{cost},i,j$ over the finite type $\Lambda$. No lemmas, rewrites, or positivity arguments appear in the body; those live in the sibling theorems on nonnegativity and flatness.
why it matters
This is the scalar the module doc calls out as the discrete gravitational action and the vacuum-energy observable. Continuum restriction of the total cost to codimension-2 hinges is claimed to recover the Regge action; the vacuum ledger cost is the ground-state value of the same sum on the full substrate. Sibling theorems totalCost_nonneg and totalCost_eq_zero_iff_flat turn the definition into the first analytic controls (nonnegativity; vanishing iff the ledger is flat). In the broader RS chain the pairwise entries are J-costs forced by T5 and the RCL gate, so the total cost is the global tally of recognition mismatch on the lattice. No downstream used_by edges are recorded yet; the definition is the entry point for those gravity and vacuum arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.