deltaCounts_zero
plain-language theorem explainer
At equal census the two named tet-free complexes (two-edge vs path-plus-isolated) have identical vertex, edge, and tetrahedron counts, so the census difference vanishes and any z to that power is 1. Anyone setting up the Poisson coarea equal-census class-mass ratio cites this. The proof is pure definitional reflexivity on the three count fields.
Claim. The two-edge complex and the path-plus-isolated complex have the same vertex count, the same edge count, and the same tetrahedron count: $n_V = n_V'$, $n_E = n_E'$, and $n_T = n_T'$. Equivalently the census difference vanishes, so $z^{\Delta\mathrm{counts}} = 1$.
background
Gap 2 / A20 (lane C16) studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. Every legal move has rate 1; under rate symmetry the stationary law on each finite cap is uniform. The headline equal-census pair is the two-edge complex versus the path-plus-isolated complex at census $(4,2,0)$.
Census observables come from the census-measure layer: $n_V$, $n_E$, and $n_T$ extract the vertex, edge, and tetrahedron (loop) counts of a named ensemble state. The module treats the factorial $n_V!, n_E!, n_T!$ as the cardinality of sort-respecting arrival orders, not as a free hypothesis. Process language is firewalled away from Aut, orbit, and Gibbs weight; those appear only in conclusions and the pre-registered ratio comparison.
The doc-comment frames this lemma as $\Delta\mathrm{counts}=0$ at equal census, hence $z^{\Delta\mathrm{counts}}=1$, clearing any pure-census tilt before the class-mass ratio is read.
proof idea
Term-mode proof by a triple of reflexivity: $\langle \mathrm{rfl},, \mathrm{rfl},, \mathrm{rfl}\rangle$. The three count fields of the two complexes are definitionally equal, so no lemma application or arithmetic is required. The statement is a pure census identity, not a dynamical claim.
why it matters
The Poisson coarea headline needs an equal-census pair so that the $\pi$-weighted class-mass ratio under uniform $\pi$ reduces to a pure fibre-size ratio. Module text records that ratio as exactly $1/2$ (fibres 24 and 48) for this pair, with the SJ-tilted decoy showing the instrument responds as $\mathrm{ratio}(q)=\mathrm{fibre_ratio}\cdot q^{\Delta SJ}$; at $q=1$ a nonunit $q^{SJ}$ tilt is excluded at these witnesses. Establishing $\Delta\mathrm{counts}=0$ is the census half of that setup: it forces $z^{\Delta\mathrm{counts}}=1$ and keeps C6 and the C27 $q^{SJ}$ trigger silent on the unit-rate process.
No downstream Lean consumers are wired yet (used_by empty). The lemma still anchors the equal-census clause of the Gap-2 ratio test and the claim that Flag 8 is unmoved. Cap-4 uniformity hosting $(4,2,0)$ remains DERIVED-UNFORMALIZED; this identity does not close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.