totalCost_eq_zero_iff_flat
plain-language theorem explainer
The total recognition cost of a ledger vanishes exactly when every pairwise cell cost is zero (the ledger is flat). Gravity and continuum-limit arguments cite this as the discrete Minkowski condition on the substrate. The proof is a two-direction Finset argument: nonnegativity plus sum-to-zero forces each summand to zero, and flatness makes the double sum vanish.
Claim. For a recognition ledger $\mathcal{L}$ on a finite substrate lattice $\Lambda$, the total cost $\sum_{i,j}\mathcal{L}(i,j)$ equals zero if and only if $\mathcal{L}(i,j)=0$ for every pair of cells $i,j$ (the ledger is flat).
background
The recognition ledger is the discrete bookkeeping object of recognition gravity: on a finite substrate lattice $\Lambda$, a cost function $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ records the accumulated recognition cost of comparing each pair of cells. By definition it is symmetric, vanishes on the diagonal, is pointwise nonnegative, and obeys RCL subadditivity via the forced gate $R(u,v)=2uv+2u+2v$.
Two derived notions matter here. The total ledger cost is the double sum $\sum_{i,j}\mathcal{L}(i,j)$. Flatness means $\mathcal{L}(i,j)=0$ for all $i,j$: every comparison is costless, the discrete stand-in for Minkowski vacuum. Module status is structural (no sorry, no RS-internal axiom).
Upstream cost notions (observer J-cost, multiplicative-recognizer cost, PRC quotient cost, rung-coarsen weighted sums) all feed the same nonnegativity that makes a vanishing sum force vanishing summands. The ledger packages that nonnegativity as a structure field used directly in the argument.
proof idea
Bidirectional constructor.
Forward ($\mathrm{totalCost}=0\Rightarrow$ flat): unfold flatness and total cost. Nonnegativity of each inner sum lets Finset.sum_eq_zero_iff_of_nonneg push the outer vanishing sum down to every row sum being zero. A second application of the same lemma on the $i$-th row, again using pointwise nonnegativity of $\mathcal{L}(i,\cdot)$, yields $\mathcal{L}(i,j)=0$ for arbitrary $j$.
Reverse (flat $\Rightarrow$ total cost zero): unfold total cost and apply Finset.sum_eq_zero twice; each summand is zero by the flatness hypothesis.
why it matters
This is the discrete vacuum criterion for recognition gravity: total cost zero characterizes the flat (Minkowski) ledger. It is the iff half of the module's one-statement theorem, which asserts that total cost is nonnegative and vanishes exactly on flat lattices, and that a flat ledger exists on every finite $\Lambda$.
Downstream it discharges flatLedger_totalCost_zero (one-line mpr from flatness of the zero ledger), fills the zero_iff_flat field of recognitionLedgerCert, and appears in recognition_ledger_one_statement. In the broader gravity story the continuum limit of total ledger cost on codimension-2 hinges is the Regge action, and vacuum energy is the ground-state total cost; both need a clean zero-cost characterization of flat configurations.
No open scaffold: the claim is fully proved and closes the flatness half of the ledger certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.