Encyclopedia Ledger Ledger Posting Adjacency Posting Step Of Monotone And Ledger Jlog Cost Le Jlog1

ARTICLE 3 claims 1 theorem 2 models

Ledger Posting Adjacency Posting Step Of Monotone And Ledger Jlog Cost Le Jlog1

A single theorem turns a ledger's smallest possible cost into a simple rule: one tick, one account, one unit.

Verify this page

The posting step

A ledger, in the Recognition Science framework, is a discrete record of events: a state holds a count of debits and credits for each of a fixed number of accounts. A posting step is the simplest possible change: exactly one unit added to exactly one account, either as a debit or a credit. The theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 states that if a transition between two ledger states is monotone, meaning no account's debit or credit count ever decreases, and if the transition's cost is no more than the cost of a single unit change, then the transition must be a posting step.

The cost here is not arbitrary. It is the ledger cost, a sum over all accounts of a function applied to the change in each debit and credit count. The function is the framework's forced cost function, J(x) = (x + 1/x)/2 - 1, which the framework proves is the only cost function satisfying five plain conditions. The theorem's power is that it runs the argument backward: given a monotone transition whose cost is at most J(1), the cost of a single unit change, the transition must be exactly that single unit change. A larger change would cost more, so the cost bound forces the simple form.

The theorem is a bridge between two descriptions of the same event. One description is abstract: a transition with a small cost. The other is concrete: a posting step, one unit to one account. The framework's library, a machine-checked collection of formal theorems, proves the equivalence. This matters because the posting step is the atomic event from which the framework builds its eight-tick recognition cycle and, from that, the number 2^3 and three spatial dimensions. The theorem is the glue that lets the framework move from a general cost principle to a specific, discrete action.

What the theorem does not claim is just as important as what it proves. It does not claim that nature must use this posting model. The theorem is a mathematical statement about a defined model; why the physical world should follow it is a separate, open bridge step. It also does not claim that any monotone transition with cost at most J(1) is a posting step in every possible cost function; the result is specific to the framework's forced J cost. Finally, it does not claim that the cost of a posting step is always J(1); that is a separate lemma, and the theorem only uses the cost bound as a hypothesis.

