cone_grows
plain-language theorem explainer
The admissible future cone is expansive: any frontier set of ledger entries sits inside the one-step cone formed by adjoining all admissible successors. Anyone formalizing append-only recognition time or monotone horizon growth cites this. The proof is a one-line unfold of the cone step plus the left-union subset law on finite sets.
Claim. For any successor map $\mathrm{next}:E\to\mathrm{Finset}\,E$ and any finite frontier $S\subseteq E$, one has $S\subseteq S\cup\bigcup_{s\in S}\mathrm{next}(s)$. Equivalently, the current frontier is contained in its one-step admissible future cone.
background
LedgerTime isolates the append-only ledger that breaks the bare tick's time symmetry: a fixed readable past versus an open future. Over an abstract entry type $E$, commits never edit in place; the write-head advances by one; and the admissible future is tracked by a cone operator.
The one-step cone is defined by adjoining every admissible successor of the current frontier: $\mathrm{coneStep}(\mathrm{next},S):=S\cup S.\mathrm{biUnion},\mathrm{next}$. Here $\mathrm{next}$ packages whatever admissibility predicate the model supplies (J-admissible continuations in the companion paper; a pure structural map in this module).
The module status note is explicit: the structural facts are ordinary finset lemmas (THEOREM), while identifying $E$ and $\mathrm{coneStep}$ with recognition entries and J-admissible sets is MODEL content argued off-Lean.
proof idea
One-line term proof. Unfold the definition of the cone step to $S\cup S.\mathrm{biUnion},\mathrm{next}$, then apply the standard library fact $\mathrm{Finset.subset_union_left}$, which states $A\subseteq A\cup B$ for finite sets. No induction and no properties of $\mathrm{next}$ are required.
why it matters
This is the set-inclusion half of the module's claim that "the admissible future cone never shrinks." Its sole recorded consumer is $\mathrm{cone_card_monotone}$, which lifts the inclusion to a cardinality inequality via $\mathrm{Finset.card_le_card}$: the number of admissible states is nondecreasing in horizon.
In the Recognition framework this underwrites the lived arrow of time as a ledger phenomenon rather than a property of the bare tick. It sits beside $\mathrm{past_immutable}$ and $\mathrm{writeHead_advances}$ as structural scaffolding for append-only recognition time; the forcing chain landmarks (T5–T8, RCL, eight-tick octave) are not invoked here, and the J-admissible reading of $\mathrm{next}$ remains a model identification outside this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.