Ledger Posting Adjacency Posting Step Iff Legal Atomic Tick

The posting step

In the Recognition Science framework, a ledger (a discrete record of events) keeps two numbers for each of its accounts: a debit total and a credit total. A tick (one unit of recognition activity) is the smallest possible change to this record. The framework's machine-checked library of formal theorems proves that a legal atomic tick, defined as a change that respects the monotone rule (no account total ever decreases) and costs exactly one unit of L1 distance, is the same thing as a posting step, defined as adding exactly one unit to exactly one account. The theorem postingStep_iff_legalAtomicTick states this equivalence directly: PostingStep L L' ↔ LegalAtomicTick L L'.

This is a mathematical model, not a claim about nature. The model chooses a specific shape for the ledger: a state is a pair of vectors, one for debits and one for credits, over a finite set of accounts. The theorem proves that within this model, the two definitions coincide. It does not prove that nature must use this posting model. Deriving why nature would be forced to use it is a separate bridge step, which the framework's own documentation marks as open.

The theorem's payoff is a clean characterization: the cheapest possible nontrivial change to a ledger, under the monotone rule, is always a single posting. This links the ledger language to the parity and Gray adjacency lemmas in the framework's library. A posting step changes the parity pattern (the pattern of which accounts have odd totals) in exactly one bit. The equivalence is the glue that lets the framework speak of a ledger and a one-bit change as the same event.

What the theorem does not claim is just as important. It does not claim that the posting model is the only possible ledger model, nor that the cost function used (the L1 cost) is the only one that could define a legal tick. It does not claim that the equivalence holds for any other notion of cost or any other ledger shape. It is a theorem about the specific definitions in the framework's library, and nothing more.

theorem postingStep_iff_legalAtomicTick {d : Nat} {L L' : LedgerState d} :
    PostingStep (d := d) L L' ↔ LegalAtomicTick (d := d) L L' :=
  ⟨postingStep_implies_legalAtomicTick (d := d), legalAtomicTick_implies_PostingStep (d := d)⟩

theorem postingStep_oneBitDiff {d : Nat} {L L' : LedgerState d} (h : PostingStep (d := d) L L') :
    OneBitDiff (parity d L) (parity d L') := by
  rcases h with ⟨k, side, rfl⟩
  simpa using parity_oneBitDiff_of_post (d := d) L k side

What this page does not claim

The posting model is the only possible ledger model. Nature is forced to use this posting model. The equivalence holds for any other cost function or ledger shape.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/LedgerPostingAdjacency.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: