pathPlusIsolated_counts
plain-language theorem explainer
The directed 2-path on three vertices plus one isolated vertex is a bounded complex with exactly four vertices, two edges, and zero tetrahedra. Census and Poisson-coarea arguments cite this as the fixed count triple for that test complex. The proof is pure definitional reflexivity on the structure fields.
Claim. For the bounded complex given by a directed 2-path on vertices $0,1,2$ together with an isolated vertex $3$, the census observables satisfy $n_V = 4$, $n_E = 2$, and $n_T = 0$.
background
In the Gap-2 census layer, an ensemble carries three real observables: vertex count $n_V$, edge count $n_E$, and tet (free-label) count $n_T$. A BoundedComplex c packages those counts with the inequalities that keep them inside the bound $c$.
The object under study is the standard test complex: a directed path of length two on vertices $0,1,2$ plus an isolated vertex $3$. Its structure fields are hard-coded as $n_V=4$, $n_E=2$, $n_T=0$ (with the bound checks discharged by decide). The same complex appears in the Poisson-coarea module under the same name and counts.
This file is an uncommitted hostile probe of Gap2 label-erasure (attacks on the G1 dependency graph, definitional collapse, directed Aut recomputation, and vacuity). The count lemma is the bookkeeping anchor for those probes.
proof idea
Term-mode proof by a triple of rfl. Each conjunct is definitionally true because the structure fields of the path-plus-isolated complex are written as the literals $4$, $2$, and $0$. No lemmas are applied; the equality is pure definitional reduction.
why it matters
Supplies the fixed census triple used by the Poisson-coarea side of Gap 2. Downstream, the mirrored count statement and the index flag index_c23_not_claimed (which records that C4+C16 do not fully discharge C23) sit on the same complex. In the hostile-probe module it pins the fibre/Aut bookkeeping so that attacks on label erasure and directed automorphism recomputation cannot silently change the vertex/edge/tet numbers. It is scaffolding hygiene rather than a physics derivation: no link to the forcing chain T0–T8, RCL, or the mass ladder is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.