selfLoopCount_twoBridges
plain-language theorem explainer
The two-bridge exact complex (two parallel edges from vertex 0 to 1) has self-loop count zero. Anyone separating bridge complexes from loop complexes via the self-loop invariant cites this evaluation. The proof unfolds both definitions and shows the filtered edge set is empty by direct Fin-2 case analysis.
Claim. For the exact complex with two vertices, two edges, and no tets whose every edge runs from vertex $0$ to vertex $1$, the number of edges with equal endpoints is $0$.
background
This module banks the enriched-carrier API for the continuum R5 residual (an oscillatory tail phase not equivalent to the zero phase), after the Fin-8 signature attack stalled. Route C is the terminal: sharper typed residuals and bridge lemmas; R5 itself stays open.
An ExactComplex v e t packages edge and tet incidence on finite vertex sets. The self-loop count of such a complex is the cardinality of the set of edge indices whose two endpoints coincide. The two-bridges complex is the concrete complex with signature $(v,e,t)=(2,2,0)$ whose edge map sends every edge index to the ordered pair $(0,1)$: two parallel non-loop bridges and no tetrahedra.
Self-loop count is a global-equivalence invariant (proved elsewhere in the module). Evaluating it on named complexes therefore separates equivalence classes without descending into full Burnside mass bookkeeping.
proof idea
Classical mode, then unfold both selfLoopCount and twoBridgesComplex. The count is the card of the Finset of i : Fin 2 with equal endpoints under the constant edge map i ↦ (0,1). A short ext i; simp lemma shows that filter equals the empty Finset on Fin 2 (because 0 ≠ 1). Rewrite by that equality and finish with simp on card ∅ = 0.
why it matters
Feeds two immediate parents. First, not_ge_twoLoops_twoBridges: combined with the evaluation selfLoopCount twoLoopsComplex = 2 and invariance of self-loop count under global equivalence, it proves the two-loops and two-bridges complexes are not globally equivalent (the numeric clash ¬(2=0)). Second, selfLoopClassTick_twoBridges: it pins the descended self-loop class tick of the two-bridges class at zero, giving a concrete quotient-internal tick outside pure shell-signature data.
In the Seven Gaps gravity stack this is scaffolding for the enriched-carrier phase attack on the continuum R5 residual, not a closure of gap2_continuum_and_measure. It does not touch the forcing chain T0–T8, RCL, or the alpha band; it is local incidence arithmetic that makes the self-loop invariant usable as a separator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.