past_addressable_at
plain-language theorem explainer
After a field commit at voxel v, every past index i of that voxel still reads the same optional entry as before the write. Cap3 and multi-voxel ledger certificates cite this for address-stable readout. The proof rewrites the written voxel via the self-commit identity, then applies single-carrier past addressability.
Claim. Let $F : V \to \mathrm{List}\, E$ be a recognition field, $v \in V$, $e \in E$, and $i \in \mathbb{N}$ with $i < |F(v)|$. Writing $F' = \mathrm{commitAt}(F,v,e)$ for the field after appending $e$ at $v$, one has $F'(v)[i]? = F(v)[i]?$.
background
Module Foundation.LedgerField lifts single-carrier append-only time from LedgerTime to a spatial index. A recognition field is LedgerField V E := V → List E: each voxel carries an independent committed history. Field commit commitAt F v e updates only voxel v by the single-list commit, leaving every other voxel untouched.
Single-voxel past addressability (from LedgerTime) already says that for a list ledger L, index i < |L|, and new entry e, the optional readout (commit L e)[i]? equals L[i]?. The field-level self identity commitAt_self states that evaluating the committed field at the written voxel recovers exactly that single-list commit: commitAt F v e v = commit (F v) e.
Together these give address-stable readout at field scale: past indices at the written voxel remain readable and unchanged after the append. The module packages this with locality, past immutability, and write-head advance as the multi-voxel keystone for Cap3.
proof idea
Two-step term proof. First rewrite the left-hand side with commitAt_self, replacing (commitAt F v e) v by the single-voxel commit commit (F v) e. The goal becomes the single-carrier statement (commit (F v) e)[i]? = (F v)[i]? under i < (F v).length. Discharge it by exact past_addressable (F v) e i hi. No induction or case split; pure transport of the list lemma across the field update at the written voxel.
why it matters
This is one of the five multi-voxel keystone theorems listed in the module doc (with commitAt_local, past_immutable_at, writeHeadAt_advances, writeHeadAt_other). Downstream, fieldLedgerCert packages them into the structure FieldLedgerCert, wiring addressable := fun F v e i hi => past_addressable_at F v e i hi.
In the Recognition framework the field type is the Cap3 substrate: independent append-only ledgers on voxels, with no cross-voxel edits and an immutable, addressable past. Hub content-emptiness (c3_l03) and the field-level widening cone (c3_l04) build on this type. The result is axiom-clean as a pure list/function fact; identifying V with physical voxels and E with recognition entries is model content argued in the companion paper, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.