loopCount_twoLoops
plain-language theorem explainer
The two-loop witness complex has loop count exactly 2. Anyone comparing incidence statistics on equal-size complexes cites this evaluation. The proof is a one-line decidability check on the finite filter defining the loop set.
Claim. For the bounded complex consisting of two loops on two vertices (sizes $(n_V,n_E,n_T)=(2,2,0)$), the number of edges with coincident endpoints equals $2$.
background
Gap 2 studies how far the gluing derivation of the class measure reaches without size-blindness. Size-blindness says the labeled weight depends only on the three index sizes $(n_V,n_E,n_T)$. The module constructs additive incidence statistics that are not functions of those sizes, to test whether the other premises force size-blindness.
Loop count is one such statistic: the number of edges of a bounded complex whose two endpoints coincide. It is relabeling-invariant, additive over disjoint unions, and vanishes on the empty complex, but is not determined by the three sizes alone.
The complex twoLoops is the explicit witness with two loops at a single vertex, sizes $(2,2,0)$. Its counterpart with the same sizes but no loops (two bridges) is used later to separate loop count from the size triple.
proof idea
One-line computational proof: decide evaluates the finite filter that counts edges with equal endpoints on the concrete two-edge complex and confirms the cardinality is 2. No algebraic lemmas are needed beyond the definition of loop count as that filter's card.
why it matters
This evaluation is the left half of the witness pair that shows loop count is not a function of the three sizes. Downstream, witnesses_same_sizes_different_loops rewrites with this fact and the companion count for two bridges, then decides inequality. That pair feeds loopEscape_not_sizeBlind, which proves that the weight $\lambda^{\mathrm{loopCount}}/(n_V!,n_E!,n_T!)$ fails size-blindness whenever $\lambda\neq 1$.
In the Gap 2 narrative, the three atom normalizations kill the loop-count escape (the single loop has loop count one, so its weight is $\lambda$ rather than 1). Establishing the concrete value on the two-loop witness is the arithmetic step that makes the non-size-blindness argument fully computational. It also appears in the posting-alphabet comparison that shows the alphabet carries no incidence data beyond the sizes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.