phiVec_coordAtomicStep_of_post
plain-language theorem explainer
A single debit or credit post at account index k changes the phi-vector by exactly +1 or -1 at coordinate k while leaving all other coordinates fixed. Ledger modelers connecting posting operations to parity adjacency would cite this to justify one-bit pattern updates. The proof constructs the existential witness for coordAtomicStep by case analysis on side and direct invocation of the phiVec_post lemmas.
Claim. Let $L$ be a ledger state with $d$ accounts. For any account index $k$ and side $s$ (debit or credit), the phi-vector of the state obtained by posting one unit at $k$ on side $s$ differs from the phi-vector of $L$ by a coordinate-atomic step: exactly one coordinate changes by $+1$ or $-1$, and all others remain unchanged.
background
LedgerState $d$ is the abbreviation for Recognition.Ledger over AccountRS $d$, whose universe is the finite set Fin $d$ of accounts. phiVec extracts the integer vector whose $i$-th entry is the difference debit minus credit at account $i$, using the Recognition.phi function. coordAtomicStep $x$ $y$ is the predicate asserting that $y$ is obtained from $x$ by altering exactly one coordinate by $+1$ or $-1$ while fixing the rest (defined in LedgerParityAdjacency).
proof idea
The term-mode proof constructs the pair witnessing coordAtomicStep. It cases on side: debit applies phiVec_post_debit to obtain the $+1$ change at $k$ and invariance elsewhere; credit applies phiVec_post_credit for the $-1$ change. The second conjunct of the witness is discharged by the same lemmas under the assumption $i ≠ k$.
why it matters
This lemma supplies the coordinate-level step required by the downstream theorem parity_oneBitDiff_of_post, which concludes that a single post produces a one-bit difference in the parity pattern. It completes the explicit ledger model described in the module documentation, bridging posting operations to the parity adjacency results that feed the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.