twoLoopsComplex
plain-language theorem explainer
Concrete exact complex of signature (2,2,0) whose two edges are both the self-loop (0,0) at a single vertex. Gravity/Gap2 authors cite it as the canonical two-loop witness when separating path classes by self-loop count. The body is a structure instance: constant edge map to (0,0) and an empty tetrahedron map via elim0.
Claim. Let $\mathrm{ExactComplex}\,n_e\,n_v\,n_t$ be the exact-shell complex type with $n_e$ edges, $n_v$ vertex labels, and $n_t$ tetrahedra. There is a complex of signature $(2,2,0)$ in which every edge is the self-loop $(0,0)$ at vertex $0$, and the tetrahedron family is empty.
background
This module banks the enriched-carrier API for the Wave C R5 attack on the continuum residual that asserts an oscillatory tail phase distinct from the zero phase. Route A (forcing late mass balance from the carrier) stalled; route B (Fin-8 signature blocker) was refused. The terminal credit path is route C: sharper typed residuals plus characterization and bridge lemmas. R5 itself remains open.
ExactComplex (from ExactShellGaugeUV) packages edge and tetrahedron vertex maps for a fixed signature. Here the signature is $(2,2,0)$: two edges, two vertex slots in the label, zero tets. Sibling machinery defines selfLoopCount on such complexes and proves it is invariant under the global equivalence used to form ExactPathClass.
Upstream edge/tet maps from Freudenthal cube and two-cube strip supply the ambient combinatorial language; this definition is the degenerate pure-loop instance used as a counter-witness against bridge-only complexes.
proof idea
Pure structure instance, not a proof. The edge map sends every index in Fin 2 to the ordered pair $(0,0)$. The tetrahedron map is fun i => i.elim0, which is the unique map out of the empty type Fin 0. No lemmas are applied.
why it matters
Supplies the two-loop witness inside the enriched-carrier phase module. Downstream, selfLoopCount_twoLoops evaluates the self-loop count to 2; not_ge_twoLoops_twoBridges then uses invariance of that count to separate this complex from the two-bridge complex (count 0). twoLoopsClass quotients it into an ExactPathClass 2 representative.
In the Gap2 program this is characterization infrastructure for route C, not a closure of the continuum residual: the module doc states R5 stays open and gap2_continuum_and_measure is not flipped. It does not touch T0–T8 forcing, RCL, or the mass ladder; it is local combinatorial support for the oscillatory-tail residual naming.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.