constTetComplex
plain-language theorem explainer
Defines the constant-tetrahedron exact complex of signature (1,0,n) for n ≥ 1: one vertex, no edges, and every tetrahedron slot pinned to vertex 0. Gravity/Gap2 authors cite it as the degenerate fixed point of slot rotation and endpoint-reversal composites. The body is a two-field structure instance with empty-edge elim0 and constant tet map.
Claim. For each integer $n \ge 1$, the constant tetrahedron complex of complexity $n$ is the exact complex with signature $(v,e,t)=(1,0,n)$ whose edge-incidence map is the empty map on $\mathrm{Fin}\,0$ and whose tetrahedron-vertex map sends every slot of every tetrahedron to the unique vertex $0$.
background
An exact complex (ExactComplex) is a cap-free combinatorial complex with fixed counts of vertices, edges, and tetrahedra, given by abstract incidence maps: edges as pairs of vertex indices, tetrahedra as maps from four slots into the vertex set. There are no capacity inequalities, so cross-cap identification issues of bounded complexes do not arise.
This module sits in the Wave C1 R4 residual of the enriched-carrier phase route for Gap2. It banks a conditional TailFiberShift hypothesis (class-preserving shell automorphisms that rotate the Fin-8 tick by +1) and records no-go fallbacks: candidate operations on labeled exact complexes (endpoint reversal, tetrahedron slot rotation, and their composite) each fix a degenerate complex in every shell.
The constant-tet object is the pure tetrahedron degeneration: one vertex, zero edges, n tets all collapsed to that vertex. Related Freudenthal edge/tet tables elsewhere supply non-degenerate cube triangulations; here the incidence data are deliberately trivial.
proof idea
Definitional structure instance, not a proof. The edge map is Fin.elim0 on the empty edge index type (signature has e = 0). The tet map is the constant function sending every tetrahedron index and every Fin-4 slot to vertex 0. The hypothesis n ≥ 1 is carried unused in the fields but keeps the complexity parameter in the intended range for downstream fixed-point lemmas.
why it matters
Supplies the degenerate witness that tet-slot rotation and the composite endpoint-reversal-then-slot-rotation fix pointwise. Downstream theorems tetSlotRotation_fixes_constTet and endpointReversalThenTetSlotRotation_fixes_constTet use it to show those candidate shell operations induce class maps that fix a class in every shell.
That fixed-class behaviour is incompatible with a free Fin-8 tick shift (τc = τc + 1 fails), so signature-level Fin-8 routes stay closed. The module status remains OPEN: TailFiberShift is uninhabited, gap2 continuum-and-measure stays false. The definition is bankable scaffolding for the no-go side of residual R4, not a positive existence claim about oscillatory tails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.