Foundation Ledger Time

The ledger's arrow of time

Time, as we experience it, has a direction: the past is fixed, the future is open. Recognition Science starts from a bare tick, an invertible unit of recognition that is itself time-symmetric. The asymmetry enters with the ledger, a discrete record of events that can only be appended to, never changed in place. This structure is formalized abstractly over any entry type, proving the structural facts about such a record.

The core definitions are simple. A ledger is a list of entries. commit appends a new entry to the end. The writeHead is the index of the present, the number of entries committed so far. Three theorems establish the essential properties. First, past_immutable: truncating the extended ledger back to its old length returns the old ledger exactly, so committing a new entry cannot alter the past. Second, past_addressable: every committed past index reads the same value after a new commit, so the past is read-only and addressable by index. Third, writeHead_advances: the present index moves forward by exactly one per commit.

The future side is captured by the admissible future cone, the set of possible continuations from a given frontier. The construction defines coneStep, which takes a frontier and adds all its admissible successors under a given next relation. Two theorems follow directly: cone_grows shows the frontier is contained in its successor cone, and cone_card_monotone shows the count of admissible states is nondecreasing in horizon. Together these state that the cone of possible futures never shrinks as the present advances.

In Recognition Science, the identification of the abstract entry type with recognition events, and of the cone step with the J-admissible continuation set, is a modeling choice argued in the companion paper. The structural facts about lists and finite sets are proved as theorems. This pins down the formal skeleton of an append-only time: a fixed, readable past and a widening, never-contracting future. This is what gives the framework its arrow of time, distinct from the symmetric tick.

/-- **Past immutability.** Truncating the extended ledger back to the old length
returns the old ledger exactly: committing a new entry cannot alter the past.

Strategy: `unfold commit; exact List.take_left l [e]` (or
`simp [commit, List.take_left]`). -/
theorem past_immutable (l : List E) (e : E) :
    (commit l e).take l.length = l := by
  unfold commit; simp

/-- **Past addressability.** Every committed past index reads the same value after
a new commit: the past is read-only and addressable by index.

Strategy: `unfold commit; exact List.getElem?_append_left hi` (find the exact
`getElem?_append` lemma for the index-in-left-segment case via the premises). -/
theorem past_addressable (l : List E) (e : E) (i : ℕ) (hi : i < l.length) :
    (commit l e)[i]? = l[i]? := by
  unfold commit; rw [List.getElem?_append_left hi]

/-- **Write-head advance.** The present index moves forward by exactly one per
commit.

Strategy: `simp [writeHead, commit, List.length_append]`. -/
theorem writeHead_advances (l : List E) (e : E) :
    writeHead (commit l e) = writeHead l + 1 := by
  unfold writeHead commit; simp

/-- **Admissible count nondecreasing.** The number of admissible states is
nondecreasing in horizon.

Strategy: `exact Finset.card_le_card (cone_grows next S)`. -/
theorem cone_card_monotone (next : E → Finset E) (S : Finset E) :
    S.card ≤ (coneStep next S).card := by
  exact Finset.card_le_card (cone_grows next S)

/-- One step of the admissible future cone: the current frontier together with all
its admissible successors under `next`. -/
def coneStep (next : E → Finset E) (S : Finset E) : Finset E :=
  S ∪ S.biUnion next

What this page does not claim

The module does not prove that the future cone is strictly expanding, only that it never shrinks. The module does not identify the entry type with any specific physical quantity; that is a modeling choice. The module does not derive the arrow of time from the tick alone; the asymmetry is introduced by the ledger.

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/Foundation/LedgerTime.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: