post
plain-language theorem explainer
The post operation updates a d-account ledger state by incrementing either the debit or credit counter at one chosen account k by one unit. Researchers working on ledger-based models of recognition events or parity adjacency cite it to formalize atomic ticks. The definition is realized by a direct case split on the posting side that constructs the updated debit and credit functions.
Claim. Let $L$ be a ledger state over $d$ accounts and let $k$ be an account index in $0..d-1$. For side $s$ equal to debit (resp. credit), the updated state post$(L,k,s)$ is the ledger whose debit (resp. credit) function is increased by 1 at coordinate $k$ while the opposite function remains unchanged.
background
LedgerState d is the abbreviation Recognition.Ledger (AccountRS d), where AccountRS equips the finite set Fin d with the trivial recognition relation. Side is the two-element inductive type carrying the labels debit and credit. The module sets up an explicit ledger-shaped model in which each tick performs a single-unit posting to exactly one account, thereby changing the vector phi = debit - credit by exactly ±1 in one coordinate and flipping exactly one bit in the induced parity pattern.
proof idea
The definition is a one-line wrapper that performs classical case analysis on the Side argument. When the side is debit the debit function is replaced by the pointwise update that adds 1 at k; when the side is credit the credit function receives the analogous update. The resulting record is returned directly.
why it matters
This definition supplies the atomic update primitive required by sequential_preserves_conservation and by the eight_tick construction in Gap45.PhysicalMotivation. It supplies the concrete posting rule that converts the abstract ledger language into the one-bit adjacency statements of LedgerParityAdjacency, thereby supporting the eight-tick octave (T7) and the derivation of D = 3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.