phiVec_post_credit
plain-language theorem explainer
The lemma shows that posting one credit unit to account k in a d-account ledger subtracts exactly one from the phi vector at coordinate k and leaves all other coordinates unchanged. Ledger modelers cite it when proving that atomic posts induce single-coordinate steps on the phi field. The proof splits on whether the query index matches k, substitutes in the equal case, and simplifies both branches using the definitions of post and phiVec together with ring normalization.
Claim. Let $L$ be a ledger state over $d$ accounts. For indices $k,i$, the phi vector after a credit post at account $k$ satisfies $phi'(i) = phi(i) - 1$ if $i=k$ and $phi'(i) = phi(i)$ otherwise.
background
LedgerState d is the abbreviation Recognition.Ledger (AccountRS d), where AccountRS equips the finite set Fin d with the trivial recognition relation. phiVec L is defined as Recognition.phi L, the integer vector whose i-th entry equals debit(i) minus credit(i) for the current ledger. The post operation adds one unit to either the debit or credit side of a single chosen account k, leaving the opposite side untouched. The module supplies the credit case of this update rule; the debit case appears in the sibling lemma phiVec_post_debit.
proof idea
The tactic proof performs by_cases on the equality i = k. In the equal branch it substitutes the hypothesis, rewrites with post and phiVec, then applies ring_nf. In the unequal branch it rewrites with post, phiVec and the inequality hypothesis hik, again using simp.
why it matters
The lemma is the credit half of the atomic-update rule and is invoked inside phiVec_coordAtomicStep_of_post to establish that any single post produces a coordinate atomic step on the phi vector. That step lemma in turn supplies the missing link between ledger posting and the one-bit parity adjacency proved in LedgerParityAdjacency. Within the Recognition framework the result realizes the local update step required by the eight-tick octave construction at the ledger level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.