LedgerField
plain-language theorem explainer
A recognition field assigns an independent append-only ledger (a list of entries) to every voxel of a spatial index. Cap3 and multi-voxel recognition-time arguments cite this type as the field-scale carrier. It is a pure type definition: maps from voxels to lists of entries, lifting the single-carrier ledger of LedgerTime.
Claim. For types $V$ (spatial voxels) and $E$ (recognition entries), a recognition field is a map $F : V \to \mathrm{List}(E)$: each voxel carries its own committed history as an independent append-only list.
background
LedgerTime treats recognition time for a single carrier as one append-only list of entries. Field-scale time addressing needs the multi-voxel lift: an independent ledger at each point of a spatial index $V$.
The module sets LedgerField V E to be exactly that assignment. A field commit appends an entry at one voxel only; other voxels stay untouched. The single-voxel write-head, past-immutability, and addressability facts then lift pointwise.
Upstream, a voxel is the fundamental length quantum in RS-native units ($\ell_0 = 1$). Concrete $V$ and $E$ from geometry modules (e.g. Freudenthal strip vertices/edges, lattice-ball edge sets) are admissible instantiations; the type itself is parametric.
proof idea
Pure type definition, not a theorem. The body is the function space $V \to \mathrm{List}, E$. No tactics, no lemmas: the multi-voxel structure is the pointwise product of single-carrier ledgers. Downstream ops (commitAt, write-head, past readout) are defined by Function.update and the single-voxel commit from LedgerTime.
why it matters
This is the multi-voxel keystone for Cap3. Every field-level theorem in the module is stated on this type: locality of commits (commitAt_local), past immutability at the written voxel (past_immutable_at), write-head advance only at the written voxel, and address-stable past readout (past_addressable_at).
Those facts assemble into FieldLedgerCert, the multi-voxel ledger certificate (append-only, local, immutable addressable past, per-voxel head). The hub content-emptiness step (c3_l03) and the field-level widening cone (c3_l04) build on this carrier.
Status is definitional and axiom-clean. Identifying $V$ with physical voxels and $E$ with recognition entries is a modeling claim argued in the companion paper, not proved here. Ties the single-carrier eight-tick ledger structure up to a spatial field without cross-voxel edits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.