hub_content_empty
plain-language theorem explainer
At any voxel of a recognition field, the entry at the present write-head index is absent: the open frontier holds no committed value. Anyone citing Cap3 hub content-emptiness (address-complete, content-empty) needs this fact. The proof unfolds the write-head definitions and applies list out-of-range lookup at the list length.
Claim. For any recognition field $F : V \to \mathrm{List}\, E$ and any voxel $v \in V$, the list lookup $(F\, v)[\mathrm{writeHead}(F\, v)]?$ equals $\mathsf{none}$. Equivalently, reading the carrier at its own present index returns nothing: the frontier is unwritten.
background
A recognition field is an independent append-only ledger at each voxel: LedgerField V E is the type $V \to \mathrm{List}, E$. The per-voxel write-head is the length of that list (the next free index), exposed as writeHeadAt F v := writeHead (F v). List lookup at an index equal to the length is out of range and returns none.
The module LedgerFieldCone records two field-level facts built on Foundation.LedgerField. The first is hub content-emptiness (Cap3 c3_l03): the hub vantage is address-complete but content-empty for a single carrier. Addressing is total (every committed index is readable), yet the value at the present write-head, the open frontier, is unwritten. There is no committed value at the frontier to retrieve, so no information is transported from the future.
Upstream, writeHead and writeHeadAt supply the present index; le_refl on the native naturals closes the length comparison used by list lookup.
proof idea
Term-mode proof in two steps. Unfold writeHeadAt and writeHead so the goal is list lookup of F v at index equal to its own length. Discharge with List.getElem?_eq_none applied to le_refl _: the index is not strictly less than the length, so the optional get is none.
why it matters
This is the panel's honest restatement of the no-time-travel claim at field level: the hub supplies addressing; a field supplies content; the frontier itself is empty. Downstream, fieldTimeCert packages the fact as the content_empty field of the FieldTimeCert structure, pairing it with field-cone widening (fieldCone_card_monotone). Together they certify that field time is address-complete, content-empty at the present, and non-contracting into the future.
In the Recognition framework this sits under Cap3 ledger-time structure rather than the T0–T8 forcing chain. It is axiom-clean as a theorem on abstract $V$/$E$; physical identification of voxels and entries remains model-level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.