twoBridgesClass
plain-language theorem explainer
Packages the complexity-2 exact path class of two parallel non-loop bridges between the same vertex pair, under shell signature (2,2,0). Gravity/Gap2 authors cite it when separating quotient-internal incidence from shell-signature-only data. The body is a one-line pair of the double-edge signature with the global-equivalence class of the two-bridges complex.
Claim. The exact path class of complexity $2$ given by shell signature $(V,E,T)=(2,2,0)$ together with the global-equivalence class of the exact complex whose two edges both run from vertex $0$ to vertex $1$ and which carries no tetrahedra.
background
Exact path classes are the combinatorially distinct exact complexes of fixed complexity $n$: a dependent sum over shell signatures of the quotient of exact labeled complexes by global equivalence. No bounded-complexity cap appears in that type.
The double-edge shell signature is $(2,2,0)$: two vertices, two edges, zero tetrahedra. The two-bridges complex realizes that signature with both edges incident as $(0,1)$ and an empty tetrahedron family. Parallel non-loop edges are the point; self-loop count on this representative is zero.
The ambient module banks an enriched-carrier API for the continuum R5 residual (existence of a nontrivial oscillatory tail phase). Route A (eventual mass balance) stalled; route C keeps a sharper typed residual and characterization lemmas without flipping the continuum-and-measure gap.
proof idea
Definitional constructor only. Pair the shell signature doubleEdgeSig with Quotient.mk of twoBridgesComplex under the exact-complex global-equivalence setoid at that signature. No lemmas or tactics beyond the structure introduction.
why it matters
Supplies the zero-self-loop witness at signature $(2,2,0)$ against the two-loops class at the same signature. Downstream, selfLoopClassTick_twoBridges evaluates the self-loop class tick on this class to $0$, and selfLoopClassTick_not_ShellSigTick uses both classes to prove the self-loop tick does not factor through shell signature alone: any purported signature-only map would identify the two classes yet assign different tick values.
That quotient-internal distinction is the concrete tick that escapes ShellSigTick in the enriched-carrier Wave C attack. It does not close R5 (still open/uninhabited) and does not flip gap2_continuum_and_measure; it only banks the carrier-side witness needed for sharper residual naming.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.