past_immutable
plain-language theorem explainer
Committing a new entry to an append-only ledger leaves every prior entry unchanged: the prefix of the extended list of length equal to the old ledger is exactly the old ledger. Anyone building time asymmetry from a fixed past and open future cites this structural fact. The proof unfolds append and discharges by the standard list take-left identity.
Claim. For any finite list $\ell$ of ledger entries and any new entry $e$, writing $\mathrm{commit}(\ell,e):=\ell\mathbin{+\!+}[e]$, one has $\mathrm{take}(|\ell|,\,\mathrm{commit}(\ell,e))=\ell$. Equivalently, appending cannot rewrite any already-committed position.
background
LedgerTime isolates the append-only record that turns a bare, invertible recognition tick into lived time asymmetry: a fixed readable past versus an open future. Over an abstract entry type $E$, the ledger is an ordinary list; commit is pure append $\ell \mapsto \ell \mathbin{+!+} [e]$, and the write-head (the present index) is just the list length.
The module's structural theorems are standard list and finset facts. Identification of $E$ with recognition events, and of the admissible cone with J-cost continuations, is deferred to the companion paper; here only the ledger algebra is proved.
Upstream, commit is defined as append and writeHead as length. Related notions of present and past appear in TimeEmergence (present snapshot versus committed earlier ticks), but this lemma needs only the list model.
proof idea
Term-mode, two tactics. Unfold the definition of commit to expose list append $\ell \mathbin{+!+} [e]$. Then simp closes the goal via the Mathlib identity that taking the left summand's length after append recovers the left list (List.take_left, equivalently List.take_append_of_le_length at equality). No induction or case split is required.
why it matters
Past immutability is the first half of the ledger's time arrow: commits never edit history. It is lifted pointwise to multi-voxel fields as past_immutable_at (commit at voxel $v$ leaves the past of $v$ fixed), and is one of the five fields of FieldLedgerCert assembled by fieldLedgerCert (local write, past immutable, head advances, head elsewhere unchanged, past addressable).
In the Recognition framework this is the formal content of "the past is fixed": the bare tick is time-symmetric, so asymmetry enters only with the append-only ledger. The module pairs this with write-head advance and nonshrinking future cones; together they underwrite the lived past/future split without touching the forcing chain (T0–T8) or the J-cost law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.