predOf
plain-language theorem explainer
Predecessor operator on a discrete dual-entry ledger: given account k and side (debit or credit), decrement that column at k by one quantum. Downstream mass-induction and reachability proofs cite it as the legal reverse of a unit post. The body is a two-branch match that rebuilds the ledger record with a pointwise subtraction on the chosen column.
Claim. For a ledger $L$ on the discrete carrier $\Lambda$, an account $k\in\Lambda$, and a posting side $s\in\{\mathrm{debit},\mathrm{credit}\}$, the predecessor $\mathrm{pred}(L,k,s)$ is the ledger that agrees with $L$ everywhere except that the chosen column at $k$ is reduced by $1$.
background
Gap 2 asks whether posting dynamics force the counts-only premise on lattice charges. Earlier arcs reduced kind-only cost to counts-only charge and then to lattice imbalance/magnitude; this module treats the dynamics themselves: unit posts that raise one debit or credit column by one quantum.
A Recognition.Ledger on discreteCarrier Λ is a pair of integer-valued debit and credit maps on the finite carrier $\Lambda$ (the recognition relation is total and unused here). LedgerPostingAdjacency.Side is the two-valued choice debit/credit. The forward step postAt increments the chosen column at $k$; the predecessor defined here is its formal inverse on nonnegative ledgers with a positive entry at that cell.
The module's committed answer is that dynamics exclude nothing among nonnegative states: every such ledger is reachable from the balanced zero ledger, so no imbalance restriction is forced.
proof idea
Pure definition by case analysis on the side. On debit, rebuild the ledger with the same credit map and with debit equal to $L.\mathrm{debit}$ except at $k$, where the value is decreased by one. On credit, symmetrically decrement only the credit column at $k$. No lemmas are applied; the match is the entire construction.
why it matters
This is the reverse step that makes mass induction on posting runs work. postAt_predOf shows that posting the predecessor at $(k,s)$ recovers $L$ whenever the chosen entry is strictly positive. predOf_nonneg preserves columnwise nonnegativity under that hypothesis, and mass_predOf_lt shows mass strictly drops, so induction on mass is well-founded.
Those three facts feed postReachable_zero_of_nonneg: every nonnegative ledger is reachable from the zero ledger by a finite posting schedule. That reachability is the module's sharp negative answer for Gap 2: dynamics produce every nonnegative imbalance configuration (including the incidence and index countermodels from earlier arcs), so they cannot force counts-only. Magnitude is untouched because the ledger type has no magnitude field at all.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.