writeHead
plain-language theorem explainer
The write-head is the present index on an append-only recognition ledger: the number of committed entries. Anyone proving past immutability, head advance, or per-voxel field locality cites it as the clock. It is a one-line alias of list length, not a derived theorem.
Claim. For a ledger $\ell$ given as a finite list of entries of type $E$, the write-head (present index) is $w(\ell) := |\ell|$.
background
LedgerTime isolates the lived arrow of time from the bare recognition tick. The tick itself is invertible and time-symmetric; asymmetry enters only when events are committed to an append-only ledger over an abstract entry type $E$.
The companion operation commit appends a single entry: $\mathrm{commit}(\ell,e)=\ell++[e]$. The write-head is the present cursor on that list. Upstream, length of finite traces in the primitive recognition calculus plays the same counting role for traces; here the count is specialized to the ledger list.
Module status: structural facts about lists and finsets are theorems; identifying $E$ with recognition entries is a modeling claim argued in the companion paper, not in this file.
proof idea
Pure definition: the write-head of a ledger list is exactly its length. No proof obligations; downstream theorems unfold this alias and apply standard list lemmas (List.length_append, List.take_left, List.getElem?_eq_none).
why it matters
This index is the present that every LedgerTime structural fact talks about. writeHead_advances shows it moves by exactly one under commit; past_immutable truncates the extended ledger back to the old head and recovers the old list. Downstream, LedgerField.writeHeadAt lifts it per voxel, and hub_content_empty uses that lift to prove the frontier is unwritten: reading at the present head returns none. In the broader Recognition picture this is the ledger-side clock that makes the fixed past versus open future precise, complementary to the eight-tick octave and the invertible bare tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.