properEdgeCount_twoBridges
plain-language theorem explainer
The two-bridge complex (two parallel non-loop edges on two vertices) has proper-edge count exactly 2. Gravity and ledger-cohomology arguments cite this as the numeric witness that separates twoBridges from twoLoops at the shared size triple (2,2,0). The proof is a one-line kernel decision on the finite filtered card.
Claim. For the bounded complex consisting of two vertices and two parallel non-loop edges (the two-bridge complex of size triple $(2,2,0)$), the number of edges whose endpoints differ equals $2$.
background
Gap 2 studies how far the gluing derivation of the class measure reaches once size-blindness is dropped. An additive incidence statistic is relabeling-invariant, additive under disjoint union, and zero on the empty complex. Besides the three index sizes, two incidence functions qualify: loop count (edges with equal endpoints) and proper-edge count (edges with distinct endpoints).
Proper-edge count is defined by filtering the edge set of a bounded complex $K$ to those $i$ with distinct endpoint pair and taking cardinality. Unlike loop count, it vanishes on every single-vertex complex, so the three unit normalizations at the atoms do not kill the proper-edge escape.
The two-bridge complex is the explicit witness with $n_V=2$, $n_E=2$, $n_T=0$ and two parallel non-loop edges $(0,1)$. It shares the size triple $(2,2,0)$ with the two-loop complex but carries a different incidence profile.
proof idea
One-line computational proof: decide evaluates the filtered Finset card that defines proper-edge count on the concrete two-bridge complex and checks equality with 2. No lemmas are invoked beyond the definition of the count and the structure fields of the witness.
why it matters
This simp fact is the numeric anchor for the C18 obstruction and the Gap-2 reach bound. Downstream, incidenceCost_not_coboundary rewrites history at twoBridges through this equality to get history 2, ruling out a ledger coboundary. incidenceCost_history_not_a_function_of_counts and incidence_is_genuine_H1_class use the same witness pair (twoLoops vs twoBridges) to show the incidence cost is not count-linear and generates an $H^1$ class outside $\mathrm{span}{dn_V,dn_E,dn_T}$.
no_odd_pullback_of_incidence_class fails the parity-odd equation at twoBridges because history is $2t$ there while any pullback re-evaluates a non-negative multiple of proper-edge count. Inside this module, properEscape_classMass_ne_mu and properEscape_not_sizeBlind use the count 2 to show the proper-edge escape has class mass $\lambda^2/|\mathrm{Aut}|$ rather than the RS measure $1/|\mathrm{Aut}|$, so the derivation's conclusion fails for that escape. The probe probe_witness_counts packages the same equality for hostile checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.