twoBridgesComplex
plain-language theorem explainer
Exact combinatorial complex of signature (2,2,0): two vertices, two parallel non-loop edges both incident as (0,1), and no tetrahedra. Gravity/Gap2 authors cite it as the bridge witness that is globally inequivalent to the two-loops complex under the self-loop count. The body is a pure structure instance: constant edge map and vacuous tet incidence via elim0.
Claim. The exact complex with $2$ vertices, $2$ edges and $0$ tetrahedra whose edge-incidence map sends every edge index to the ordered pair $(0,1)$, and whose tetrahedron-incidence map is the empty map on $\mathrm{Fin}\,0$.
background
An ExactComplex v e t is a cap-free combinatorial complex: exactly $v$ vertices, $e$ edges and $t$ tetrahedra, with abstract incidence data edgeVerts : Fin e → Fin v × Fin v and tetVerts : Fin t → Fin 4 → Fin v. Unlike bounded complexes there is no capacity inequality, so cross-cap identification cannot arise.
This module banks the enriched-carrier API for the Wave C R5 attack on the continuum residual that asserts an oscillatory tail phase inequivalent to the zero phase. After the Fin-8 signature blocker stalled, route C records sharper typed residuals and concrete quotient-internal ticks that escape shell-signature ticks.
The two-bridges complex is the non-loop twin of the two-loops complex: same signature $(2,2,0)$, but both edges are ordinary bridges $(0,1)$ rather than self-loops. Self-loop count is the global equivalence invariant that separates them.
proof idea
Definitional structure instance, not a proof. Both edge indices are sent constantly to the pair $(0,1)$. With $t=0$, tetrahedron incidence is the unique map out of Fin 0, written fun i => i.elim0. No lemmas are applied.
why it matters
Supplies the concrete non-loop witness used by three local results: selfLoopCount_twoBridges (count equals $0$), not_ge_twoLoops_twoBridges (global inequivalence to the two-loops complex via the self-loop invariant), and twoBridgesClass (the corresponding exact path class in the quotient). Together they show that signature alone does not determine the enriched-carrier phase: two complexes of type $(2,2,0)$ can sit in distinct global classes.
In the Gap2 continuum story this is part of route C after routes A and B refused: it does not close R5 or flip gap2_continuum_and_measure, but it pins a sharper residual naming the enriched-carrier obligation. No direct link to T0–T8 forcing, RCL, or the mass ladder; the landmark is the continuum oscillatory-tail residual under the seven gravity gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.