FieldTimeCert
plain-language theorem explainer
Packages two field-level time axioms as a single Prop: the hub is content-empty at every write-head (no future value to retrieve), and the multi-voxel admissible cone never shrinks under one cone step. Anyone citing Cap3 c3_l03/c3_l04 or the field-time certificate will use this structure. It is a pure Prop bundle; the inhabiting theorem wires the two proved lemmas.
Claim. A field-time certificate is a proposition asserting (i) for every recognition field $F:V\to\mathrm{List}\,E$ and voxel $v$, the entry at the present write-head of $F$ at $v$ is absent ($\mathrm{none}$), and (ii) for every successor map $\mathrm{next}$, per-voxel frontier $S$, and finite voxel set $vs$, the summed admissible-continuation count over $vs$ is nondecreasing after one cone step at each voxel.
background
A recognition field (LedgerField V E) is an independent append-only ledger at each voxel: a map $V\to\mathrm{List},E$. The per-voxel write-head is the present index of that list; reading at the write-head is the open frontier. Module context (Cap3): the hub is address-complete but content-empty for a single carrier, so no committed future value exists to retrieve.
The single-carrier admissible cone is advanced by coneStep: the frontier union all admissible successors under a relation next. The field-level cone count fieldConeCard sums per-voxel frontier cardinalities over a finite voxel set. Upstream, the single-carrier cone never shrinks; the field lift asserts the summed count is nondecreasing under one simultaneous cone step at every voxel.
Status in the module is theorem-level and axiom-clean once the two component facts are proved; the physical reading of $V$/$E$ as voxels and recognition entries is model-only.
proof idea
No proof body: this is a structure definition packaging two fields of type Prop. The first field is the universal statement of hub content-emptiness (read at write-head yields none). The second is the universal inequality that fieldConeCard after coneStep on every voxel is at least the prior card. Inhabitation is deferred to the sibling theorem fieldTimeCert, which fills the fields by hub_content_empty and fieldCone_card_monotone.
why it matters
This is the Cap3 field-time certificate type: it names the conjunction of hub content-emptiness (c3_l03) and field-level cone widening (c3_l04). Downstream, fieldTimeCert constructs the unique interesting inhabitant by wiring those two lemmas, so any later argument that needs "time does not leak future content and the future cone only widens" can take a FieldTimeCert hypothesis or cite the global instance.
In the Recognition ledger picture this blocks naive time-travel readings: addressing is total, content at the frontier is unwritten, and admissible futures expand rather than contract. It sits in Foundation above LedgerField and LedgerTime, and is the field-level counterpart of the single-carrier monotone cone. No forcing-chain (T0–T8) step is discharged here; the role is structural hygiene for multi-voxel time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.