Foundation Ledger Time Write Head

The write-head

A ledger, in the plainest sense, is a discrete record of events that can only be appended to. The write-head is the index of the present moment in that record: the number of entries committed so far. In the Recognition Science framework, this is not a metaphor stretched into a slogan. It is a formal definition, written as a function that takes a list of entries and returns its length. The framework's machine-checked library of formal theorems then proves three structural facts about this object.

First, committing a new entry advances the write-head by exactly one. If the ledger held n entries before, it holds n plus one after. Second, the past is immutable: truncating the extended ledger back to its old length returns the old ledger exactly, and every old index reads the same value after a new commit. The past is read-only and addressable. Third, the set of admissible future continuations never shrinks. The count of possible next states is nondecreasing in horizon, so the future cone widens or holds steady; it never closes in.

The bare recognition tick, the framework's atomic unit of time, is invertible and therefore time-symmetric. The lived asymmetry between a fixed, readable past and an open, widening future is not in the tick itself. It enters with the ledger. That is the conceptual payload of the write-head: it is the point where time's symmetry breaks, not by decree but by the simple act of appending to a record. The past is what has been written; the future is what remains admissible.

In Recognition Science, the structural facts above are theorems, proved in the framework's library. The identification of the ledger's entries with recognition events, and of the admissible continuation set with the J-cost continuation set, is a modeling choice argued in the companion paper, not a theorem. The write-head establishes the architecture of time as an append-only record; it does not establish what counts as an admissible continuation, nor why the cost function takes the specific form it does.

/-- The write-head index (the present): the number of committed entries. -/
def writeHead (l : List E) : ℕ := l.length

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

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

What this page does not claim

The write-head does not determine what constitutes an admissible future continuation. The write-head does not derive the specific form of the J-cost function. The identification of ledger entries with recognition events is a modeling choice, not a theorem.

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: