writeHeadAt_advances
plain-language theorem explainer
After a field commit at voxel v, the present index (write-head) at v increases by exactly one. Anyone formalizing multi-voxel append-only time or Cap3 field-ledger certificates cites this. The proof reduces to the single-voxel head-advance lemma via the self-update identity for commitAt.
Claim. Let $F$ be a recognition field on voxels $V$ with entries $E$, and fix $v\in V$ and $e\in E$. Writing $e$ at $v$ advances the present index at $v$ by one: $\mathrm{writeHead}((F\text{ with }e\text{ appended at }v)(v))=\mathrm{writeHead}(F(v))+1$.
background
Module Foundation.LedgerField lifts single-carrier append-only time to a spatial field. A recognition field is an assignment $F:V\to\mathrm{List},E$: each voxel carries its own committed history. A field commit at $v$ updates only that voxel by the single-list append, leaving every other voxel untouched.
The per-voxel write-head is the present index of the list at $v$, i.e. the length of the committed history there. Single-voxel time already proves that appending one entry advances that head by one. The field-level statement is the same fact, localized at the written voxel.
Upstream, commitAt_self records that evaluating the updated field at the written voxel recovers the single-voxel commit. The single-carrier lemma writeHead_advances then supplies the numeric $+1$.
proof idea
Unfold the field write-head to the single-list write-head on $F(v)$. Rewrite the committed field at $v$ with commitAt_self, so the left-hand side becomes the write-head of the single-voxel commit of $F(v)$ by $e$. Finish by the upstream single-carrier theorem writeHead_advances applied to that list and entry. Three short steps; no new arithmetic.
why it matters
This is one of the five multi-voxel keystone facts listed in the module doc for Cap3: after a commit, the written voxel's present index moves by exactly one. It is wired directly into fieldLedgerCert as the head_advances field of FieldLedgerCert, alongside locality, past immutability, head-stability on other voxels, and address-stable past readout.
Together these certify that field-scale recognition time remains append-only and local: time ticks only where a write occurs. Downstream hub content-emptiness and the field-level widening cone build on this type. The result is axiom-clean as pure ledger algebra; identifying $V$ and $E$ with physical voxels and 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.