Ledger Posting Adjacency

Posting and adjacency

A ledger in the ordinary sense is a book of accounts, each holding a running total of debits and credits. The same picture appears inside Recognition Science. A ledger, a discrete record of events, has a fixed number of accounts. A tick, one unit of recognition activity, posts exactly one unit to exactly one account, either as a debit or a credit. Nothing else can happen in a single step. That rule is a definitional choice, a model, not a claim about nature.

The interesting fact is what this posting rule does to a derived quantity. Each account has a balance phi, defined as debit minus credit. A single post changes phi by plus or minus one at exactly one coordinate. The result then takes a binary pattern, the parity of each balance, and proves the adjacency result: after any legal single post, the parity pattern differs in exactly one bit. This is the Gray code adjacency property, familiar from electronics and combinatorics, appearing here as a consequence of a bookkeeping rule.

The equivalence is clean. A posting step, one unit into one account, is exactly the same thing as a legal atomic tick, defined as a monotone ledger change with L1 cost equal to one. The theorem postingStep_iff_legalAtomicTick states this equivalence. A related theorem, legalAtomicTick_oneBitDiff, states that such a tick always produces a one-bit difference in the parity pattern. The proofs are machine-checked in the framework's library of formal theorems.

Why does this matter? The result is the missing glue between ledger language and a parity adjacency lemma that already existed. It shows that a ledger-shaped model, with posting updates, is compatible with the one-bit adjacency structure. It does not show that nature must use this posting model. That bridge, from mathematics to physics, remains open. The value here is structural: a clean, checkable statement that a bookkeeping rule and a binary adjacency property are the same thing.

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)⟩

lemma phiVec_coordAtomicStep_of_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
    coordAtomicStep (d := d) (phiVec (d := d) L) (phiVec (d := d) (post L k side)) := by
  classical
  refine ⟨k, ?_, ?_⟩
  · cases side with
    | debit =>
        left
        -- at k, phi increases by 1
        simpa using (by
          have := (phiVec_post_debit (d := d) L k k)
          simpa using this)
    | credit =>
        right
        -- at k, phi decreases by 1
        simpa using (by
          have := (phiVec_post_credit (d := d) L k k)
          simpa using this)
  · intro i hik
    cases side with
    | debit =>
        -- other coordinates unchanged
        have := (phiVec_post_debit (d := d) L k i)
        simpa [hik] using this
    | credit =>
        have := (phiVec_post_credit (d := d) L k i)
        simpa [hik] using this

theorem legalAtomicTick_oneBitDiff {d : Nat} {L L' : LedgerState d}
    (h : LegalAtomicTick (d := d) L L') :
    OneBitDiff (parity d L) (parity d L') :=
  postingStep_oneBitDiff (legalAtomicTick_implies_PostingStep (d := d) h)

What this page does not claim

The posting model is a definitional choice, not a derived law of nature. The result does not prove that the parity pattern itself has physical meaning. The bridge from this mathematical model to physical recognition is not established here.

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: