FieldLedgerCert
plain-language theorem explainer
Packages five universal properties of multi-voxel recognition fields: local commits, immutable past, write-head advance only at the written voxel, and address-stable readout. Cap3 field-ledger arguments cite this certificate rather than the five lemmas separately. It is a Prop structure (definition), witnessed later by assembling the single-voxel lifts.
Claim. A multi-voxel ledger certificate is the conjunction of: for every field $F:V\to\mathrm{List}\,E$, voxel $v$, and entry $e$, (i) $w\neq v$ implies the commit at $v$ leaves $F(w)$ unchanged; (ii) truncating the committed ledger at $v$ to its old length recovers $F(v)$; (iii) the write-head at $v$ increases by exactly one; (iv) the write-head at every $w\neq v$ is unchanged; (v) every index $i$ already in the past of $v$ still reads the same entry after the commit.
background
Recognition time for a single carrier is an append-only list (LedgerTime). At field scale one needs an independent ledger per spatial voxel: a recognition field is a map $F:V\to\mathrm{List},E$. The commit operation commitAt updates only voxel $v$ by appending $e$, via function update, and leaves every other voxel untouched.
The per-voxel write-head is the present index of that voxel's list. Single-voxel past immutability already says that truncating a committed list back to its old length recovers the old list exactly (past_immutable: "committing a new entry cannot alter the past"). This module lifts that fact, together with locality and head-motion, to the field.
The certificate is the multi-voxel keystone named in the module doc: locality (no cross-voxel edits), immutable addressable past, and a write-head that advances by one only at the written voxel.
proof idea
No proof body: this is a structure of type Prop whose five fields are the universal statements above. The concrete witness is the downstream theorem fieldLedgerCert, which fills each field by applying the corresponding lifted lemma (commitAt_local, past_immutable_at, writeHeadAt_advances, writeHeadAt_other, past_addressable_at). Those lemmas themselves reduce to the single-voxel LedgerTime facts plus Function.update case splits on voxel equality.
why it matters
This is the packaged interface for Cap3's multi-voxel ledger layer. Downstream, fieldLedgerCert is the single theorem that discharges the whole certificate, so later Cap3 material can depend on one object rather than five separate lemmas.
The module doc places it as the multi-voxel keystone for Cap3: hub content-emptiness (c3_l03) and the field-level widening cone (c3_l04) build on this type. It is the field-scale lift of LedgerTime's append-only discipline (past immutability and unit head advance), which underwrites recognition time as an ordered, non-rewritable record across space.
Status is definitional and axiom-clean; identifying $V$ with physical voxels and $E$ with 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.