Ledger Posting Adjacency Jlog1 Le Ledger Jlog Cost Of Monotone Nontrivial

The posting step

A ledger, a discrete record of events, can change in many ways. One account might gain a debit while another gains a credit, or several accounts might move at once. The Recognition Science framework asks a sharp question about such changes: when a ledger moves from one state to a different one, how expensive is that move? The answer, proved in the framework's machine-checked library of formal theorems, is that the cheapest possible real change has a fixed price, and that price is the cost of posting exactly one entry.

The precise statement concerns a ledger with any number of accounts, where a state records how much has been debited and credited to each account. A monotone change means no account's debit or credit total ever decreases. The framework defines a cost function, called Jlog, that assigns a real number to the difference between two ledger states. The theorem Jlog1_le_ledgerJlogCost_of_monotone_nontrivial proves that if the change is monotone and the two states are not identical, then the Jlog cost of the change is at least Jlog(1), the cost of a single posting. In plainer terms: any real, non-decreasing change to the ledger costs at least as much as adding one unit to one account.

This lower bound is tight. A companion theorem shows that a single posting step, moving exactly one unit into exactly one account, achieves the minimum: its Jlog cost equals Jlog(1). Together the two results characterize the cheapest possible ledger update. The framework models a recognition event as such a posting, so the theorem pins down the minimum cost of any genuine event. It is the cost floor beneath every real change in the ledger.

In Recognition Science, this result is the bridge between the abstract cost function and the concrete picture of a ledger being updated one entry at a time. It shows that the framework's notion of a minimal event is not arbitrary: it is forced by the requirement that changes be monotone and non-trivial. The theorem does not say that nature must use this posting model. That step, deriving why the physical world would follow this ledger structure, remains a separate open question in the framework.

/-- Every monotone nontrivial transition costs at least one unit of `Jlog`.
Together with `ledgerJlogCost_eq_Jlog1_of_postingStep`, this makes the
minimum-J posting semantics used downstream explicitly non-vacuous. -/
theorem Jlog1_le_ledgerJlogCost_of_monotone_nontrivial
    {d : Nat} {L L' : LedgerState d}
    (hmono : MonotoneLedger (d := d) L L')
    (hneq : L ≠ L') :
    Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
  by_contra hnot
  have hlt :
      ledgerJlogCost (d := d) L L' < Cost.Jlog (1 : ℝ) :=
    lt_of_not_ge hnot
  have hpost :
      PostingStep (d := d) L L' :=
    postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1
      hmono hneq (le_of_lt hlt)
  have heq :=
    ledgerJlogCost_eq_Jlog1_of_postingStep hpost
  linarith

/-- Every one-account posting has exactly the unit `Jlog` transition cost. -/
theorem ledgerJlogCost_eq_Jlog1_of_postingStep
    {d : Nat} {L L' : LedgerState d}
    (h : PostingStep (d := d) L L') :
    ledgerJlogCost (d := d) L L' = Cost.Jlog (1 : ℝ) := by
  rcases h with ⟨k, side, rfl⟩
  exact ledgerJlogCost_post L k side

What this page does not claim

The theorem does not claim that nature must use this posting model; that bridge is open. The theorem does not claim anything about ledgers that can decrease, only monotone changes. The theorem does not claim the Jlog cost is the only possible cost function, only that it has this minimum.

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: