PostingStep
plain-language theorem explainer
PostingStep encodes the atomic update rule for a d-account ledger: L' differs from L by exactly one unit posted to one account as either debit or credit. Researchers working on ledger-to-parity mappings in Recognition Science cite this to bridge variational dynamics with one-bit adjacency. The definition is a direct existential quantification over the post operation.
Claim. Let $L, L'$ be ledger states over $d$ accounts. Then $L'$ is obtained from $L$ by a posting step if there exists an account index $k$ and a side $s$ (debit or credit) such that $L'$ equals the result of incrementing the debit or credit entry at $k$ by one.
background
LedgerState d is defined as Recognition.Ledger (AccountRS d), where AccountRS equips Fin d with the trivial recognition relation. The post function increments either the debit or credit vector at a chosen coordinate k by one unit. Side is the inductive type with constructors debit and credit. This definition sits inside the module whose purpose is to upgrade the abstract ledger model to an explicit posting mechanism that induces one-bit changes in the parity vector. Upstream LedgerState structures appear in VariationalDynamics (with config and tick) and InformationIsLedger (as lists of recognition events); the local abbrev specializes to the debit-credit form.
proof idea
The definition is the direct existential: PostingStep holds precisely when L' equals post L k side for some k and side.
why it matters
PostingStep is the central predicate linking atomic ledger updates to the parity adjacency results. It is used to prove postingStep_iff_legalAtomicTick and postingStep_oneBitDiff, which establish that legal atomic ticks produce exactly one-bit flips in the parity vector. This fills the gap between the ledger model and the Gray-code adjacency needed for the eight-tick octave. The module doc notes that deriving why nature uses this posting model remains a separate axiom step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.