fieldConeCard
plain-language theorem explainer
Total admissible-continuation count on a multi-voxel ledger field: sum of the sizes of the per-voxel admissible entry sets over a finite voxel collection. Anyone lifting single-carrier cone monotonicity to the field cites this cardinality. It is a plain Finset sum with no proof obligations.
Claim. Given a per-entry successor relation $\mathrm{next}$, a map $S$ sending each voxel to a finite set of admissible entries, and a finite voxel set $vs$, the field-cone cardinality is $\sum_{v \in vs} |S(v)|$.
background
Module LedgerFieldCone sits on the multi-voxel ledger and records two Cap3 field-level facts: hub content-emptiness (addressing is total, content at the write-head frontier is empty) and the field-level widening cone.
At single-carrier level, an admissible cone is the set of entries reachable under a successor relation next. The single-carrier count is nondecreasing under one cone step (LedgerTime.cone_card_monotone). Here $S : V \to \mathrm{Finset}, E$ assigns to each voxel its current admissible set; $vs$ is a finite collection of voxels. The field cone is the disjoint union (as a sum of cardinalities) of those per-voxel cones.
Related counting primitives elsewhere (event counts, lattice edge sets, PRC step extensions) play the same role of tallying finite admissible structure; this definition is the field-level tally used by the widening theorem.
proof idea
Definition only: unfold to the Finset sum $\sum_{v \in vs} (S, v).\mathrm{card}$. No lemmas, no tactics, no hypotheses beyond DecidableEq on the entry type for Finset operations downstream.
why it matters
Supplies the numeric measure for Cap3 c3_l04 (field-level widening cone). Downstream, fieldCone_card_monotone states that this count is nondecreasing when every voxel advances one cone step: the field future cone never shrinks. That inequality is the second conjunct of FieldTimeCert, which packages hub content-emptiness with cone widening as the field-level time certificate (no future retrieval; future options only grow).
Together these close the panel restatement that time on the ledger field is one-way at the content level. Status is theorem-clean once the monotone lift is proved; the model identification of $V$/$E$ with physical voxels remains interpretive only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.