Encyclopedia Ledger Ledger Posting Adjacency Posting Step Implies Legal Atomic Tick

ARTICLE 4 claims 4 theorems

Ledger Posting Adjacency Posting Step Implies Legal Atomic Tick

In a discrete ledger of recognition events, the smallest possible lawful change is exactly one unit posted to one account, and the framework proves the two descriptions coincide.

Verify this page

Posting steps and legal atomic ticks

A ledger is a discrete record of events, here kept as a list of accounts, each with a debit and a credit balance. A posting step is the simplest possible update: it adds exactly one unit to exactly one account, on either the debit or the credit side. The framework's library of machine-checked formal theorems proves that this minimal action is the same thing as a legal atomic tick, its term for the smallest change that respects the ledger's monotonicity rule (no balance ever decreases) and costs exactly one unit of its L1 distance, the sum of absolute differences across all accounts.

The equivalence runs in both directions. If a posting step occurs, the resulting state is a legal atomic tick. Conversely, any legal atomic tick must have been a posting step. The proof is short: a single post changes the difference between debit and credit by plus or minus one at exactly one coordinate, so the parity pattern, the bit string of which balances are odd, changes in exactly one bit. That one-bit adjacency is the bridge to Gray-code style structure in the framework's account of recognition cycles.

In Recognition Science, this theorem is the glue that connects the informal language of ledgers to a precise parity lemma. It shows that the discrete recognition carrier, the minimal substrate of accounts, behaves exactly as the posting model says. The framework models nature's smallest recognition events as these posting steps, and the theorem confirms that the model is internally consistent: the cheapest legal move is always a single post, never a combination or a fractional unit.

What the theorem does not claim is that nature must use this posting model. That is a separate, open bridge step between the mathematics and the physics. The theorem also does not say that every sequence of posting steps is physically meaningful, only that each step is the minimal legal change. It leaves untouched the question of why the cost function takes its particular form, which is proved elsewhere in the framework, and it does not by itself force any particular number of accounts or dimensions.

