allLoopsComplex
plain-language theorem explainer
The all-loop complex of complexity n (n ≥ 1) is the exact combinatorial complex with signature (1, n, 0): one vertex, n edges, zero tetrahedra, and every edge a self-loop at that vertex. Gravity and Gap-2 authors cite it as the degenerate labeled complex fixed by endpoint reversal and by the composite endpoint-reversal-plus-tet-slot-rotation. The body is a direct structure instance: constant edge map to (0,0) and empty tet map via elim0.
Claim. For every natural number $n \ge 1$, the all-loop complex of complexity $n$ is the exact complex of signature $(v,e,t)=(1,n,0)$ whose edge incidence sends every edge index to the self-loop $(0,0)$ and whose tetrahedron incidence is the empty map on $\mathrm{Fin}\,0$.
background
An exact complex of signature $(v,e,t)$ is a cap-free combinatorial complex with exactly $v$ vertices, $e$ edges and $t$ tetrahedra, given by abstract incidence maps edgeVerts : Fin e → Fin v × Fin v and tetVerts : Fin t → Fin 4 → Fin v. Unlike bounded complexes, there are no capacity inequalities, so cross-cap identification issues do not arise.
This module banks a conditional TailFiberShift bridge for the enriched-carrier phase route (Wave C1 residual R4). The structure hypothesis is a tail family of class-preserving shell automorphisms that rotate the Fin-8 tick by +1; existence remains open. As fallback credit, the module records no-gos: candidate operations on labeled exact complexes (endpoint reversal, tetrahedron slot rotation, and their composite) each fix a degenerate complex in every shell.
The all-loop complex is the edge-degenerate witness: one vertex, n self-loops, no tets. Upstream edge/tet tables from Freudenthal cube and two-cube strip triangulations supply the ambient incidence language; here they are specialized to the constant self-loop and the empty tet family.
proof idea
Definitional construction, not a proof. Instantiate ExactComplex 1 n 0 by setting every edge incidence to the pair (0, 0) and discharging the empty tetrahedron family with Fin 0 elimination (elim0). The hypothesis 1 ≤ n is carried only to match the complexity convention used by the no-go lemmas; it is unused in the fields.
why it matters
Supplies the degenerate labeled complex that endpoint reversal and the composite endpoint-reversal-then-tet-slot-rotation fix pointwise. Downstream, endpointReversal_fixes_allLoops and endpointReversalThenTetSlotRotation_fixes_allLoops are one-line simp theorems establishing those fixed points. Fixed classes in every shell are incompatible with a genuine tick shift (τ c = τ c + 1 fails in Fin 8), so signature-level Fin-8 routes stay closed by the Burnside stall.
In the Recognition Gravity Gap-2 program this is fallback credit on residual R4: TailFiberShift remains an uninhabited structure hypothesis, gap2_continuum_and_measure stays false, and the module introduces no sorry or new axiom. The definition is the concrete witness that makes the no-go statements checkable rather than schematic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.