sortRespectingArrivalCount
plain-language theorem explainer
Counts sort-respecting arrival orders on a tet-free complex as nV! · nE! · 0!, the product of factorials of the three letter-block sizes. Gravity and coarea authors cite it when converting raw LIFO census states into order-erasure weights. The body is a one-line product of Nat.factorial on the vertex and edge counts with the empty tetrahedron block.
Claim. For a tet-free serially named complex $K$ at cap $B$, the cardinality of sort-respecting arrival orders is $n_V(K)! \cdot n_E(K)! \cdot 0!$.
background
Gap 2 / A20 studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. States are TetFree B records: vertex count $n_V \le B$, edge count $n_E \le B$, and an edge-endpoint map, with no tetrahedra present. Every legal move (append vertex, unpost max unused vertex, append edge, unpost max edge) has rate 1.
The module headline stresses that the factorial $n_V!, n_E!, n_T!$ is the cardinality of sort-respecting arrival orders of the three letter blocks, not a measure hypothesis inserted into a stationary ansatz. Because the slice is tet-free, the tetrahedron block is empty, so $n_T = 0$ and $0! = 1$.
C35 firewall: process symbols here name neither Aut, orbit, stabilizer, nor Gibbs weight; those appear only on the conclusion side when fibre size is later compared to directed Aut order.
proof idea
Definitional one-liner. Expand the three letter-block factorials: Nat.factorial on $n_V$, on $n_E$, and on $0$ (empty tetrahedron block), then multiply. No lemmas, no tactics, no hypotheses beyond the TetFree field projections.
why it matters
Feeds orderErasureWeight, which takes the rational reciprocal of this count and is the weight that "emerges from counting orders, not from inserting $1/n!$ into a stationary ansatz." In the Gap 2 Poisson coarea story, fibre size of an Aut class equals this arrival-order cardinality divided by directed Aut order (orbit-stabilizer, conclusion side only). That underwrites the equal-census ratio test at census $(4,2,0)$: under uniform stationary $\pi$, the class-mass ratio of the two Aut-distinct witnesses is exactly $1/2$. Flag 8 stays unmoved; FullTheoryLedger is not imported. Landmark contact is local to the gravity seven-gaps lane (C16), not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.