past_addressable
plain-language theorem explainer
After a ledger commit appends one new entry, every previously valid index still returns the same optional value. Formalizations of append-only recognition time and field pasts cite this as the addressability half of past immutability. The proof unfolds the append definition and applies the standard left-segment list lookup lemma.
Claim. Let $\ell$ be a finite list of entries, $e$ a new entry, and $i\in\mathbb{N}$ with $i<|\ell|$. Writing $\mathrm{commit}(\ell,e):=\ell\mathbin{+\mkern-6mu+}[e]$, one has $(\mathrm{commit}(\ell,e))[i]?=\ell[i]?$.
background
LedgerTime isolates the lived past/future asymmetry of recognition from the bare invertible tick. Time symmetry of the tick is broken by an append-only ledger of committed events over an abstract entry type $E$: commits never edit in place, the committed past is immutable and index-addressable, and the admissible future cone is nondecreasing in horizon.
The commit operation is ordinary list append: $\mathrm{commit}(\ell,e)=\ell\mathbin{+\mkern-6mu+}[e]$. The write-head is the length of the committed list (the present). Optional index lookup $\ell[i]?$ returns the entry at $i$ when $i$ is in range and none otherwise. The companion facts in this module are past immutability (same content, not just addressability) and write-head advance by exactly one.
Status is THEOREM for these structural list facts; identifying $E$ with recognition entries is a modeling claim argued in the companion paper, not here.
proof idea
One-line term-style proof. Unfold $\mathrm{commit}$ to expose $\ell\mathbin{+\mkern-6mu+}[e]$, then rewrite by Mathlib's List.getElem?_append_left at the hypothesis $i<|\ell|$, which states that optional lookup into a concatenation at an index still inside the left segment equals lookup in the left list alone.
why it matters
This is the addressability half of the ledger's fixed past: indices already written remain readable at the same values after any later commit. Downstream, past_addressable_at in LedgerField lifts the fact pointwise to a voxel field by rewriting through self-commit and applying this theorem on the fiber list at $v$. Together with past immutability and write-head advance, it supplies the structural backbone for recognition time as an append-only record rather than a reversible tick. The module marks the $E$/cone identification as MODEL; the list lemmas themselves close without scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.