fieldTimeCert
plain-language theorem explainer
Packages the two field-level time facts into one certificate: every voxel ledger is content-empty at its present write-head, and the multi-voxel admissible-continuation count never shrinks under one simultaneous cone step. Cap3 time-structure citations (c3_l03/c3_l04) land here. The proof is a structure instance that wires the two already-proved lemmas.
Claim. A field time certificate holds: for every multi-voxel ledger field $F$ and voxel $v$, the entry of $F(v)$ at its present write-head index is absent ($\mathrm{none}$); and for every finite voxel set, the total admissible-continuation count is nondecreasing when every voxel advances one cone step.
background
This module sits on the multi-voxel ledger (Foundation.LedgerField). Each voxel carries a sequential ledger of recognition entries; the write-head is the next unwritten index. Addressing is total over committed indices, but the open frontier has no committed value.
Hub content-emptiness (Cap3 c3_l03) states that reading a voxel at its own write-head returns nothing: the hub is address-complete yet content-empty at the present, so no future value can be retrieved. The companion fact is the field-level widening cone (Cap3 c3_l04): summing admissible-continuation counts over a finite voxel set yields a nondecreasing total under one cone step at every voxel.
Upstream, single-carrier cone monotonicity is already available; fieldCone_card_monotone lifts it by summing over voxels. The certificate structure simply conjoins emptiness at the frontier with that nondecreasing field cone count.
proof idea
Structure-instance proof with two fields. The content-emptiness field is the function that applies hub_content_empty at each ledger field and voxel (that lemma unfolds the write-head and uses List.getElem?_eq_none at the frontier length). The cone-widens field introduces the parameters and applies fieldCone_card_monotone, which unfolds the field cone cardinality and uses Finset.sum_le_sum with the single-carrier step inequality at each voxel. No new arithmetic.
why it matters
This is the packaged Cap3 time certificate for the multi-voxel ledger: no future retrieval at the hub frontier, and the field future cone widens rather than contracts. Module status is theorem (axiom-clean), with only the identification of abstract $V$/$E$ with physical voxels and recognition entries treated as model-level.
It closes the local Cap3 pair c3_l03/c3_l04 inside Foundation. No downstream consumers are wired yet in the graph; the declaration exists so later time-arrow or causality arguments can cite one Prop rather than two separate lemmas. It does not touch the forcing chain T0–T8, RCL, or constants; it is ledger-time infrastructure under the Recognition composition setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.