commitAt_self
plain-language theorem explainer
After committing entry e at voxel v of a recognition field F, the field value at v equals the ordinary single-voxel append of e onto F(v). Anyone lifting LedgerTime lemmas to the multi-voxel field cites this reduction. The proof unfolds the pointwise update definition and applies Function.update_self.
Claim. For a recognition field $F : V \to \mathrm{List}\, E$, a voxel $v \in V$, and an entry $e \in E$, evaluating the field-level commit at the written voxel recovers the single-voxel commit: $(\mathrm{commitAt}\, F\, v\, e)(v) = \mathrm{commit}(F(v), e)$.
background
A recognition field assigns an independent append-only ledger to each voxel of a spatial index: $\mathrm{LedgerField}, V, E := V \to \mathrm{List}, E$. The single-voxel primitive $\mathrm{commit}, l, e := l \mathbin{++} [e]$ appends one entry. Field-level commit is the pointwise lift $\mathrm{commitAt}, F, v, e := \mathrm{Function.update}, F, v, (\mathrm{commit}, (F, v), e)$, so only voxel $v$ changes.
The module Foundation.LedgerField lifts the single-carrier append-only structure of Foundation.LedgerTime to this multi-voxel setting. Locality (writes at one voxel leave others untouched) and past immutability are the multi-voxel keystones for Cap3; both need a clean reduction from field evaluation at the written voxel back to ordinary list commit.
Function.update is the standard pointwise override on a function type. Its self-evaluation identity is the only library fact required here.
proof idea
One-line reduction. Unfold commitAt to expose Function.update F v (commit (F v) e), then rewrite by Function.update_self, which states that updating a function at $v$ and evaluating at $v$ returns the new value. No induction and no ledger-specific lemmas.
why it matters
This is the bridge that lets every single-voxel LedgerTime theorem transport to the written voxel of a field. Three immediate parents rewrite through it: past_immutable_at (truncating the written voxel after commit recovers the old ledger), writeHeadAt_advances (the present index at $v$ grows by one), and past_addressable_at (every prior index at $v$ still reads the same entry).
Together those theorems are the multi-voxel keystone listed in the module doc for Cap3: field past is immutable and address-stable, and the write-head advances only at the written voxel. The hub content-emptiness certificate and the field-level widening cone build on this type. The result is model-only in identifying $V$ with physical voxels and $E$ with recognition entries; the Lean statement itself is axiom-clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.