past_immutable_at
plain-language theorem explainer
Committing a new entry at voxel v leaves the already-committed history of v unchanged: the prefix of the updated ledger of the old length equals the old ledger. Field-level Cap3 arguments and the FieldLedgerCert bundle cite this as the multi-voxel lift of single-carrier past immutability. The proof is a two-line reduction via commitAt_self into the single-voxel past_immutable lemma.
Claim. Let $F$ be a recognition field on voxels $V$ with entries $E$, and fix a voxel $v$ and entry $e$. After committing $e$ at $v$, the prefix of the updated ledger at $v$ of length equal to the old ledger length equals the old ledger at $v$: $\mathrm{take}((F'\,v),\,|F\,v|)=F\,v$, where $F'$ is the field after the commit.
background
A recognition field is an assignment of an independent append-only ledger to each spatial voxel: $\mathrm{LedgerField},V,E := V \to \mathrm{List},E$. The single-carrier theory in LedgerTime already treats one list as an append-only recognition history; this module lifts that structure to many voxels so time-addressing works at field scale.
Field commit commitAt F v e updates only voxel $v$ by appending $e$ to $F,v$, leaving every other voxel untouched. The sibling identity commitAt_self records that the value at the written voxel after commit is exactly the single-voxel commit of the old list. Upstream, single-voxel past immutability states that truncating a committed list back to its pre-commit length recovers the old list.
The local setting is the multi-voxel keystone for Cap3: locality of writes, immutability of each voxel's past, write-head advance, and address-stable readout of committed indices. Identifying $V$ with physical voxels and $E$ with recognition entries is model content argued in the companion paper, not in this module.
proof idea
Term-mode, two steps. First rewrite the left-hand side with commitAt_self, which replaces the field evaluation after commit by the ordinary single-voxel commit of $F,v$. The goal collapses to the single-carrier statement that taking the prefix of length $|F,v|$ after appending $e$ recovers $F,v$. Discharge that by applying past_immutable from LedgerTime to the list $F,v$ and entry $e$. No induction or case split is needed; the field theorem is a pure lift of the list theorem through the update-at-$v$ identity.
why it matters
This is one of the five field-level theorems the module advertises as the multi-voxel keystone for Cap3. Downstream, fieldLedgerCert packages it as the past_immutable field of FieldLedgerCert, alongside local write, head advance, head-other, and addressability. Without past immutability at each voxel, committed recognition history could be rewritten by later commits, breaking append-only time and any readout that addresses past ticks by index.
In the broader Recognition framework this supports the ledger picture of recognition time: once an entry is committed at a voxel, later local writes only extend the list. The hub content-emptiness (c3_l03) and field-level widening cone (c3_l04) build on this type and its cert bundle. The result is axiom-clean as a pure list/function fact; physical identification of voxels remains external model content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.