pathPlusIsolated
plain-language theorem explainer
A tet-free bounded complex of bound 4 with census (4,2,0): the directed path 0–1–2 plus an isolated vertex 3. It is one of the two equal-census witnesses in the Gap-2 Poisson coarea ratio test. The construction is purely definitional: fixed counts, decide-checked bounds, and explicit edge/tet maps.
Claim. The tet-free bounded complex of bound $4$ with $n_V=4$, $n_E=2$, $n_T=0$, whose edges are the directed pairs $(0,1)$ and $(1,2)$ and whose tetrahedron map is empty (vacuous on $\mathrm{Fin}\,0$). Equivalently: the directed $2$-path on vertices $0,1,2$ together with an isolated vertex $3$.
background
Gap 2 / A20 studies a LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. Every legal move (append vertex, unpost max unused vertex, append edge, unpost max edge) has rate 1. The module measures stationarity on finite caps and compares class masses at equal census under the uniform stationary law.
A BoundedComplex B packages vertex/edge/tet counts with bound certificates and incidence maps edgeVerts and tetVerts. Census observables (nV, nE, nT) are the raw counts. The process lives on the tet-free slice; here nT = 0.
This complex is the path-plus-isolated witness at census (4,2,0). Its partner is the two-edge complex at the same counts. Upstream geometry modules supply analogous incidence maps for Freudenthal triangulations; the census-measure layer exposes nV, nE, nT as observables.
proof idea
Definitional structure instance, not a proof. Counts are set to nV := 4, nE := 2, nT := 0. The three bound hypotheses hV, hE, hT are discharged by decide. Edges are the piecewise map sending index 0 to (0,1) and every other index to (1,2). The tet map is t.elim0 (empty domain). No lemmas are invoked beyond decidable arithmetic on finite bounds.
why it matters
This is one of the two Aut-distinct equal-census witnesses for the Gap-2 ratio test (clause β). Downstream, deltaCounts_zero records that it shares census (4,2,0) with twoEdgeComplex, so the count-tilt factor is identically 1. pathPlusIsolated_counts exposes the census by rfl. Under uniform stationary π the π-weighted class-mass ratio of the two fibres is exactly 1/2 (fibres 24 and 48), which is the directed Aut correction at these witnesses.
The hostile-probe module reuses the same complex to inhabit Aut and to check locality. Cap-3 uniformity is measured; cap-4 uniformity (host of these witnesses) is derived-unformalized from rate symmetry plus irreducibility. Flag 8 is untouched; no FullTheoryLedger import. The construction feeds residual_family_silent and the SJ-tilt decoy exclusion at q=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.