deficit
plain-language theorem explainer
The ledger deficit at a substrate cell is the sum of pairwise recognition costs from that cell to every cell on the lattice. Gravity, continuum-bridge, and constant-derivation arguments cite it as the discrete curvature density sitting at a vertex. The body is a plain finite sum of the ledger cost function; no proof content.
Claim. For a recognition ledger $\mathcal{L}$ on a finite lattice $\Lambda$ and a cell $i\in\Lambda$, the deficit is $\Delta_i = \sum_{j\in\Lambda} \mathcal{L}(i,j)$.
background
The recognition ledger is the bookkeeping object of recognition gravity: on a finite substrate lattice $\Lambda$, a ledger $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ records the accumulated recognition cost of comparing each pair of cells. It is required to be symmetric, vanish on the diagonal, stay non-negative, and obey RCL subadditivity via the forced gate $R(u,v)=2uv+2u+2v$.
Among the derived quantities listed in the module, the cell deficit is $\Delta_i=\sum_j\mathcal{L}(i,j)$, alongside the total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$ and the flatness predicate ($\mathcal{L}\equiv 0$). The continuum story is that the total cost restricted to codimension-2 hinges limits to the Regge action; the cell deficit is the local sum that feeds that accounting.
Upstream geometry modules use the same word for angular deficit $2\pi-\sum\theta$ at a hinge (DihedralAngle, Schlaefli). Those are parallel discrete-curvature notions, not the same definition: here the sum is over ledger costs, not dihedral angles.
proof idea
Definition only. Expand as the finite sum $\sum_j L.\mathrm{cost},i,j$ over the Fintype of cells. No lemmas, no tactics.
why it matters
This is the local density that turns the ledger into a curvature bookkeeping device. Downstream, ContinuumBridge uses it for flat-zero-cost and stationarity-iff-Laplacian-zero statements; FreudenthalTriangulationCert ties hinge counts to zero-deficit claims; AlphaDerivation and LambdaRecDerivation reuse the deficit language for angular deficit at cube vertices ($2\pi-3(\pi/2)$) when extracting geometric seeds and $\lambda_{\mathrm{rec}}$.
In the module's three-use taxonomy it supports (1) gravitational action via hinge-restricted total cost, (2) page-curve entropy bookkeeping across horizon cells, and (3) vacuum energy as ground-state total cost. It sits next to totalCost and the flatness lemmas (totalCost_eq_zero_iff_flat), so every non-negativity or vanishing argument about local curvature density routes through this sum. Framework link: discrete curvature concentrated at hinges, the same structural role T8's $D=3$ and the eight-tick lattice play when the continuum limit is taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.