commitAt
plain-language theorem explainer
Field-level write: append one recognition entry to the ledger at a single voxel, leaving every other voxel unchanged. Cap3 locality and past-immutability proofs cite this as the multi-voxel commit primitive. Defined by pointwise Function.update of the single-carrier append at the chosen voxel.
Claim. Let $F$ be a recognition field ($V \to \mathrm{List}\, E$), assigning an independent append-only ledger to each voxel. For $v \in V$ and entry $e$, the field commit at $v$ is the field $F'$ with $F'(v) = F(v)\mathbin{++}[e]$ and $F'(w) = F(w)$ for all $w \neq v$.
background
LedgerTime treats recognition time for one carrier as an append-only list of entries. A field-scale ledger needs the multi-voxel lift: a recognition field is a map $V \to \mathrm{List}, E$, one independent history per spatial index (voxel). The module states this type and lifts single-voxel theorems to it.
The single-carrier commit is ordinary list append: $\mathrm{commit}(l,e) = l \mathbin{++} [e]$. The present (write-head) is the length of the committed list. Field commit is the local lift of that operation: edit only the chosen voxel's list.
Decidable equality on $V$ is assumed so pointwise update is well-defined. Physical identification of $V$ with voxels and $E$ with recognition entries is model content argued in the companion paper, not in this module.
proof idea
Definition, not a proof. Body is one application of Function.update: replace the value of $F$ at $v$ by the single-voxel commit of $e$ onto $F(v)$. All other points of the function are left as in $F$. Downstream locality and self-evaluation lemmas unfold this and apply Function.update_of_ne / Function.update_self.
why it matters
This is the multi-voxel write primitive for Cap3. Every field-level keystone theorem is stated in terms of it: locality (commit at $v$ leaves $w \neq v$ fixed), self-evaluation (at $v$ the field equals the single-carrier commit), past immutability and addressability at the written voxel, and write-head advance by one at $v$ only.
Those facts assemble into the multi-voxel ledger certificate: append-only, local, immutable addressable past, per-voxel head that advances only where written. The hub content-emptiness and field-level widening cone build on this type. Framework-wise it is the field-scale carrier for recognition time, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.