postAt
plain-language theorem explainer
One posting step on a recognition ledger over a discrete finite carrier: given ledger L, account k, and side (debit or credit), return the ledger with that column incremented by one quantum at k and every other entry left alone. Gap-2 dynamics, reachability, and schedule arguments all cite it as the atomic step. The body is a two-branch match with a pointwise update on the chosen column.
Claim. Fix a finite discrete carrier $\Lambda$ and a recognition ledger $L$ on that carrier (nonnegative integer debit and credit columns). For an account $k\in\Lambda$ and a side $s\in\{\mathrm{debit},\mathrm{credit}\}$, the one-step post of $L$ at $(k,s)$ is the ledger that adds $1$ to the $s$-column of account $k$ and leaves every other debit and credit entry unchanged.
background
Gap 2 asks whether the measure on lattice imbalance is forced to be counts-only. Earlier arcs reduced that question through kind-only cost and counts-only charge down to lattice imbalance and magnitude. This module treats the remaining layer: the posting dynamics that generate ledger states, not the state type alone.
A recognition ledger on a discrete carrier is a pair of maps (debit, credit) from accounts to integers. The imbalance (phi) at an account is debit minus credit. A posting side is debit or credit. The atomic dynamics is one quantum post: raise exactly one column of exactly one account by one. The present definition is that step, lifted from the Fin-indexed adjacency post to an arbitrary decidable finite carrier.
Module context: posts only ever raise columns, so from the balanced zero ledger every nonnegative ledger is reachable, every integer imbalance configuration arises as phi of some reachable ledger, and magnitude is untouched because the ledger type has no magnitude field.
proof idea
Definition by cases on the posting side. On debit, rebuild the ledger with debit updated by a pointwise if-then-else that adds one at account k and is identity elsewhere, credit copied unchanged. On credit, the symmetric update: debit copied, credit incremented only at k. No lemmas; pure structural match and function update.
why it matters
This is the generator of the entire Gap-2 dynamics. The inductive reachability relation is the reflexive-transitive closure of single posts; schedule execution applies it at each non-idle tick. Downstream lemmas record how imbalance transforms: debit post raises phi at k by one, credit post lowers it by one, and posts at k leave phi at every other account fixed. Inversion (post after predecessor recovers L when the column is positive) also routes through this step.
Framework role: the module's committed answer is that dynamics forces nothing counts-only. Because every nonnegative ledger is post-reachable from zero, every imbalance, including the incidence and index countermodels from earlier arcs, is dynamically generable. The schedule-level countermodel and the silence of posting about magnitude both depend on this atomic step. It is the dynamics half of the Gap-2 forcing chain, not a gravity force law itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.