commit
plain-language theorem explainer
Append-only commit of one ledger entry: the new history is the old list with a single terminal event. Anyone formalizing recognition time, past immutability, or per-voxel ledger fields cites this as the primitive write. The body is the standard list append of a singleton.
Claim. Given a finite list $\ell$ of entries of type $E$ and a new entry $e$, the commit operation returns $\ell$ concatenated with the singleton $[e]$. Writes never edit earlier positions; they only extend the record.
background
LedgerTime isolates the lived arrow of time from the bare recognition tick. The tick itself is invertible and time-symmetric; asymmetry enters only when events are recorded in an append-only ledger of committed recognitions.
Over an abstract entry type $E$, a ledger state is a List E. The write-head (present) is the length of that list: the number of already committed entries. Commit is the unique structural write: append one new entry at the end.
The module treats structural list facts as theorems and leaves the identification of $E$ with recognition events (and of future cones with $J$-admissible continuations) as a modeling claim argued in the companion paper, not in this file.
proof idea
Definitional one-liner: commit l e is definitionally l ++ [e]. No tactics or lemmas; downstream proofs unfold this and apply standard Mathlib list facts such as List.getElem?_append_left and length-of-append.
why it matters
This is the sole write primitive for recognition time in the foundation layer. Downstream, past_addressable and past_immutable prove that indices already in the list keep their values after a commit, and writeHead / writeHead_advances show the present moves by exactly one.
LedgerField lifts the same operation pointwise: commitAt updates one voxel via Function.update and this commit, with locality theorems (commitAt_local, writeHeadAt_other) and self-consistency (commitAt_self). Together they encode the fixed readable past versus open future that the module doc contrasts with the invertible bare tick.
In the broader Recognition Science picture this is scaffolding for time emergence and ledger snapshots, not a forcing-chain (T0–T8) step; it supplies the append-only substrate those continuum and mass constructions assume when they speak of committed history.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.