postAt_predOf
plain-language theorem explainer
Posting one quantum on side s at account k after the predecessor of ledger L recovers L, whenever the touched column of L is strictly positive. Mass-induction reachability proofs cite this as the inverse step that makes every nonzero nonnegative ledger the post of a legal predecessor. The argument is case analysis on debit versus credit, then pointwise ledger extensionality with local arithmetic at k.
Claim. Let $L$ be a recognition ledger on the discrete carrier $\Lambda$, let $k\in\Lambda$, and let $s$ be a posting side (debit or credit). If the corresponding column of $L$ at $k$ is strictly positive, then posting one quantum on side $s$ at $k$ after taking the predecessor of $L$ at $(k,s)$ recovers $L$: $\mathrm{post}(\mathrm{pred}(L,k,s),k,s)=L$.
background
Gap 2 asks whether posting dynamics forces the counts-only premise behind the gravity measure. Earlier arcs reduced kind-only cost to counts-only charge and then to lattice imbalance and magnitude; this module treats the dynamics that produce ledger states, not the state type alone.
A recognition ledger on discreteCarrier Λ is a pair of integer-valued debit and credit columns on the finite carrier Λ. One posting step (postAt) increments a single account's debit or credit by one quantum; the predecessor (predOf) decrements the same column when it is positive. Ledger equality is pointwise on both columns (ledger_ext).
The module's committed answer is that the dynamics excludes nothing among nonnegative ledgers: every such ledger is reachable from the balanced zero ledger by a finite posting run. The predecessor/post inverse pair is the local engine of that reachability argument.
proof idea
Case-split on the posting side. In each branch apply ledger extensionality, so it suffices to check debit and credit pointwise.
On the active column: at the touched account k, unfold the if-then definitions of post and pred to get (pred debit/credit at k) + 1 and L's column minus 1; omega closes the Nat arithmetic under the positivity hypothesis. Off k, both post and pred are identity, so the two if-neg rewrites give equality. On the inactive column the whole composition is definitionally L, so rfl finishes.
The credit case is symmetric (roles of the two columns swapped).
why it matters
This is the local inverse law that licenses mass induction in postReachable_zero_of_nonneg: every nonnegative ledger of positive mass is the post of its predecessor, so reachability from the zero ledger descends by mass. That parent theorem is the module's main result: the dynamics reaches every nonnegative state and therefore cannot force any restriction on imbalances.
In the Gap 2 chain this closes the dynamics arc against the counts-only premise. Because every nonnegative ledger (hence every integer imbalance configuration) is dynamically generable, the incidence-reading and index-reading countermodels from earlier arcs are not excluded by posting rules. Magnitude falls separately: posting never touches a magnitude field. The result is scaffolding for the sharper claim that counts-only is not a theorem about schedules (schedule_countermodel_not_countsOnly, imbalance_realized).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.