THEOREM postingStep_iff_legalAtomicTick · IndisputableMonolith/LedgerPostingAdjacency.lean
postingStep_iff_legalAtomicTick · IndisputableMonolith/LedgerPostingAdjacency.lean:957 
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_implies_legalAtomicTick · IndisputableMonolith/LedgerPostingAdjacency.lean
postingStep_implies_legalAtomicTick · IndisputableMonolith/LedgerPostingAdjacency.lean:785 
theorem postingStep_implies_legalAtomicTick {d : Nat} {L L' : LedgerState d}
    (h : PostingStep (d := d) L L') : LegalAtomicTick (d := d) L L' := by
  rcases h with ⟨k, side, rfl⟩
  exact legalAtomicTick_of_post (d := d) L k side
THEOREM legalAtomicTick_implies_PostingStep · IndisputableMonolith/LedgerPostingAdjacency.lean
legalAtomicTick_implies_PostingStep · IndisputableMonolith/LedgerPostingAdjacency.lean:843 
theorem legalAtomicTick_implies_PostingStep {d : Nat} {L L' : LedgerState d}
    (h : LegalAtomicTick (d := d) L L') : PostingStep (d := d) L L' := by
  classical
  rcases h with ⟨hmono, hcost⟩
  rcases hmono with ⟨hmonoD, hmonoC⟩
  -- split the total cost into debit-cost and credit-cost
  let dCost : Nat := ∑ i : Fin d, Int.natAbs (L'.debit i - L.debit i)
  let cCost : Nat := ∑ i : Fin d, Int.natAbs (L'.credit i - L.credit i)
  have hsplit : dCost + cCost = 1 := by
    simpa [ledgerL1Cost, dCost, cCost] using hcost
  have hcases := Nat.add_eq_one_iff.mp hsplit
  cases hcases with
  | inl hc =>
      -- dCost = 0, cCost = 1 → credit posting
      have hd0 : dCost = 0 := hc.1
      have hc1 : cCost = 1 := hc.2
      -- choose the unique changed credit coordinate
      have ⟨k, hk1, hkrest⟩ :=
        exists_unique_of_sum_univ_eq_one (d := d) (f := fun i => Int.natAbs (L'.credit i - L.credit i)) hc1
      -- debit diffs all 0
      have hdAll :
          ∀ i : Fin d, Int.natAbs (L'.debit i - L.debit i) = 0 := by
        have hall0 :
            ∀ i : Fin d, i ∈ (Finset.univ : Finset (Fin d)) → Int.natAbs (L'.debit i - L.debit i) = 0 := by
          have :=
            (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
              (f := fun i => Int.natAbs (L'.debit i - L.debit i))
              (fun _ _ => Nat.zero_le _)).1 hd0
          simpa [dCost] using this
        intro i; exact hall0 i (by simp)
      -- build PostingStep = post at k on credit side
      refine ⟨k, Side.credit, ?_⟩
      -- prove L' = post L k credit by field ext (no `[ext]` lemma registered)
      cases L with
      | mk debit credit =>
        cases L' with
        | mk debit' credit' =>
          -- show the debit field is unchanged
          have hdebit' : debit' = debit := by
            funext i
            have hz := int_eq_of_natAbs_eq_zero (hdAll i)
            have hz' : (debit' i - debit i) = 0 := by simpa using hz
            linarith
          -- show the credit field matches the `post` update
          have hcredit' :
              credit' = (fun i => if i = k then credit i + 1 else credit i) := by
            funext i
            by_cases hik : i = k
            · subst hik
              -- goal reduces to `credit' i = credit i + 1`
              simp
              have hzabs : Int.natAbs (credit' i - credit i) = 1 := hk1
              have hnn : 0 ≤ (credit' i - credit i) := by
                have : credit i ≤ credit' i := hmonoC i
                linarith
              have hz : (credit' i - credit i) = 1 :=
                int_natAbs_eq_one_of_nonneg (z := (credit' i - credit i)) hzabs hnn
              linarith
            · -- goal reduces to `credit' i = credit i`
              have hzabs : Int.natAbs (credit' i - credit i) = 0 := hkrest i hik
              have hz : (credit' i - credit i) = 0 := int_eq_of_natAbs_eq_zero hzabs
              simp [hik]
              linarith
          -- finish
          subst hdebit' hcredit'
          simp [post]
          ext i <;> by_cases h : i = k <;> simp [h]
  | inr hc =>
      -- dCost = 1, cCost = 0 → debit posting
      have hd1 : dCost = 1 := hc.1
      have hc0 : cCost = 0 := hc.2
      have ⟨k, hk1, hkrest⟩ :=
        exists_unique_of_sum_univ_eq_one (d := d) (f := fun i => Int.natAbs (L'.debit i - L.debit i)) hd1
      have hcAll :
          ∀ i : Fin d, Int.natAbs (L'.credit i - L.credit i) = 0 := by
        have hall0 :
            ∀ i : Fin d, i ∈ (Finset.univ : Finset (Fin d)) → Int.natAbs (L'.credit i - L.credit i) = 0 := by
          have :=
            (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
              (f := fun i => Int.natAbs (L'.credit i - L.credit i))
              (fun _ _ => Nat.zero_le _)).1 hc0
          simpa [cCost] using this
        intro i; exact hall0 i (by simp)
      refine ⟨k, Side.debit, ?_⟩
      cases L with
      | mk debit credit =>
        cases L' with
        | mk debit' credit' =>
          have hcredit' : credit' = credit := by
            funext i
            have hz := int_eq_of_natAbs_eq_zero (hcAll i)
            have hz' : (credit' i - credit i) = 0 := by simpa using hz
            linarith
          have hdebit' :
              debit' = (fun i => if i = k then debit i + 1 else debit i) := by
            funext i
            by_cases hik : i = k
            · subst hik
              simp
              have hzabs : Int.natAbs (debit' i - debit i) = 1 := hk1
              have hnn : 0 ≤ (debit' i - debit i) := by
                have : debit i ≤ debit' i := hmonoD i
                linarith
              have hz : (debit' i - debit i) = 1 :=
                int_natAbs_eq_one_of_nonneg (z := (debit' i - debit i)) hzabs hnn
              linarith
            · have hzabs : Int.natAbs (debit' i - debit i) = 0 := hkrest i hik
              have hz : (debit' i - debit i) = 0 := int_eq_of_natAbs_eq_zero hzabs
              simp [hik]
              linarith
          subst hcredit' hdebit'
          simp [post]
          ext i <;> by_cases h : i = k <;> simp [h]
THEOREM postingStep_oneBitDiff · IndisputableMonolith/LedgerPostingAdjacency.lean
postingStep_oneBitDiff · IndisputableMonolith/LedgerPostingAdjacency.lean:146 
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

Nature must use this posting model; that bridge step remains open. Every posting step sequence is physically meaningful. The theorem forces any particular number of accounts or spatial dimensions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND