Ledger Posting Adjacency Min Jlog Cost Monotone Step Implies Posting Step

The cheapest allowed change

A ledger with two columns, debit and credit, for each of several accounts. A ledger, a discrete record of such balances, changes over time. The theorem in question concerns the cheapest possible change from one valid ledger state to another, where the cost of a change is measured by a specific function, Jlog, that assigns a nonnegative real number to the difference in each account.

The theorem, named minJlogCost_monotoneStep_implies_postingStep, states: if you have two distinct ledger states, the second reachable from the first by only increasing account balances (a monotone step), and if the Jlog cost of this change is minimal among all such monotone changes, then the change must be a posting step. A posting step is the simplest possible operation: it adds exactly one unit to exactly one account, either as a debit or a credit. The proof, checked by the framework's machine-checked library of formal theorems, shows that any minimal-cost monotone change has this atomic form.

This result is a bridge. It connects the abstract language of recognition costs to a concrete, combinatorial model of ledger updates. It says that if nature or any system is forced to pay the minimum Jlog cost to move between states, it can only do so by making a single, indivisible posting. This is a mathematical theorem about a defined cost function and a defined ledger model; it is not a claim about why nature must use this model.

The theorem does not say that a posting step is always the cheapest change; it says that if a change is cheapest and monotone, it must be a posting step. It also does not establish that the Jlog cost function is the only possible cost, nor does it derive the ledger model from physical principles. Those remain separate, open questions. The theorem's power is in its precision: it pins down the exact shape of a minimal-cost transition within a specific, formalized framework.

theorem minJlogCost_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'' →
      ledgerJlogCost (d := d) L L' ≤ ledgerJlogCost (d := d) L L'') :
    PostingStep (d := d) L L' := by
  classical
  -- compare against a concrete single-post candidate (Jlog-cost = Jlog 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
      have := congrArg (fun s => s.debit k0) hEq
      simpa [post] using this
    linarith
  have hmono' : MonotoneLedger (d := d) L (post L k0 Side.debit) :=
    post_monotone (d := d) L k0 Side.debit
  have hcost' : ledgerJlogCost (d := d) L (post L k0 Side.debit) = Cost.Jlog (1 : ℝ) :=
    ledgerJlogCost_post (d := d) L k0 Side.debit
  have hleJ1 : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ) := by
    have := hmin (post L k0 Side.debit) hmono' hpostNe
    simpa [hcost'] using this
  exact postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 (d := d) (L := L) (L' := L') hmono hneq hleJ1

What this page does not claim

The theorem does not prove that nature must use this posting model. The theorem does not claim that a posting step is always the minimal-cost change. The theorem does not derive the Jlog cost function from first principles.

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: