cone_card_monotone
plain-language theorem explainer
The cardinality of an admissible frontier is nondecreasing under one cone step: |S| ≤ |S ∪ ⋃_{s∈S} next(s)|. Anyone formalizing ledger time or future-cone growth cites this. The proof is a one-line application of Finset cardinality monotonicity to the already-proved inclusion of the frontier in its successor cone.
Claim. For any successor map $\mathrm{next}:E\to\mathrm{Finset}\,E$ and any finite frontier $S\subseteq E$, the cardinality satisfies $|S|\le |\mathrm{coneStep}(\mathrm{next},S)|$, where $\mathrm{coneStep}(\mathrm{next},S):=S\cup\bigcup_{s\in S}\mathrm{next}(s)$.
background
LedgerTime isolates the append-only structure that turns a time-symmetric recognition tick into an asymmetric lived past and future. Over an abstract entry type $E$, commits never edit in place; the committed past is immutable and addressable, and the write-head advances by one.
The admissible future is tracked by a frontier finset $S$ and a successor map $\mathrm{next}$. One cone step is the union of the current frontier with all its admissible successors: $\mathrm{coneStep}(\mathrm{next},S)=S\cup S.\mathrm{biUnion},\mathrm{next}$. The companion lemma $\mathrm{cone_grows}$ states the set inclusion $S\subseteq\mathrm{coneStep}(\mathrm{next},S)$ (proved by unfolding and left-union subset).
This module treats those facts as pure finset structure. Identification of $E$ with recognition entries and of $\mathrm{coneStep}$ with the $J$-admissible continuation set is left to the companion paper (MODEL, not THEOREM here).
proof idea
One-line term proof. Apply the standard Mathlib fact that $A\subseteq B$ implies $|A|\le|B|$ (Finset.card_le_card) to the inclusion $S\subseteq\mathrm{coneStep}(\mathrm{next},S)$ already established by cone_grows. No unfolding of coneStep is needed at this layer.
why it matters
Closes the cardinality half of the module's cone package: cone_grows gives set inclusion; this gives nondecreasing admissible count in horizon. Downstream, fieldCone_card_monotone lifts the same inequality to a finite voxel field by summing per-voxel cone cards, so the field future cone never shrinks under one simultaneous cone step.
In the Recognition framework this is structural scaffolding for ledger time, not a forcing-chain step (T0–T8). It underwrites the claim that the lived future widens while the past stays fixed, separating append-only ledger asymmetry from the bare invertible tick. Status remains THEOREM for the finset facts; the physics identification of the cone with $J$-admissible continuations stays MODEL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.