totalCost_nonneg
plain-language theorem explainer
On any finite substrate lattice the total recognition-ledger cost is nonnegative. Gravity and cosmology certificates cite this as the global positivity bound on the discrete action. The proof is a double Finset sum of the pointwise nonnegativity field of the ledger.
Claim. Let $\Lambda$ be a finite substrate lattice and let $\mathcal{L}$ be a recognition ledger on $\Lambda$ (a symmetric, diagonal-zero, nonnegative cost $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ obeying RCL subadditivity). Then the total ledger cost satisfies $0\le\sum_{i,j\in\Lambda}\mathcal{L}(i,j)$.
background
The recognition ledger is the discrete bookkeeping object of recognition gravity: on a finite lattice $\Lambda$ one assigns to each ordered pair of cells a recognition cost $\mathcal{L}(i,j)\ge 0$, required to be symmetric, zero on the diagonal, and RCL-subadditive via the forced gate $R(u,v)=2uv+2u+2v$. The module treats this structure as the common substrate for three continuum limits: Regge action on codimension-2 hinges, Page-curve radiation entropy across a horizon cut, and vacuum energy as the ground-state total cost.
The total cost is the double sum $\sum_{i,j}\mathcal{L}(i,j)$. Pointwise nonnegativity is part of the ledger structure itself (nonneg), so global positivity is the elementary sum of those bounds. Parallel total-cost nonnegativity statements appear in the cosmology recognition-equilibrium layer and in the SM-Lagrangian skeleton, each reducing to nonnegativity of a J-type cost on positive ratios.
proof idea
Unfold the definition of total cost (double Finset sum of cost). Apply Finset.sum_nonneg on the outer sum, then again on the inner sum; each summand is discharged by the ledger field L.nonneg i j. No algebraic identity beyond double summation of a nonnegative family is used.
why it matters
This is the positivity half of the recognition-ledger one-statement and of recognitionLedgerCert (total_nonneg). Downstream, the same bound feeds the cosmology recognition-equilibrium package (as cost_nonneg in the equilibrium structure) and the SM-Lagrangian skeleton certificate (total_nonneg). In the gravity reading it guarantees that the discrete action whose continuum limit is the Regge action cannot go negative, so the flat (Minkowski) ledger is a true ground state once paired with the companion zero-iff-flat theorem. It sits under the RCL gate and the J-cost nonnegativity forced earlier in the foundation chain, without needing the full T0–T8 forcing apparatus at this layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.