pathPlusIsolated
plain-language theorem explainer
Explicit 4-vertex bounded complex: a directed 2-path on vertices 0–1–2 plus an isolated vertex 3, with census (nV,nE,nT)=(4,2,0) and empty tetrahedron list. Hostile-probe and Poisson-coarea modules cite it as the standard residual test complex at that census. Construction is by direct field assignment and decide on the bound proofs.
Claim. Let $K$ be the bounded complex of capacity 4 with $n_V=4$, $n_E=2$, $n_T=0$, edge map $e\mapsto(0,1)$ if $e=0$ and $(1,2)$ otherwise, and empty tetrahedron vertex map. Then $K$ is the directed path on three vertices plus one isolated vertex.
background
A BoundedComplex c packages finite vertex, edge, and tetrahedron counts (at most $c$) together with incidence maps edgeVerts and tetVerts. Census observables nV, nE, nT extract those counts as the discrete data compared across complexes in Gap-2 gravity arguments.
This module is an uncommitted hostile probe of Gap2 label-erasure: it stress-tests Aut recomputation, fibre counts, and definitional collapse at the small census $(4,2,0)$. Section D notes that for $n_T=0$, Aut membership reduces to ordered edge-commutation on vertex and edge permutations.
Upstream geometry modules supply analogous incidence tables (Freudenthal cube and two-cube strip edge/tet lists); here the incidence is the minimal path-plus-isolated pattern used as a residual comparator.
proof idea
Definitional structure instance, not a proof. Counts are literal numerals; the three bound hypotheses hV, hE, hT are discharged by decide. Edge incidence is the piecewise map sending edge 0 to $(0,1)$ and every other edge index to $(1,2)$. The tet map is elim0 on the empty Fin 0, so there are no tetrahedra.
why it matters
Gives the canonical residual complex at census $(4,2,0)$ for Gap-2 label-erasure and Poisson-coarea work. Downstream, pathPlusIsolated_counts freezes the census equalities; pathPlus_aut_inhabited shows Aut is nonempty via the identity relabel; deltaCounts_zero equates its census to twoEdgeComplex so the coarea weight factor $z^{\Delta\mathrm{counts}}$ is 1; and residual_family_silent / Cap-3 stationary uniformity arguments use it as a named residual state. In the RS gravity Gap-2 chain this is scaffolding for directed-Aut kernel enumeration (C16 receipt) and for showing residual families do not spoil the erasure Jacobian, not a forcing-chain (T0–T8) landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.