commitAt_local
plain-language theorem explainer
A field-level commit at voxel v leaves every other voxel w unchanged: the post-commit field agrees with the original field at w. Anyone formalizing multi-voxel recognition ledgers or Cap3 locality cites this. The proof unfolds the commit as a pointwise function update and applies the standard off-diagonal update identity.
Claim. Let $F$ be a recognition field on voxels $V$ with entries $E$, i.e. $F : V \to \mathrm{List}\, E$. For any voxels $v,w \in V$ with $w \neq v$ and any entry $e \in E$, the field obtained by committing $e$ at $v$ satisfies $(\mathrm{commit}_v e\, F)(w) = F(w)$.
background
A recognition field is the multi-voxel lift of the single-carrier append-only ledger from LedgerTime: LedgerField V E := V → List E, one independent committed history per spatial index. Single-voxel time is a list of entries; field scale assigns such a list to every voxel.
The field commit commitAt F v e is defined as Function.update F v (commit (F v) e), where single-voxel commit is list append l ++ [e]. Only the ledger at v grows; the definition is built so other voxels are untouched. The module states this as the multi-voxel keystone for Cap3: locality means a write at one voxel does not edit another.
Upstream, commit is the append-only operation on one carrier. The spatial types V and E are parameters here (model identification with physical voxels and recognition entries is external). Decidable equality on V is assumed so pointwise update is well-defined.
proof idea
Term-style tactic proof in two steps. Unfold commitAt to expose Function.update F v (commit (F v) e). Then rewrite with Function.update_of_ne hw: for w ≠ v, update at v evaluates to the original function value at w. No induction or ledger algebra is needed; locality is exactly the off-support clause of function update.
why it matters
This is the first listed multi-voxel keystone theorem in LedgerField: locality / no spooky cross-voxel edits. It is wired directly into the certificate bundle fieldLedgerCert as the local_write field, packaging Cap3 ledger laws at field scale.
Downstream, writeHeadAt_other rewrites through this lemma: after a commit at v, the write-head (present index) at every other voxel is unchanged, because the underlying list at that voxel is unchanged. Together with past-immutability, head-advance, and addressability, it lifts single-voxel LedgerTime structure to an independent ledger per voxel.
In the Recognition framework this underwrites field-level append-only time without nonlocal ledger mutation. The hub content-emptiness (c3_l03) and field-level widening cone (c3_l04) build on this type. Status is axiom-clean theorem; only the physical reading of V and E is model-side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.