postEdge
plain-language theorem explainer
Constructor that appends one serially named edge with chosen endpoints to a tet-free bounded complex, raising the edge census by one while keeping the vertex set fixed. Gravity/C16 authors cite it as the forward half of the LIFO edge post/unpost pair. The body is a structure literal: copy vertices and bounds, set nE := nE+1, and route the new max edge name to the chosen pair.
Claim. Given a tet-free complex $K$ at cap $B$ with edge count strictly below $B$, and endpoints $a,b$ among the existing vertices of $K$, form the complex with the same vertex census, edge census $n_E(K)+1$, and edge-endpoint map that agrees with $K$ on all prior edge names and sends the new maximal edge name to $(a,b)$.
background
Gap 2 (lane C16) studies a raw LIFO Poissonized post/unpost process on serially named tet-free slices of bounded complexes. The state space is TetFree B: complexes with vertex and edge censuses at most $B$, no tetrahedra, and edges named by serial indices Fin nE with an endpoint map into vertex pairs. Process symbols deliberately avoid Aut, orbit, gauge, and Gibbs weight; those appear only in conclusions.
Legal moves are: append a vertex; unpost the max vertex if unused; append an edge with chosen endpoints; unpost the max edge. Every legal move has unit rate. The present constructor is the forward edge-append half of that pair. Serial naming (next free edge index) is essential so that unpost of the max name is the exact reverse, which later yields LIFO reverse-pair rate symmetry and, with irreducibility, a uniform stationary law on each finite cap.
proof idea
Definition by structure fields, not a proof. Vertex census and the vertex bound are copied from $K$. Edge census is $K.nE+1$; the edge bound is Nat.succ_le_of_lt applied to the hypothesis $nE < B$. The endpoint map is a case split on the new edge index: indices strictly below the old $nE$ reuse $K$'s map; the residual (maximal) index is assigned the chosen pair $(a,b)$.
why it matters
This is the elementary forward edge move in the C16 MODEL process. Downstream, postEdge_nE records the census bump, postEdge_unpost_nE shows the LIFO round-trip recovers $nE$, and moveRate_symm_lifo_edge is the one-line rate-symmetry identity moveRate K (postEdge ...) = moveRate (postEdge ...) K, both sides unit. That symmetry (with the vertex twin and irreducibility) forces the uniform stationary candidate on each finite cap, which underpins the measured Cap-3 uniformity and the derived Cap-4 uniformity hosting the $(4,2,0)$ ratio test. Flag 8 and FullTheoryLedger stay untouched; the constructor itself carries no Aut or orbit content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.