pathPlusIsolated_counts
plain-language theorem explainer
The directed 2-path on three vertices plus one isolated vertex is a tet-free complex with census exactly (4,2,0). Anyone comparing equal-census witnesses in the Poisson coarea ratio test cites this. The proof is pure definitional reflexivity on the three count fields.
Claim. Let $K$ be the bounded complex given by a directed 2-path on vertices $0,1,2$ together with an isolated vertex $3$. Then the vertex, edge, and tet counts of $K$ satisfy $n_V(K)=4$, $n_E(K)=2$, and $n_T(K)=0$.
background
Gap 2 (lane C16) studies a LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. Legal moves (append vertex, unpost unused max vertex, append edge, unpost max edge) each have rate 1. Under rate symmetry the stationary law on each finite cap is uniform; the equal-census pair at $(4,2,0)$ is the host of the directed Aut-corrected class-mass ratio test.
Census observables extract the three integer coordinates of a named complex: vertex count $n_V$, edge count $n_E$, and tet count $n_T$ (the free label). The witness pathPlusIsolated is the BoundedComplex of capacity 4 whose fields are hard-coded $n_V=4$, $n_E=2$, $n_T=0$, geometrically a directed 2-path plus an isolated vertex. Its Aut-distinct partner at the same census is the two-edge complex used in the $\pi$-weighted fibre comparison.
proof idea
Term-mode triple of rfl. The three conjuncts are definitional equalities: the structure fields of the witness are literally the numerals 4, 2, and 0, so each projection equals its claimed value by reflexivity. No lemmas are invoked.
why it matters
Pins the census of one of the two equal-census witnesses in the Poisson coarea ratio test. Module headline: at census $(4,2,0)$ the stationary class-mass ratio of the two Aut-distinct complexes is exactly $1/2$ (fibres 24 and 48) under uniform $\pi$. Without this count certificate the pair cannot be entered into the fibre-sum comparison or the SJ-tilt decoy receipt.
Downstream, the same certificate is re-exported in the label-erasure hostile probe and is referenced when recording that C4+C16 does not claim full C23 satisfaction (index_c23_not_claimed). Flag 8 and FullTheoryLedger stay untouched; the result is pure witness bookkeeping inside the C35 firewall (no Aut, orbit, or gauge language on the process side).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.