boundaryCost_nonneg
plain-language theorem explainer
Boundary cost of a recognition ledger across any substrate bipartition is nonnegative. Gravity and holography arguments that treat the interior–exterior interface cost as an action or entropy term cite this. The proof unfolds the double sum and applies nonnegativity of each ledger entry.
Claim. Let $\Lambda$ be a finite substrate lattice and $\mathcal{L}$ a recognition ledger on $\Lambda$ (symmetric, diagonal-zero, nonnegative pairwise costs). For any bipartition of $\Lambda$ into complementary interior and exterior regions, the boundary cost $\sum_{i\in\mathrm{int}}\sum_{j\in\mathrm{ext}}\mathcal{L}(i,j)$ satisfies $0\le$ that sum.
background
The recognition ledger is the bookkeeping object of recognition gravity: on a finite substrate $\Lambda$, a map $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ records the accumulated recognition cost of comparing cells $i$ and $j$. By structure it is symmetric, vanishes on the diagonal, is pointwise nonnegative, and obeys RCL subadditivity via the forced gate $R(u,v)=2uv+2u+2v$.
A substrate bipartition splits $\Lambda$ into complementary interior and exterior Finsets (disjoint, union the universe). In the gravitational reading this cut is a horizon. The boundary cost is the sum of ledger entries with one leg in the interior and one in the exterior: the discrete analogue of a boundary term in the action, and the ledger input to Page-curve style reduced-state entropy.
Nonnegativity of pairwise costs is part of the ledger structure (and ultimately traces to the J-cost $J(x)=(x+x^{-1})/2-1\ge 0$ on positive ratios). Total ledger cost nonnegativity is the global sibling of the same idea; here the sum is restricted to the cut.
proof idea
Term-mode proof by unfolding. Expand boundaryCost as a double Finset sum over interior then exterior. Apply Finset.sum_nonneg to the outer sum, then again to the inner sum. Each summand is $\mathcal{L}(i,j)$, which is $\ge 0$ by the ledger's nonneg field. No algebraic identities beyond sum-of-nonnegatives are used.
why it matters
In the Recognition Ledger module the continuum limit of total ledger cost on codimension-2 hinges is identified with the Regge action, radiation entropy with a reduced state across a horizon cut, and vacuum energy with the ground-state total cost. Boundary cost is the cut-restricted sum that feeds those readings: a nonnegative interface cost is the minimal sanity check before treating it as an action or entropy contribution.
The module is marked structural (0 sorry, 0 RS-internal axiom). This lemma sits beside totalCost_nonneg and the flatness characterization totalCost_eq_zero_iff_flat, and next to the announced symmetry of boundary cost under interior/exterior swap. No downstream dependents are recorded yet; it is infrastructure for horizon and Page-curve arguments rather than a forcing-chain (T0–T8) step. It does not itself derive Einstein equations or the alpha band; it only locks the sign of the cut cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.