coneStep
plain-language theorem explainer
One step of the admissible future cone: adjoin to a frontier set every admissible successor under a given next-map. Growth and cardinality theorems that encode lived time asymmetry in the ledger cite this construction. The body is the plain Finset union of the frontier with its biUnion under next.
Claim. Given a successor map $n : E \to \mathrm{Finset}\, E$ and a frontier $S \subseteq E$, the one-step admissible cone is $S \cup \bigcup_{s \in S} n(s)$.
background
LedgerTime formalizes recognition time as an append-only ledger over an abstract entry type $E$. The bare recognition tick is invertible and time-symmetric; the lived split between a fixed past and an open future enters with the ledger record of committed events.
Alongside commit, write-head advance, and past immutability, the module introduces an admissible future cone. The successor map $n : E \to \mathrm{Finset}, E$ packages which continuations are allowed from each entry. A frontier $S$ is any finite set of entries; one cone step enlarges $S$ by every $n$-successor of its members.
The module marks the structural Finset facts as theorems and treats the identification of $E$ with recognition entries (and of this step with the $J$-admissible continuation set) as a model claim argued in the companion paper, not here.
proof idea
Definitional, not a proof. The body is the Finset expression $S \cup S.\mathrm{biUnion}, n$: keep every current frontier element and adjoin the union of $n(s)$ over $s \in S$. Downstream growth lemmas unfold this definition and apply standard Finset subset and card inequalities.
why it matters
This is the primitive operator behind the module's cone-never-shrinks facts. Immediately, cone_grows shows $S \subseteq$ one-step cone, and cone_card_monotone lifts that to nondecreasing cardinality (admissible count nondecreasing in horizon).
At field level, fieldCone_card_monotone sums the same step over voxels, and FieldTimeCert packages cone widening with content-empty frontiers as the certificate that field future cones widen and never contract. Together these encode the lived asymmetry of recognition time: past is append-only and immutable; future is an open, nondecreasing cone of admissible continuations. The structural lemmas are standard Finset facts; the physics content is the model identification with $J$-admissible continuations argued outside this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.