flatLedger_totalCost_zero
plain-language theorem explainer
On any finite substrate lattice, the identically zero (flat) recognition ledger has vanishing total cost. Gravity and continuum-limit arguments cite this as the Minkowski baseline: zero curvature cost before hinges or horizons are introduced. The proof is a one-line application of the zero-cost characterization of flatness to the already-proved flatness of the constant-zero ledger.
Claim. For every finite lattice $\Lambda$, if $\mathcal{L}_0$ is the flat recognition ledger on $\Lambda$ (the map with $\mathcal{L}_0(i,j)=0$ for all cells $i,j$), then the total ledger cost satisfies $\sum_{i,j}\mathcal{L}_0(i,j)=0$.
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. Module conventions require symmetry, vanishing diagonal, non-negativity, and RCL subadditivity via the forced gate $R(u,v)=2uv+2u+2v$.
Derived scalars include the total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$ and the cell deficit $\Delta_i=\sum_j\mathcal{L}(i,j)$. Flatness means $\mathcal{L}\equiv 0$; the constant-zero map is the flat ledger on any $\Lambda$. Upstream cost notions (J-cost on ratios, event costs, ledger double-entry totals) all specialize here to pairwise non-negative entries whose sum is the total cost.
The continuum story uses this structure three ways: hinge-restricted total cost limits to the Regge action, bipartition boundary costs feed Page-curve entropy, and the vacuum energy is the ground-state total cost on the full lattice.
proof idea
Term-mode one-liner. Apply the reverse implication of the sibling characterization that total cost vanishes if and only if the ledger is flat, feeding the already-established fact that the constant-zero ledger is flat. No expansion of the double sum is needed: flatness supplies every entry zero, and the iff closes the equality to zero.
why it matters
This is the Minkowski baseline inside the recognition-ledger package: zero total cost exactly when there is no pairwise recognition defect. It is wired into recognitionLedgerCert as the flat_total_zero field and into the packaged one-statement theorem, which asserts existence of a flat ledger on every finite lattice together with non-negativity of total cost and the zero-iff-flat equivalence.
In the gravity reading, vanishing total cost is the discrete stand-in for flat spacetime before codimension-2 hinge deficits generate Regge curvature. That matches the module claim that continuum restriction of total ledger cost to hinges recovers the Regge action, and that vacuum energy is the ground-state total cost. Within the broader RS chain, the pairwise costs are instances of the unique J-cost (T5) composed under the Recognition Composition Law; this lemma does not re-derive J, it only pins the zero section of the ledger calculus used downstream for action, Page curve, and vacuum bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.