Encyclopedia Ledger Ledger Posting Adjacency Legal Atomic Tick Implies Posting Step

ARTICLE 3 claims 3 theorems

Ledger Posting Adjacency Legal Atomic Tick Implies Posting Step

A legal atomic tick is exactly one posting: a single unit moved to a single account, nothing more.

Verify this page

The posting step

In ordinary bookkeeping, a posting is the smallest meaningful update: you move one unit into one account, either as a debit or a credit. The Recognition Science declaration legalAtomicTick, a legal atomic tick, formalizes this as a ledger state change that is monotone (no account ever decreases) and has a total cost of exactly one unit under a simple distance measure. The theorem legalAtomicTick_implies_PostingStep proves that any such tick is in fact a posting: it must move exactly one unit to exactly one account, with all other accounts unchanged.

The proof is short and structural. A legal atomic tick has a cost of one, and the cost is a sum of nonnegative absolute differences across all accounts. If two or more accounts changed, the sum would be at least two. If one account changed by more than one unit, the sum would again exceed one. Monotonicity rules out negative changes. Therefore exactly one account changes, and it changes by exactly one unit. The theorem postingStep_iff_legalAtomicTick then gives the converse: every posting is a legal atomic tick, so the two notions coincide exactly.

This equivalence is the glue between the ledger language and a parity pattern. Each account's balance difference, debit minus credit, is a vector. A posting changes that vector by plus or minus one at exactly one coordinate. The induced parity pattern, which records the sign of each coordinate, therefore changes in exactly one bit. The theorem legalAtomicTick_oneBitDiff states this consequence directly. The library proves that a single posting is the unique minimal way to move from one monotone ledger state to another, under both the simple L1 cost and the logarithmic Jlog cost.

In Recognition Science, this result is a mathematical model, not a claim about nature. The framework's library, a machine-checked collection of formal theorems, proves the equivalence within its own definitions. It does not prove that nature must use this posting model. That bridge, why physical recognition should follow this ledger structure, is a separate open step. The theorem is also not a claim about time: it says nothing about when postings occur, only what a single legal step must be.

What the theorem gives a reader is a precise, checkable answer to a simple question: if a recognition event is atomic and legal, what can it do? Exactly one posting. That fact anchors the later results about parity patterns and minimal cost, and it shows that the ledger language is not loose metaphor but a structure with exact consequences.

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_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 legalAtomicTick_oneBitDiff · IndisputableMonolith/LedgerPostingAdjacency.lean
legalAtomicTick_oneBitDiff · IndisputableMonolith/LedgerPostingAdjacency.lean:1027 
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 theorem does not prove that nature must use this posting model. The theorem does not say when postings occur, only what a single legal step must be. The theorem does not claim that the ledger is a physical object.

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