Foundation Ledger Time Past Immutable

The immutable past

A ledger, in the plainest sense, is a discrete record of events that only ever grows: you add new entries at the end, and you never go back to edit or erase an old one. The Recognition Science framework builds its model of time on exactly this structure. Its declaration past_immutable is a machine-checked theorem stating that when you commit a new entry to such a record, truncating the extended record back to its previous length returns the previous record exactly. In symbols, for any record l and any new entry e, the first l.length entries of l ++ [e] are just l. The act of adding cannot alter what is already written.

The theorem is proved in the framework's machine-checked library of formal theorems as a standard fact about lists: appending an element to a list, then taking the prefix of the original length, gives you the original list back. Its companion facts fill out the picture. writeHead_advances shows the present index, the number of committed entries, moves forward by exactly one per commit. past_addressable shows every committed past index reads the same value after a new commit, so the past is read-only and addressable by position. Two further theorems describe the future: the set of admissible continuations never shrinks, and its count is nondecreasing in horizon. Together these form the framework's structural account of why the past feels fixed and the future feels open, even though the bare recognition tick that generates time is itself invertible and symmetric.

In Recognition Science, this is a deliberate modeling choice layered on top of the mathematics. The theorems themselves are structural facts about lists and finite sets, tagged THEOREM. The identification of those lists with recognition entries, and of the continuation set with the J-admissible set from the framework's cost function, is a MODEL, argued in the companion paper rather than proved in the library. The framework does not claim that physical time is literally a list, nor that this structure explains why time flows. It claims something narrower: if you model time as an append-only ledger of committed events, then the immutability of the past and the growth of the future cone follow as formal consequences, checkable line by line.

What this buys is a precise vocabulary for a familiar asymmetry. The framework's starting point, the recognition tick, is time-symmetric; the ledger is where asymmetry enters. By separating the symmetric tick from the append-only record, the framework can state exactly where the arrow of time lives in its account: not in the individual event, but in the structure that accumulates events. The past is not just remembered; it is, in this model, structurally unchangeable, and that is a theorem, not a hope.

/-- **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

/-- **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

/-- **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]

/-- **The cone never shrinks.** The frontier is contained in its successor cone.

Strategy: `unfold coneStep; exact Finset.subset_union_left`. -/
theorem cone_grows (next : E → Finset E) (S : Finset E) :
    S ⊆ coneStep next S := by
  unfold coneStep; exact Finset.subset_union_left

What this page does not claim

The identification of ledger entries with physical recognition events, which is a MODEL argued in the companion paper. That physical time is literally a list or that this structure explains the experience of time passing. That the past is immutable in any metaphysical sense beyond the formal property of the append-only structure.

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: