emptyTF
plain-language theorem explainer
The empty tet-free complex at any finite name-cap B: zero vertices, zero edges, and a vacuous edge-endpoint map. It is the unique zero-letter state of the C16 LIFO post/unpost chain on BoundedComplex slices. Anyone measuring stationarity or irreducibility from the empty seed cites it. Construction is a direct structure instance: Nat.zero_le for the bounds and Fin-elim0 for the empty edge map.
Claim. For every bound $B \in \mathbb{N}$, there is a tet-free serially named complex at cap $B$ with $n_V = 0$, $n_E = 0$, the inequalities $0 \le B$, and edge-endpoint map on the empty finite type $\mathrm{Fin}\,0$.
background
Gap 2 (A20, lane C16) studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. The state space is TetFree B: pairs $(n_V, n_E)$ at most $B$, plus an endpoint assignment $\mathrm{Fin},n_E \to \mathrm{Fin},n_V \times \mathrm{Fin},n_V$. No Aut, orbit, or gauge data lives in that structure (C35 firewall).
Legal moves append a vertex, unpost the max unused vertex, append an edge with chosen endpoints, or unpost the max edge; every legal move has rate 1. The module headline is that this process has symmetric legal rates, hence a uniform stationary law on each finite cap, with the equal-census class-mass ratio $1/2$ at the $(4,2,0)$ witnesses under uniformity.
The empty complex is the seed of that chain: the unique zero-letter state from which irreducibility is claimed for the cap-3 census (910 named states, uniform $1/910$).
proof idea
Pure structure construction, not a tactic proof. Set vertex and edge counts to $0$. Discharge the two bound obligations $n_V \le B$ and $n_E \le B$ by Nat.zero_le B. Supply the endpoint map as the unique function out of Fin 0 via elim0 (no edges to name). The resulting inhabitant has type TetFree B for every $B$.
why it matters
In the Gap 2 / Poisson recognition coarea program, every measured stationarity and irreducibility statement is anchored at the empty seed: the off-diagonal rate matrix is symmetric, the chain is irreducible from empty, and the unique stochastic stationary law on cap-3 is uniform $1/910$. Cap-4 uniformity (host of the $(4,2,0)$ ratio test) is the same rate-symmetry plus irreducibility argument, still starting here.
Sibling process primitives (postVertex, unpostMaxVertex, postEdge, unpostMaxEdge, moveRate, arrival-order factorials) act on this state space; the empty complex is the zero of that monoid of named complexes. Flag 8 stays unmoved and FullTheoryLedger is not imported: this is pure process scaffolding for the C16 kill test, not a gravity-constant claim. No downstream theorem yet wires it (used-by count is zero), so its role is foundational rather than a finished ratio lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.