THEOREM postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 · IndisputableMonolith/LedgerPostingAdjacency.lean
postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 · IndisputableMonolith/LedgerPostingAdjacency.lean:263 · truncated 
theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 {d : Nat} {L L' : LedgerState d}
    (hmono : MonotoneLedger (d := d) L L')
    (hneq : L ≠ L')
    (hle : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ)) :
    PostingStep (d := d) L L' := by
  classical
  -- helper: deltas
  let dΔ : Fin d → ℤ := fun i => L'.debit i - L.debit i
  let cΔ : Fin d → ℤ := fun i => L'.credit i - L.credit i
  have hdNonneg : ∀ i : Fin d, 0 ≤ dΔ i := by
    intro i
    have : L.debit i ≤ L'.debit i := hmono.1 i
    dsimp [dΔ]
    linarith
  have hcNonneg : ∀ i : Fin d, 0 ≤ cΔ i := by
    intro i
    have : L.credit i ≤ L'.credit i := hmono.2 i
    dsimp [cΔ]
    linarith

  -- show every delta is ≤ 1 (otherwise cost would exceed Jlog 1)
  have hdLeOne : ∀ i : Fin d, dΔ i ≤ 1 := by
    intro i
    by_contra hgt
    have hlt : (1 : ℤ) < dΔ i := lt_of_not_ge hgt
    have h2 : (2 : ℤ) ≤ dΔ i := by
      -- `2 ≤ z ↔ 1 < z`
      exact (Int.add_one_le_iff).2 hlt
    -- strict lower bound on this term
    have hx : (1 : ℝ) < ((dΔ i : ℤ) : ℝ) := by
      -- cast `1 < dΔ i` to ℝ
      exact_mod_cast hlt
    have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((dΔ i : ℤ) : ℝ) :=
      jlog_lt_jlog_of_one_lt (x := ((dΔ i : ℤ) : ℝ)) hx
    -- this term is bounded by total cost (single term ≤ sum) and total cost ≤ Jlog 1: contradiction
    let fD : Fin d → ℝ := fun j => Cost.Jlog ((dΔ j : ℤ) : ℝ)
    have hterm_le_sum : fD i ≤ ∑ j : Fin d, fD j := by
      -- `fD i ≤ sum univ fD` by nonneg
      have hnonneg : ∀ j : Fin d, 0 ≤ fD j := fun _ => Cost.Jlog_nonneg _
      -- use `i` in univ
      -- work directly with `Finset.univ` to avoid rewriting via `Fintype.sum`
      have : fD i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fD :=
        Finset.single_le_sum (by
          intro j hj
          exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
      simpa using this
    have hsum_le_cost : (∑ j : Fin d, fD j) ≤ ledgerJlogCost (d := d) L L' := by
      -- debit sum ≤ debit sum + credit sum
      have hcredit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((cΔ j : ℤ) : ℝ) :=
        Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
      dsimp [ledgerJlogCost, dΔ, cΔ]
      exact le_add_of_nonneg_right hcredit_nonneg
    have hterm_le_cost : Cost.Jlog ((dΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
      -- rewrite `fD i` and compose inequalities
      have : fD i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
      simpa [fD] using this
    have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' :=
      lt_of_lt_of_le hterm_lt hterm_le_cost
    exact (not_lt_of_ge hle) this

  have hcLeOne : ∀ i : Fin d, cΔ i ≤ 1 := by
    intro i
    by_contra hgt
    have hlt : (1 : ℤ) < cΔ i := lt_of_not_ge hgt
    have hx : (1 : ℝ) < ((cΔ i : ℤ) : ℝ) := by exact_mod_cast hlt
    have hterm_lt : Cost.Jlog (1 : ℝ) < Cost.Jlog ((cΔ i : ℤ) : ℝ) :=
      jlog_lt_jlog_of_one_lt (x := ((cΔ i : ℤ) : ℝ)) hx
    let fC : Fin d → ℝ := fun j => Cost.Jlog ((cΔ j : ℤ) : ℝ)
    have hterm_le_sum : fC i ≤ ∑ j : Fin d, fC j := by
      have hnonneg : ∀ j : Fin d, 0 ≤ fC j := fun _ => Cost.Jlog_nonneg _
      have : fC i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fC :=
        Finset.single_le_sum (by
          intro j hj
          exact hnonneg j) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
      simpa using this
    have hsum_le_cost : (∑ j : Fin d, fC j) ≤ ledgerJlogCost (d := d) L L' := by
      have hdebit_nonneg : 0 ≤ ∑ j : Fin d, Cost.Jlog ((dΔ j : ℤ) : ℝ) :=
        Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
      dsimp [ledgerJlogCost, dΔ, cΔ]
      exact le_add_of_nonneg_left hdebit_nonneg
    have hterm_le_cost : Cost.Jlog ((cΔ i : ℤ) : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
      have : fC i ≤ ledgerJlogCost (d := d) L L' := le_trans hterm_le_sum hsum_le_cost
      simpa [fC] using this
    have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' :=
      lt_of_lt_of_le hterm_lt hterm_le_cost
    exact (not_lt_of_ge hle) this

  -- Convert bounded deltas to `{0,1}` cases.
  have hd01 : ∀ i : Fin d, dΔ i = 0 ∨ dΔ i = 1 := by
    intro i
    have h0 : 0 ≤ dΔ i := hdNonneg i
    have h1 : dΔ i ≤ 1 := hdLeOne i
    cases hdi : dΔ i with
    | ofNat n =>
        have hn : n ≤ 1 := by
          have : (Int.ofNat n) ≤ (1 : ℤ) := by simpa [hdi] using h1
          exact (Int.ofNat_le).1 this
        rcases Nat.le_one_iff_eq_zero_or_eq_one.1 hn with rfl | rfl <;> simp [hdi]
    | negSucc n =>
        exfalso
        have : ¬ (0 ≤ (Int.negSucc n)) := by
          have : (Int.negSucc n) < 0 := by simpa using (Int.negSucc_lt_zero n)
          exact not_le_of_gt this
        exact this (by simpa [hdi] using h0)

  have hc01 : ∀ i : Fin d, cΔ i = 0 ∨ cΔ i = 1 := by
    intro i
    have h0 : 0 ≤ cΔ i := hcNonneg i
    have h1 : cΔ i ≤ 1 := hcLeOne i
    cases hci : cΔ i with
    | ofNat n =>
        have hn : n ≤ 1 := by
          have : (Int.ofNat n) ≤ (1 : ℤ) := by simpa [hci] using h1
          exact (Int.ofNat_le).1 this
        rcases Nat.le_one_iff_eq_zero_or_eq_one.1 hn with rfl | rfl <;> simp [hci]
    | negSucc n =>
        exfalso
        have : ¬ (0 ≤ (Int.negSucc n)) := by
          have : (Int.negSucc n) < 0 := by simpa using (Int.negSucc_lt_zero n)
          exact not_le_of_gt this
        exact this (by simpa [hci] using h0)

  -- existence of some 1 (since L ≠ L')
  have hex1 : (∃ i : Fin d, dΔ i = 1) ∨ (∃ i : Fin d, cΔ i = 1) := by
    by_contra hnone
    have hnoneD : ∀ i : Fin d, dΔ i = 0 := by
      intro i
      have : ¬ dΔ i = 1 := by
        have : ¬ (∃ i : Fin d, dΔ i = 1) := (not_or.mp hnone).1
        exact fun hi => this ⟨i, hi⟩
      cases hd01 i with
      | inl hz => exact hz
      | inr h1 => exact (this h1).elim
    have hnoneC : ∀ i : Fin d, cΔ i = 0 := by
      intro i
      have : ¬ cΔ i = 1 := by
        have : ¬ (∃ i : Fin d, cΔ i = 1) := (not_or.mp hnone).2
        exact fun hi => this ⟨i, hi⟩
      cases hc01 i with
      | inl hz => exact hz
      | inr h1 => exact (this h1).elim
    -- all deltas are 0 ⇒ ledger equal
    cases L with
    | mk debit credit =>
      cases L' with
      | mk debit' credit' =>
        have hdebitEq : debit' = debit := by
          funext i
          have : debit' i - debit i = 0 := by simpa [dΔ] using hnoneD i
          linarith
        have hcreditEq : credit' = credit := by
          funext i
          have : credit' i - credit i = 0 := by simpa [cΔ] using hnoneC i
          linarith
        exact hneq (by cases hdebitEq; cases hcreditEq; rfl)
  -- uniqueness: cannot have both a debit-1 and a credit-1, and cannot have two debit-1s, etc., else cost > Jlog 1.
  have j1pos : 0 < Cost.Jlog (1 : ℝ) := by
    have hnonneg : 0 ≤ Cost.Jlog (1 : ℝ) := Cost.Jlog_nonneg 1
    have hne : Cost.Jlog (1 : ℝ) ≠ 0 := by
      intro hzero
      have : (1 : ℝ) = 0 := (Cost.Jlog_eq_zero_iff 1).mp hzero
      norm_num at this
    exact lt_of_le_of_ne hnonneg (Ne.symm hne)
  have not_two_ones :
      ¬((∃ i : Fin d, dΔ i = 1) ∧ (∃ j : Fin d, cΔ j = 1)) := by
    intro hboth
    rcases hboth with ⟨⟨i, hi⟩, ⟨j, hj⟩⟩
    -- each side contributes at least Jlog 1
    let fD : Fin d → ℝ := fun k => Cost.Jlog ((dΔ k : ℤ) : ℝ)
    let fC : Fin d → ℝ := fun k => Cost.Jlog ((cΔ k : ℤ) : ℝ)
    have hDi : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fD k := by
      -- `fD i = Jlog 1` and all terms nonneg
      have hnonneg : ∀ k : Fin d, 0 ≤ fD k := fun _ => Cost.Jlog_nonneg _
      have : fD i ≤ ∑ k : Fin d, fD k := by
        have : fD i ≤ Finset.sum (Finset.univ : Finset (Fin d)) fD :=
          Finset.single_le_sum (by
            intro k hk; exact hnonneg k) (by simp : i ∈ (Finset.univ : Finset (Fin d)))
        simpa using this
      have : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fD k := by
        simpa [fD, hi] using this
      exact this
    have hCj : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fC k := by
      have hnonneg : ∀ k : Fin d, 0 ≤ fC k := fun _ => Cost.Jlog_nonneg _
      have : fC j ≤ ∑ k : Fin d, fC k := by
        have : fC j ≤ Finset.sum (Finset.univ : Finset (Fin d)) fC :=
          Finset.single_le_sum (by
            intro k hk; exact hnonneg k) (by simp : j ∈ (Finset.univ : Finset (Fin d)))
        simpa using this
      have : Cost.Jlog (1 : ℝ) ≤ ∑ k : Fin d, fC k := by
        simpa [fC, hj] using this
      exact this
    -- so total cost ≥ 2*Jlog1
    have hcost_ge :
        Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
      -- debitSum + creditSum
      dsimp [ledgerJlogCost, dΔ, cΔ]
      exact add_le_add hDi hCj
    have hlt : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
      have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
      exact lt_of_lt_of_le this hcost_ge
    exact (not_lt_of_ge hle) hlt

  -- Choose which side has the unique 1.
  cases hex1 with
  | inl hd =>
      rcases hd with ⟨k, hk⟩
      have : ¬ (∃ j : Fin d, cΔ j = 1) := by
        intro hc
        exact not_two_ones ⟨⟨k, hk⟩, hc⟩
      -- all credit deltas are 0
      have hcAll0 : ∀ j : Fin d, cΔ j = 0 := by
        intro j
        have hn1 : ¬ cΔ j = 1 := by
          intro hj
          exact this ⟨j, hj⟩
        cases hc01 j with
        | inl hz => exact hz
        | inr h1 => exact (hn1 h1).elim
      -- all debit deltas are 0 except at k
      have hdAll : ∀ j : Fin d, j ≠ k → dΔ j = 0 := by
        intro j hjk
        have hn1 : ¬ dΔ j = 1 := by
          intro hj1
          -- two debit ones would force cost > Jlog 1 similarly (simpler: use L1 minimality lemma later)
          -- We can derive contradiction by comparing debitSum with two Jlog1 terms.
          let fD : Fin d → ℝ := fun t => Cost.Jlog ((dΔ t : ℤ) : ℝ)
          have hnonneg : ∀ t : Fin d, 0 ≤ fD t := fun _ => Cost.Jlog_nonneg _
          have hi : fD k = Cost.Jlog (1 : ℝ) := by simpa [fD, hk]
          have hj : fD j = Cost.Jlog (1 : ℝ) := by simpa [fD, hj1]
          -- show debitSum ≥ fD k + fD j
          have hsplit :=
            (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := fD) (a := k) (by simp))
          have hjmem : j ∈ (Finset.univ.erase k : Finset (Fin d)) := by simp [hjk]
          have hj_le_rest :
              fD j ≤ Finset.sum (Finset.univ.erase k : Finset (Fin d)) fD := by
            exact Finset.single_le_sum (by
              intro t ht; exact hnonneg t) hjmem
          have hdebit_ge :
              Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ∑ t : Fin d, fD t := by
            -- rewrite sum and use `hj_le_rest`
            calc
              Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ)
                  = fD k + fD j := by simp [hi, hj]
              _ ≤ fD k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) fD := by
                    linarith
              _ = ∑ t : Fin d, fD t := by simpa using hsplit.symm
          -- total cost ≥ debitSum
          have hcredit_nonneg : 0 ≤ ∑ t : Fin d, Cost.Jlog ((cΔ t : ℤ) : ℝ) :=
            Finset.sum_nonneg (fun _ _ => Cost.Jlog_nonneg _)
          have hcost_ge : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) ≤ ledgerJlogCost (d := d) L L' := by
            dsimp [ledgerJlogCost, dΔ, cΔ]
            exact le_trans (le_trans hdebit_ge (le_add_of_nonneg_right hcredit_nonneg)) (le_rfl)
          have : Cost.Jlog (1 : ℝ) < ledgerJlogCost (d := d) L L' := by
            have : Cost.Jlog (1 : ℝ) + Cost.Jlog (1 : ℝ) > Cost.Jlog (1 : ℝ) := by linarith
            exact lt_of_lt_of_le this hcost_ge
          exact (not_lt_of_ge hle) this
        cases hd01 j with
        | inl hz => exact hz
        | inr h1 => exact (hn1 h1).elim
      -- now show L' = post L k debit
      refine ⟨k, Side.debit, ?_⟩
      cases L with
      | mk debit credit =>
        cases L' with
        | mk debit' credit' =>
          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
              have hdiff : debit' i - debit i = 1 := by simpa [dΔ] using hk
              have : debit' i = debit

-- … truncated for the page; open the module for the rest.
MODEL ledgerJlogCost · IndisputableMonolith/LedgerPostingAdjacency.lean
ledgerJlogCost · IndisputableMonolith/LedgerPostingAdjacency.lean:168 
/-- A Jlog-based step cost over integer ledger deltas (cast to ℝ). -/
noncomputable def ledgerJlogCost {d : Nat} (L L' : LedgerState d) : ℝ :=
  (∑ i : Fin d, Cost.Jlog ((L'.debit i - L.debit i : ℤ) : ℝ)) +
  (∑ i : Fin d, Cost.Jlog ((L'.credit i - L.credit i : ℤ) : ℝ))
MODEL PostingStep · IndisputableMonolith/LedgerPostingAdjacency.lean
PostingStep · IndisputableMonolith/LedgerPostingAdjacency.lean:142 
/-- One atomic posting step between ledger states. -/
def PostingStep {d : Nat} (L L' : LedgerState d) : Prop :=
  ∃ k : Fin d, ∃ side : Side, L' = post L k side

What this page does not claim

The theorem does not claim that nature must use this posting model; that is a separate open bridge step. The theorem does not claim that any monotone transition with cost at most J(1) is a posting step under any cost function other than the framework's forced J cost. The theorem does not claim that the cost of a posting step is always J(1); that is a separate lemma.

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