fieldLedgerCert
plain-language theorem explainer
Packages the five multi-voxel ledger laws (locality, past immutability, head advance at the written voxel, head freeze elsewhere, and address-stable past readout) into one certificate proposition. Anyone citing the field-level append-only ledger as a Cap3 keystone points here. The proof is a pure structure inhabitant: each field is discharged by the matching per-voxel lift lemma.
Claim. There exists a multi-voxel ledger certificate: for every spatial index $V$ (with decidable equality), entry type $E$, field $F : V \to \mathrm{List}\, E$, voxel $v$, and entry $e$, (i) a commit at $v$ leaves every $w \neq v$ unchanged; (ii) the committed past of $v$ is immutable under that commit; (iii) the write-head at $v$ advances by exactly one; (iv) the write-head at every other voxel is unchanged; (v) every previously committed index at $v$ still reads the same value after the commit.
background
Foundation.LedgerTime treats recognition time as a single append-only list. At field scale one needs an independent ledger per spatial voxel: a recognition field is simply $F : V \to \mathrm{List}, E$. The commit operation commitAt appends an entry at one chosen voxel via function update and leaves every other voxel untouched.
The single-voxel laws (past immutability, write-head advance, addressable past) lift pointwise. Locality is the genuinely new field-level fact: a write at $v$ cannot edit $w \neq v$. The certificate structure bundles these five universal statements into one Prop so downstream Cap3 material can assume the whole package at once.
Upstream, commitAt_local is the locality theorem ("a commit at voxel $v$ leaves every other voxel $w \neq v$ exactly as it was"); past_immutable_at, writeHeadAt_advances, writeHeadAt_other, and past_addressable_at are the corresponding field lifts of the single-carrier lemmas from LedgerTime.
proof idea
Term-mode structure construction. Each of the five fields of FieldLedgerCert is filled by eta-expanding the matching theorem already proved in this module:
local_write←commitAt_localpast_immutable←past_immutable_athead_advances←writeHeadAt_advanceshead_other←writeHeadAt_otheraddressable←past_addressable_at
No new reasoning: pure packaging of the five lifts into one certificate inhabitant.
why it matters
Module doc calls this the multi-voxel keystone for Cap3. The certificate is the single named Prop that asserts the field ledger is append-only, local (no spooky cross-voxel edits), with an immutable addressable past and a per-voxel write-head that advances only at the written site. Hub content-emptiness (c3_l03) and the field-level widening cone (c3_l04) are stated to build on this type.
In the Recognition framework this is the formal bridge from single-carrier recognition time to a spatially indexed field of ledgers, the setting in which continuum and continuum-limit arguments later sit. Status is axiom-clean theorem; identifying $V$ with physical voxels and $E$ with recognition entries remains a modeling step argued in the companion paper, not here. No downstream Lean users are recorded yet; the certificate is the export surface for those Cap3 developments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.