loopCount_twoBridges
plain-language theorem explainer
The two-bridge complex (two parallel edges on two vertices, sizes (2,2,0)) has loop count zero: neither edge is a self-loop. Anyone comparing the size-blindness witnesses cites this as the zero side of the pair. The proof is a one-line kernel decision on the finite incidence data.
Claim. Let $K$ be the bounded complex with two vertices, two edges, and no tetrahedra, whose edges are the parallel non-loops $(0,1)$ and $(0,1)$. Then the number of edges of $K$ with equal endpoints is $0$.
background
Gap 2 asks how far the gluing derivation of the class measure reaches without size-blindness. An additive incidence statistic is relabeling-invariant, additive on disjoint unions, and zero on the empty complex. The three index sizes qualify; so do the loop count (edges with equal endpoints) and the proper-edge count.
For any such statistic and $\lambda>0$, the weight $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$ satisfies gluing multiplicativity wherever automorphism counts multiply, and its class mass is $\lambda^{\mathrm{stat}}/|\mathrm{Aut},K|$. The three atom normalizations kill the loop-count escape but leave the proper-edge escape open.
Here twoBridges is the complex with $n_V=2$, $n_E=2$, $n_T=0$ and both edges the non-loop $(0,1)$. Its companion witness twoLoops has the same three sizes but two self-loops. Loop count is defined by filtering edges with equal endpoints and taking cardinality.
proof idea
One-line kernel proof: by decide. The finite complex is fully concrete (two vertices, two edges with explicit endpoint pairs both unequal), so the filtered Finset is empty and its card is definitionally zero. Marked @[simp] for downstream rewrites.
why it matters
This is the zero half of the witness pair that shows loop count is not a function of the three index sizes. Downstream, witnesses_same_sizes_different_loops rewrites both sides via loopCount_twoLoops and this lemma, then decides the inequality. That pair feeds loopEscape_not_sizeBlind: if the loop-stat weight were size-blind, the two witnesses would receive equal weight, but they differ by a factor $\lambda^{\pm 2}$ whenever $\lambda\neq 1$.
The same pair appears in postingAlphabet_is_determined_by_the_sizes, which shows the posting alphabet depends only on cell counts and therefore cannot see the incidence distinction the escape exploits. In the Gap 2 story this pins the positive reach bound: the other five hypotheses do not force size-blindness, because the loop-count weight satisfies them yet fails premise (i).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.