phi_postAt_ne
plain-language theorem explainer
Posting one quantum of debit or credit at account k leaves the imbalance phi unchanged at every other account i. Gravity Gap-2 arguments cite this when tracking how a posting schedule moves only the targeted letter. The proof is a two-case term on Side: both columns at i are definitionally the original values once i ≠ k.
Claim. Let $L$ be a recognition ledger on the discrete carrier $\Lambda$. For distinct accounts $i \neq k$ and either posting side $s \in \{\mathrm{debit},\mathrm{credit}\}$, the imbalance satisfies $\varphi(\mathrm{post}_s(L,k))(i) = \varphi(L)(i)$.
background
Gap 2 asks whether the ledger posting dynamics force the counts-only premise used upstream in the kind-rule chain. A recognition ledger on the discrete carrier discreteCarrier Λ is a pair of nonnegative integer columns (debit, credit) indexed by accounts in Λ; the imbalance map φ is the pointwise difference debit − credit.
The atomic dynamics step postAt L k s increments exactly one column at account k by one quantum and leaves every other entry fixed. Side is the two-valued choice debit versus credit. Because posts only raise a single column, reachability from the zero ledger covers every nonnegative ledger, and every integer imbalance configuration arises as φ of some reachable state.
This lemma isolates the locality of that step: away from the posted account, φ is invariant. That locality is what lets a one-tick schedule on a two-letter witness change φ at one edge letter while leaving the other letter’s φ at zero.
proof idea
Case-split on the posting side s.
Debit case: the debit column of postAt L k debit equals L.debit off k by if_neg h, and the credit column is definitionally L.credit. Rewrite φ as debit − credit at i to obtain equality with φ L i.
Credit case: symmetric. Debit is unchanged by definition; credit equals L.credit off k again by if_neg h. The same rewrite closes the goal.
No external lemmas beyond the definition of postAt and the if-neg branch are required.
why it matters
Parent use is schedule_countermodel_not_countsOnly: after one tick of the countermodel schedule, the run equals postAt zeroLedger cmEdge0 debit, so φ is 1 on edge letter 0 and (by this lemma) still 0 on the other same-kind letter. That pair is not kind-constant, so no counts-only law about schedules follows from the dynamics.
In the Gap-2 forcing chain this is the sharp negative answer at the dynamics layer: posts exclude nothing among nonnegative ledgers, and locality of φ lets the incidence/index countermodels appear as concrete one-tick runs. Magnitude is untouched separately (ledgers have no mag field); the imbalance conjunct falls here. The result sits under the gravity seven-gaps program rather than the T0–T8 foundation chain, but it closes the dynamics half of why ChargesCountsOnly is not forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.