postingStep_iff_legalAtomicTick
plain-language theorem explainer
The equivalence identifies a single atomic posting on a d-dimensional ledger with a monotone transition of L1 cost exactly one. Ledger modelers in recognition science cite this to connect explicit posting mechanics to minimal-cost updates. The proof is a direct pairing of the two one-directional implication lemmas.
Claim. For any natural number $d$ and ledger states $L,L'$ in dimension $d$, a single posting step from $L$ to $L'$ holds if and only if the transition is monotone in ledger counts and the $L^1$ distance between them equals one.
background
LedgerState d is the type Recognition.Ledger (AccountRS d), consisting of debit and credit vectors over d accounts. PostingStep requires that L' equals the result of posting one unit to exactly one account on one side. LegalAtomicTick requires the transition to be monotone and to have ledger L1 cost exactly one. The module upgrades vector lemmas to an explicit ledger model whose single-post updates change the phi vector by exactly one unit at one coordinate, inducing a one-bit parity change. Upstream LedgerState structures from variational dynamics and information theory supply the conserved log-ratio and recognition-event interpretations that this ledger posting refines.
proof idea
The proof is a one-line wrapper that applies the two implication lemmas postingStep_implies_legalAtomicTick and legalAtomicTick_implies_PostingStep.
why it matters
This biconditional supplies the exact bridge between the posting definition and the legality predicate, directly enabling the downstream theorem minCost_monotoneStep_implies_postingStep. It completes the glue between ledger language and the parity/Gray adjacency result in LedgerParityAdjacency, supporting the recognition composition law for ledger updates that preserve one-bit parity patterns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.