Encyclopedia Ledger Ledger Posting Adjacency Min Cost Monotone Step Implies Posting Step

ARTICLE 3 claims 3 theorems

Ledger Posting Adjacency Min Cost Monotone Step Implies Posting Step

A theorem about a ledger shows that when moving between two states costs the least possible, the move must be a single posting to one account.

Verify this page

The minimal step

In the Recognition Science framework, a ledger is a discrete record of events, here modeled as a pair of vectors: debits and credits across a fixed set of accounts. A tick, the smallest unit of change, posts exactly one unit to exactly one account, either as a debit or a credit. The theorem minCost_monotoneStep_implies_postingStep states that if a change from one ledger state to another is monotone (no account's balance decreases) and has the minimum possible cost under a simple counting metric, then that change must be a single posting step.

The cost metric in question, ledgerL1Cost, counts the total absolute difference in debits and credits across all accounts between two states. The theorem proves that if this cost is as small as it can be for a non-identical, monotone transition, then the transition is a posting step: exactly one unit moves on one side of one account. The proof relies on a companion fact: a posting step always has cost exactly 1, and any monotone, non-identical transition with cost at most 1 must be a posting step. The result is a formal theorem in the framework's machine-checked library of formal theorems, meaning it is derived from definitions and prior lemmas without additional assumptions.

The theorem does not claim that nature must use this posting model. The framework's own documentation marks the step from this mathematical model to a physical necessity as a separate, open bridge problem. It also does not claim that the minimum cost is unique; other transitions could tie at the same cost, but the theorem guarantees that any such minimum, under monotonicity, is a posting step. Finally, the theorem concerns only the L1 counting cost, not the framework's logarithmic cost function J, although a parallel theorem exists for that cost as well.

THEOREM minCost_monotoneStep_implies_postingStep · IndisputableMonolith/LedgerPostingAdjacency.lean
minCost_monotoneStep_implies_postingStep · IndisputableMonolith/LedgerPostingAdjacency.lean:963 
theorem minCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
    {L L' : LedgerState d}
    (hmono : MonotoneLedger (d := d) L L')
    (hneq : L ≠ L')
    (hmin : ∀ L'' : LedgerState d, MonotoneLedger (d := d) L L'' → L ≠ L'' →
      ledgerL1Cost (d := d) L L' ≤ ledgerL1Cost (d := d) L L'') :
    PostingStep (d := d) L L' := by
  classical
  -- compare against a concrete single-post candidate (cost = 1)
  let k0 : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
  have hpostNe : L ≠ post L k0 Side.debit := by
    intro hEq
    have hdeb : L.debit k0 = L.debit k0 + 1 := by
      -- RHS is `L.debit k0 + 1`
      have := congrArg (fun s => s.debit k0) hEq
      simpa [post] using this
    linarith
  have hle1 : ledgerL1Cost (d := d) L L' ≤ 1 := by
    have hmono' : MonotoneLedger (d := d) L (post L k0 Side.debit) :=
      post_monotone (d := d) L k0 Side.debit
    have hcost' : ledgerL1Cost (d := d) L (post L k0 Side.debit) = 1 :=
      ledgerL1Cost_post (d := d) L k0 Side.debit
    have := hmin (post L k0 Side.debit) hmono' hpostNe
    simpa [hcost'] using this
  have hcostNe0 : ledgerL1Cost (d := d) L L' ≠ 0 := by
    intro h0
    have : L' = L := (ledgerL1Cost_eq_zero_iff (d := d) L L').1 h0
    exact hneq (by simpa [this])
  have hcost1 : ledgerL1Cost (d := d) L L' = 1 := by
    have hcases := Nat.le_one_iff_eq_zero_or_eq_one.1 hle1
    cases hcases with
    | inl h0 => exact (hcostNe0 h0).elim
    | inr h1 => exact h1
  -- conclude via the `PostingStep ↔ LegalAtomicTick` equivalence
  have hlegal : LegalAtomicTick (d := d) L L' := ⟨hmono, hcost1⟩
  exact (postingStep_iff_legalAtomicTick (d := d)).2 hlegal
THEOREM ledgerL1Cost_post · IndisputableMonolith/LedgerPostingAdjacency.lean
ledgerL1Cost_post · IndisputableMonolith/LedgerPostingAdjacency.lean:720 
private lemma ledgerL1Cost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
    ledgerL1Cost (d := d) L (post L k side) = 1 := by
  classical
  cases side with
  | debit =>
      -- debit changes by +1 at k; credit unchanged
      have hdebit :
          (∑ i : Fin d, Int.natAbs ((post L k Side.debit).debit i - L.debit i)) = 1 := by
        -- isolate `k` and show everything else is 0
        let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.debit).debit i - L.debit i)
        have hsplit :=
          (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
        have fk : f k = 1 := by
          simp [f, post]
        have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
          refine Finset.sum_eq_zero ?_
          intro i hi
          have hik : i ≠ k := by
            simpa [Finset.mem_erase] using hi
          simp [f, post, hik]
        -- rewrite `∑ univ` using `hsplit.symm`
        simpa [f] using (by
          calc
            (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
              simpa using hsplit.symm
            _ = 1 := by simp [fk, hErase])
      have hcredit :
          (∑ i : Fin d, Int.natAbs ((post L k Side.debit).credit i - L.credit i)) = 0 := by
        -- credit is unchanged everywhere
        refine Finset.sum_eq_zero ?_
        intro i _
        simp [post]
      -- assemble
      simp [ledgerL1Cost, hdebit, hcredit]
  | credit =>
      -- credit changes by +1 at k; debit unchanged
      have hdebit :
          (∑ i : Fin d, Int.natAbs ((post L k Side.credit).debit i - L.debit i)) = 0 := by
        refine Finset.sum_eq_zero ?_
        intro i _
        simp [post]
      have hcredit :
          (∑ i : Fin d, Int.natAbs ((post L k Side.credit).credit i - L.credit i)) = 1 := by
        let f : Fin d → Nat := fun i => Int.natAbs ((post L k Side.credit).credit i - L.credit i)
        have hsplit :=
          (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
        have fk : f k = 1 := by
          simp [f, post]
        have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
          refine Finset.sum_eq_zero ?_
          intro i hi
          have hik : i ≠ k := by
            simpa [Finset.mem_erase] using hi
          simp [f, post, hik]
        simpa [f] using (by
          calc
            (∑ i : Fin d, f i) = f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
              simpa using hsplit.symm
            _ = 1 := by simp [fk, hErase])
      simp [ledgerL1Cost, hdebit, hcredit]
THEOREM minCost_monotoneStep_implies_postingStep · IndisputableMonolith/LedgerPostingAdjacency.lean
minCost_monotoneStep_implies_postingStep · IndisputableMonolith/LedgerPostingAdjacency.lean:963 
theorem minCost_monotoneStep_implies_postingStep {d : Nat} [NeZero d]
    {L L' : LedgerState d}
    (hmono : MonotoneLedger (d := d) L L')
    (hneq : L ≠ L')
    (hmin : ∀ L'' : LedgerState d, MonotoneLedger (d := d) L L'' → L ≠ L'' →
      ledgerL1Cost (d := d) L L' ≤ ledgerL1Cost (d := d) L L'') :
    PostingStep (d := d) L L' := by
  classical
  -- compare against a concrete single-post candidate (cost = 1)
  let k0 : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
  have hpostNe : L ≠ post L k0 Side.debit := by
    intro hEq
    have hdeb : L.debit k0 = L.debit k0 + 1 := by
      -- RHS is `L.debit k0 + 1`
      have := congrArg (fun s => s.debit k0) hEq
      simpa [post] using this
    linarith
  have hle1 : ledgerL1Cost (d := d) L L' ≤ 1 := by
    have hmono' : MonotoneLedger (d := d) L (post L k0 Side.debit) :=
      post_monotone (d := d) L k0 Side.debit
    have hcost' : ledgerL1Cost (d := d) L (post L k0 Side.debit) = 1 :=
      ledgerL1Cost_post (d := d) L k0 Side.debit
    have := hmin (post L k0 Side.debit) hmono' hpostNe
    simpa [hcost'] using this
  have hcostNe0 : ledgerL1Cost (d := d) L L' ≠ 0 := by
    intro h0
    have : L' = L := (ledgerL1Cost_eq_zero_iff (d := d) L L').1 h0
    exact hneq (by simpa [this])
  have hcost1 : ledgerL1Cost (d := d) L L' = 1 := by
    have hcases := Nat.le_one_iff_eq_zero_or_eq_one.1 hle1
    cases hcases with
    | inl h0 => exact (hcostNe0 h0).elim
    | inr h1 => exact h1
  -- conclude via the `PostingStep ↔ LegalAtomicTick` equivalence
  have hlegal : LegalAtomicTick (d := d) L L' := ⟨hmono, hcost1⟩
  exact (postingStep_iff_legalAtomicTick (d := d)).2 hlegal

What this page does not claim

The theorem does not prove that the minimum cost transition is unique. The theorem does not apply to non-monotone transitions or to costs other than the L1 counting metric.

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