phi_postAt_credit_self
plain-language theorem explainer
A single credit posting at account k lowers that account's ledger imbalance by exactly one. Gravity and ledger-dynamics arguments in the Gap 2 chain cite this when tracking how posting schedules move phi. The proof unfolds the credit case of postAt and closes by integer arithmetic on debit minus credit.
Claim. Let $L$ be a recognition ledger on the discrete carrier $\Lambda$ and let $k\in\Lambda$. After posting one credit quantum at $k$, the account imbalance satisfies $\varphi(\mathrm{post}_{k,\mathrm{credit}}(L),\,k)=\varphi(L,k)-1$, where $\varphi(L,k)=L.\mathrm{debit}(k)-L.\mathrm{credit}(k)$.
background
Gap 2 asks whether the measure behind the gravity gap is forced to be counts-only. Earlier arcs reduced that question to lattice charges and then to ledger dynamics: the posting rules that generate states, not the state type alone. This module answers that the dynamics excludes nothing among nonnegative column configurations.
A Recognition.Ledger on a recognition structure is a pair of integer maps debit and credit on the carrier units. Here the carrier is discreteCarrier Λ: units are Λ with the total relation, so every pair is related and no posting graph is baked into the structure. The imbalance at an account is the integer phi L k := debit k - credit k.
One dynamics step is postAt L k s: increment either the debit or the credit column of account k by one quantum, leaving every other entry fixed. That is the lift of LedgerPostingAdjacency.post from finite index sets to an arbitrary decidable finite carrier. Credit postings therefore raise only the credit column at k.
proof idea
Unfold the credit branch of postAt: the new debit map equals the old one at every account (in particular at k), and the new credit at k is the old credit plus one via the positive branch of the pointwise if. Rewrite the goal as equality of integer differences (debit' k) - (credit' k) = (debit k) - (credit k) - 1, substitute the two unfoldings, and finish with omega. No external lemmas beyond definitional reduction of postAt and phi are required.
why it matters
In the Gap 2 fifth arc the committed answer is that posting dynamics do not force the counts-only premise: every nonnegative ledger is reachable from the zero ledger, so every integer imbalance configuration arises as phi of a reachable state. Tracking how a single posting moves phi is the elementary step behind those reachability and schedule arguments (imbalance_realized, schedule countermodels).
This theorem is the credit half of the local update law; its sibling phi_postAt_debit_self is the debit half. Together they say a debit post raises imbalance by one and a credit post lowers it by one at the touched account and nowhere else (cf. phi_postAt_ne). That is the exact bookkeeping used when exhibiting schedules whose imbalance after one tick is not kind-constant, and when arguing that magnitude is untouched because posting never sees a magnitude field.
No downstream consumers are recorded yet; the lemma sits as local infrastructure inside the dynamics-kind-rule module rather than as a named paper proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.