twoEdge_counts
plain-language theorem explainer
The two-disjoint-edge witness complex has census triple (4, 2, 0): four vertices, two edges, zero tets. Anyone running the Gap-2 equal-census class-mass ratio against its Aut-distinct partner cites this identity. The proof is pure definitional equality by reflexivity on the structure fields.
Claim. The labeled complex of two disjoint edges has vertex count $n_V = 4$, edge count $n_E = 2$, and tet count $n_T = 0$.
background
Gap 2 (A20, lane C16) studies a LIFO Poissonized post/unpost process on tet-free bounded complexes. Legal moves have unit rate; under rate symmetry the stationary law on each finite cap is uniform. The headline ratio test compares two Aut-distinct complexes at the shared census $(4,2,0)$ and claims class-mass ratio exactly $1/2$ under that uniform law.
A BoundedComplex B carries three natural counts: vertices, edges, and free tet labels, with bounds relative to $B$. The census observables $n_V$, $n_E$, $n_T$ simply project those fields (as reals) out of an ensemble point. The witness twoEdgeComplex is the concrete $B=4$ complex whose edges are $0\to 1$ and $2\to 3$, with fields hard-coded to $n_V=4$, $n_E=2$, $n_T=0$.
The companion single-edge complex (two vertices, one edge) sits upstream as the elementary gluing atom; the two-edge complex is the disjoint union of two such atoms and is the first equal-census witness named in the module headline.
proof idea
Term-mode proof by a triple of rfl. The three conjuncts are definitional equalities: the structure fields of the two-edge complex are literally 4, 2, and 0, so each projection equals the corresponding numeral by reduction. No lemmas are invoked.
why it matters
The module headline fixes the equal-census pair at $(4,2,0)$ and asserts that the $\pi$-weighted class-mass ratio of the two Aut-distinct witnesses is exactly $1/2$ (fibres $24$ and $48$) once uniformity is granted. This declaration pins the left-hand witness to that census triple by definition, so every subsequent fibre-count or ratio comparison can quote the triple without re-opening the structure.
In the broader Recognition Gravity stack this is scaffolding for the Poisson coarea / directed-Aut correction story (Gap 2), not a forcing-chain step (T0–T8). Flag 8 stays unmoved; no ledger import. The factorial $n_V!,n_E!,n_T!$ later appears as the cardinality of sort-respecting arrival orders, so locking $(n_V,n_E,n_T)=(4,2,0)$ also locks that factorial to $4!\cdot 2!\cdot 0! = 48$ on this witness.
No downstream formal dependents are recorded yet; the declaration exists so the ratio-test clause can name a concrete complex whose census is known by rfl.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.