writeHeadAt_other
plain-language theorem explainer
After a field commit at voxel v, the write-head (present index) at every other voxel w is unchanged. Anyone citing multi-voxel locality or the Cap3 field-ledger certificate needs this. The proof unfolds the write-head and rewrites by the locality of commitAt.
Claim. Let $F$ be a recognition field on voxels $V$ with entries $E$. For any voxels $v,w$ with $w \neq v$ and any entry $e$, the write-head of $F$ at $w$ after committing $e$ at $v$ equals the write-head of $F$ at $w$ before the commit.
background
A recognition field is an assignment of an independent append-only ledger to each spatial voxel: LedgerField V E is the function type $V \to \mathrm{List}, E$. Single-carrier append-only time lives in LedgerTime; this module lifts that structure to the multi-voxel setting needed for field-scale addressing.
A field commit at voxel $v$ appends entry $e$ only on $v$, via function update. Locality is already proved as commitAt_local: for $w \neq v$, the ledger at $w$ is literally identical after the commit. The write-head at a voxel is the present index of that voxel's list (its length as the next free slot).
The module's keystone package for Cap3 is locality, past immutability, head advance at the written voxel, head stability elsewhere, and address-stable past readout.
proof idea
One short tactic proof. Unfold the definition of the per-voxel write-head so both sides become a function of the ledger list at $w$. Then rewrite by commitAt_local, which supplies equality of the underlying lists at $w \neq v$ after a commit at $v$. Equality of heads follows immediately.
why it matters
This is the complementary half of write-head dynamics: commits advance the head only at the written voxel and leave every other head fixed. Together with writeHeadAt_advances, commitAt_local, past_immutable_at, and past_addressable_at, it fills the multi-voxel keystone listed in the module doc for Cap3.
Downstream, fieldLedgerCert packages it as the head_other field of FieldLedgerCert, the certificate that a recognition field is a local, append-only, addressable ledger. That certificate is the formal substrate for hub content-emptiness and the field-level widening cone arguments that sit on this type. Model identification of $V$ with physical voxels and $E$ with recognition entries is external; the theorem itself is axiom-clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.