writeHead_advances
plain-language theorem explainer
Committing one ledger entry advances the present index by exactly one. Anyone formalizing append-only recognition time or a spatial ledger field cites this as the discrete clock step. The proof unfolds the write-head as list length and commit as singleton append, then simplifies with the length-of-append identity.
Claim. For any finite ledger $l$ of entries of type $E$ and any new entry $e$, if $\mathrm{commit}(l,e)$ denotes the append-only extension $l{+}{+}[e]$ and the write-head is the length of the ledger, then the write-head after commit equals the old write-head plus one: $\mathrm{length}(l{+}{+}[e]) = \mathrm{length}(l)+1$.
background
LedgerTime isolates the lived arrow of time in Recognition Science. The bare recognition tick is invertible and time-symmetric; asymmetry enters only when events are recorded in an append-only ledger. Over an abstract entry type $E$, commit is ordinary list append of a singleton, and the write-head (the present) is defined as the length of the committed list.
The module pairs this clock step with past immutability and past addressability: truncating after a commit recovers the old ledger, and every prior index still reads the same value. Downstream, the same pattern is lifted pointwise to a ledger field on a spatial index set $V$.
Status in the module doc is THEOREM for these structural list facts; identifying $E$ with recognition entries is left to the companion paper model layer.
proof idea
One-line term-style proof. Unfold the definitions of write-head (list length) and commit (append of a singleton). The goal reduces to $\mathrm{length}(l{+}{+}[e])=\mathrm{length}(l)+1$, which simp discharges via the standard Mathlib length-of-append lemma (as the doc-comment strategy notes: simp [writeHead, commit, List.length_append]).
why it matters
This is the discrete present-step for recognition time: each commit moves the write-head forward by one, so the ledger length is a faithful clock. It feeds directly into writeHeadAt_advances in LedgerField, which states the same fact at a fixed voxel $v$: after commitAt, the local write-head at $v$ increases by one (proved by unfolding the pointwise head, rewriting the self-commit, and applying this theorem).
In the framework, the eight-tick octave (T7) and the invertible bare tick sit underneath; the ledger supplies the non-invertible, append-only record that separates a fixed past from an open future. Together with past_immutable, past_addressable, and the nonshrinking future cone lemmas in the same module, it is the structural backbone for any later claim that recognition history is readable and that admissible continuations only grow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.