exactComplex_zero_eq
plain-language theorem explainer
Any exact complex with zero edges and zero tetrahedra at shell 0 equals the isolated-vertices complex. Used by the shell-0 path-class uniqueness step in the Gap2 tick-phase tail blocker (finite-head impossibility). Proof is a structure cases split plus Fin-0 elimination via funext.
Claim. If $K$ is an exact complex at shell $0$ with zero edges and zero tetrahedra, then $K$ equals the isolated-vertices complex at shell $0$.
background
Module hardens the R4 residual in the Gap2 tick-phase story after the R2 cross-family correction. Two routes matter: (a) all-shell tick-fiber mass balance forces every exact shell amplitude to vanish, hence contiguous-block sums and oscillatory tail; (b) finite-head impossibility at shell 0, where the class space is a singleton so mass cannot balance across tick fibers.
An exact complex packages edge-vertex and tetrahedron-vertex data (Freudenthal-style edgeVerts / tetVerts). The isolated-vertices complex is the empty choice of those data. Parameters (0,0,0) mean shell index 0 with empty edge and tet index types, so both maps are functions out of Fin 0.
Upstream geometry supplies the edge/tet vertex tables used elsewhere; here only the empty-index fact is needed. The sibling shellSig_zero_eq plays the same role one level up for signatures.
proof idea
Term-mode structure induction: case-split K as mk e t. For edges, funext over the empty index type: every i : Fin 0 is eliminated by elim0, so e equals the isolated complex's edge map. Same for tetrahedra. Rewrite both fields to finish. No external lemmas beyond empty-type elimination.
why it matters
Feeds exactPathClass_zero_eq ("Every class at shell 0 equals the unique empty-complex class"), which underwrites the finite-head half of the R4 blocker: shell 0 is a singleton class, so classMu mass sits in one tick fiber for every phase and TickFiberMassBalanced is impossible. That pairs with the eventual-balance repair (late amplitudes killed) so the finite head does not obstruct OscillatoryTail.
Lives in Gravity / SevenGaps Wave C1 R4 hardening. Does not close the open R4 residual (existence of a substrate phase with oscillatory tail) nor the signature-level SignatureFin8OscillatoryTailBlocker. No contact with T5–T8 forcing, RCL, or the alpha band; pure combinatorial support for the Gap2 continuum/measure side-conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.