eq_zeroLedger_of_mass_zero
plain-language theorem explainer
A recognition ledger whose mass vanishes is identically the zero ledger: every debit and credit column is zero. Downstream mass-induction for post-reachability cites this as the base case. The proof unpacks mass as a sum of nonnegative absolute column entries, forces each summand to zero, then applies ledger extensionality.
Claim. Let $L$ be a recognition ledger on the discrete carrier of $\Lambda$. If the mass of $L$ is zero, then $L$ equals the zero ledger (all debit and credit entries vanish).
background
Gap 2 asks whether posting dynamics forces the counts-only premise behind the kind-only cost. This module answers no: from the balanced zero ledger, every ledger with nonnegative columns is reachable by posting steps, so the dynamics excludes no nonnegative imbalance configuration.
A Recognition.Ledger on the discrete carrier stores integer debit and credit columns per site. Mass is the sum over sites of $\lvert\mathrm{debit}\rvert + \lvert\mathrm{credit}\rvert$. The zero ledger is the unique ledger with both columns identically zero. Ledger equality is decided by pointwise equality of the two columns (ledger_ext).
Posting increments one column by one quantum and never decreases mass, so mass zero is the natural base of the reachability induction.
proof idea
Unfold the hypothesis mass L = 0 into a finite sum of nonnegative natural numbers equaling zero. Apply Finset.sum_eq_zero_iff_of_nonneg (using Nat.zero_le) to conclude each summand vanishes: for every site $i$, $\lvert L.\mathrm{debit}, i\rvert + \lvert L.\mathrm{credit}, i\rvert = 0$. Integer absolute-value arithmetic (omega) yields debit i = 0 and credit i = 0 pointwise. Finish by ledger_ext, supplying the two pointwise identities.
why it matters
This is the mass-zero base case for postReachable_zero_of_nonneg, the module's main theorem: every nonnegative ledger is reachable from the zero ledger by a finite posting run. That reachability is what makes Gap 2's dynamics answer sharp: the dynamics excludes nothing among nonnegative states, so it cannot force counts-only on imbalance (and says nothing about magnitude, which lives outside the ledger columns).
Without uniqueness of the mass-zero ledger, the induction step that peels a predecessor off a positive-mass nonnegative ledger would lack a clean zero base. The result is pure double-entry bookkeeping, not a forcing-chain landmark (T0–T8), but it closes the dynamics arc that kills the dual premise left open by Gap2LatticeKindRule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.