phi_postAt_debit_self
plain-language theorem explainer
Posting one debit quantum at account k raises the ledger imbalance φ at k by exactly one. Gap-2 gravity arguments cite this when tracking how posting schedules move pointwise imbalance. The proof is a direct integer calculation: the debit column at k increments by one, credit is copied, and φ is debit minus credit.
Claim. For any recognition ledger $L$ on a discrete finite carrier $\Lambda$ and any account $k\in\Lambda$, if $L'$ is obtained from $L$ by posting one debit quantum at $k$, then $\varphi(L',k)=\varphi(L,k)+1$, where $\varphi$ denotes the pointwise imbalance $\mathrm{debit}-\mathrm{credit}$.
background
A recognition ledger on a structure $M$ is a pair of integer-valued maps $\mathrm{debit},\mathrm{credit}:M.U\to\mathbb{Z}$. On the discrete carrier with units $\Lambda$ (total relation, no posting graph), the imbalance $\varphi(L,k)$ is simply $L.\mathrm{debit},k-L.\mathrm{credit},k$.
This module is the dynamics arc of Gravity Gap 2. Upstream arcs reduced the measure's size-blindness to a counts-only premise on charges; the question here is whether the posting rules that generate ledgers force that premise. A single posting step increments exactly one account's debit or credit column by one quantum. From the balanced zero ledger every nonnegative ledger is reachable, so every integer imbalance arises as $\varphi$ of some reachable state.
The present identity records the elementary effect of a debit post on $\varphi$ itself, the quantity whose kind-constancy is at stake in the counts-only claim.
proof idea
Unfold the debit-side posting step: at account $k$ the new debit equals the old debit plus one (the equality branch of the pointwise update), while the credit map is identical to the original. Rewrite the goal as an equality of integer differences
$(\mathrm{debit}',k)-(\mathrm{credit}',k)=(\mathrm{debit},k)-(\mathrm{credit},k)+1$,
substitute the two column identities, and finish with integer arithmetic (omega). No external lemmas beyond the definition of the posting step are required.
why it matters
The sole downstream consumer is schedule_countermodel_not_countsOnly, the module's main negative theorem: after one tick of an explicit posting schedule on the two-bridge witness, imbalance is $1$ on one edge letter and $0$ on another letter of the same kind, so no counts-only law about schedules is derivable from the dynamics. This debit-self identity is the arithmetic step that identifies the run's imbalance with a single debit post at the countermodel edge.
In the Gap-2 chain (weight size-blind if cost kind-only; cost kind-only if charge counts-only; charge counts-only if lattice imbalance and magnitude are), the dynamics layer gives the sharpest answer: posting excludes nothing among nonnegative ledgers and realizes non-counts-only imbalances. Magnitude is untouched because bare ledgers carry no magnitude field; enrichment attaches magnitude separately. The result is local bookkeeping that makes the schedule countermodel fully explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.