Foundation Ledger Time Write Head Advances

The advancing write-head

In the Recognition Science framework, a ledger, a discrete record of committed events, is what turns reversible recognition ticks into the one-way time we experience. The declaration writeHead_advances states the core structural fact: each time a new entry is committed, the present index, the number of committed entries, moves forward by exactly one. If the ledger holds five entries and you append a sixth, the write-head reads six, never five again, and never seven in one step.

This is a theorem about lists, not about physics. The framework's machine-checked library of formal theorems proves it by unfolding the definitions: committing an entry appends it to the end of the list, and the write-head is simply the list's length. The proof is a short calculation with list append, and the result is tagged THEOREM because it is axiom-clean and kernel-checked. Two companion theorems, past_immutable and past_addressable, complete the picture: truncating the extended ledger back to its old length returns the old ledger exactly, and every past index reads the same value after a new commit. The past is fixed and readable; the write-head only advances.

The framework models the admissible future as a cone that never shrinks. The declaration cone_grows proves that the current frontier is contained in its successor cone, and cone_card_monotone proves the count of admissible continuations is nondecreasing in horizon. Together these state that as the write-head advances, the set of possible futures does not contract: the past closes, the future widens.

What writeHead_advances does not claim is the identification of the ledger's entries with actual recognition events. That identification, and the choice of which continuations count as admissible, is a MODEL, argued in the companion paper and not proved here. The theorem is purely structural: it holds for any list of entries, whatever those entries mean. The framework's claim is that this append-only structure, with its immutable past and growing future cone, is the right formal skeleton for the asymmetry of lived time; the theorem itself only guarantees the skeleton is consistent.

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

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

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

/-- Commit a new entry to the ledger: append-only. -/
def commit (l : List E) (e : E) : List E := l ++ [e]

What this page does not claim

The theorem does not prove that time itself is asymmetric in the physical world. The theorem does not define which events are admissible continuations. The theorem does not identify the entry type E with any specific physical quantity.

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: