writeHeadAt
plain-language theorem explainer
The present index of a recognition field at a chosen voxel is the length of that voxel's append-only ledger. Anyone proving multi-voxel locality, head advance, or hub emptiness cites this projection. It is a one-line lift of the single-carrier write-head to field scale.
Claim. For a recognition field $F : V \to \mathrm{List}\, E$ and voxel $v \in V$, the per-voxel write-head (present index) is $\mathrm{writeHeadAt}(F,v) := |F(v)|$, the number of committed entries at $v$.
background
Module LedgerField lifts single-carrier recognition time to a spatial index: a recognition field is an assignment $F : V \to \mathrm{List}, E$ of an independent append-only ledger to each voxel. Single-voxel time lives in LedgerTime, where commit appends an entry and the write-head is the present index (length of the committed list).
At field scale one needs the same present index, but parameterized by voxel. The companion single-voxel head is the number of committed entries; this definition simply evaluates the field at $v$ and reads that head. Downstream locality and cone statements treat each voxel's present separately, so the projection must be named before the multi-voxel theorems can state advance-at-$v$ and freeze-elsewhere.
proof idea
Pure definitional abbreviation: apply the single-carrier write-head to the list $F(v)$. No proof obligations; unfolding writeHeadAt reduces goals to ordinary list-length facts about F v.
why it matters
This is the field-level present used by the multi-voxel keystone for Cap3. writeHeadAt_advances states the head moves by one at the written voxel after commitAt; writeHeadAt_other states it is frozen elsewhere. Both feed FieldLedgerCert (append-only, local, immutable addressable past, per-voxel head advance only at the write site).
hub_content_empty and FieldTimeCert read the field at this index and demand none: the frontier is unwritten, so the hub is content-empty at the present. That emptiness underpins the field-level widening cone and the hub content-emptiness claim (c3_l03). Without a named per-voxel present, those certificates cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.