edgeHeavyComplex
plain-language theorem explainer
Exact combinatorial complex of signature (1, n, 0): one vertex, n edges, zero tetrahedra, every edge a self-loop at the unique vertex. Gravity and QG auditors cite it as the edge-heavy witness that seeds a path class inside shell n for the Gap 2 tick-phase substrate. The body is a pure data constructor (constant edge map; empty tet map via Fin-0 elimination).
Claim. For each natural number $n$, the edge-heavy exact complex of signature $(v,e,t)=(1,n,0)$ is the labeled complex whose single vertex carries all $n$ edges as loops $(0,0)$ and whose tetrahedron index set is empty.
background
The ambient module banks the Wave C1 R2 schema residual: tick assignments on exact path classes inside shell $n$, with escape from the dead classes ShellConstant and EventuallyZeroPhase requiring intra-shell tick variance. Eight-tick structure is only a Fin-8 trace hypothesis; equidistribution is an independent Prop here.
An exact complex (from ExactShellGaugeUV) is a cap-free combinatorial type with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra, given by incidence maps edgeVerts : Fin e → Fin v × Fin v and tetVerts : Fin t → Fin 4 → Fin v. No capacity inequalities appear, so cross-cap identification pathologies of bounded complexes cannot arise.
Upstream geometry modules supply concrete Freudenthal edge and tet tables for cubes and two-cube strips; those are full triangulations. The present constructor is the opposite extreme: maximal edge count relative to a single vertex and no tets.
proof idea
Definitional constructor for the ExactComplex structure at parameters $(1,n,0)$. The edge incidence map is the constant function sending every edge index to the loop $(0,0)$ on the unique vertex in Fin 1. The tet incidence map is obtained by eliminating on Fin 0 (no tetrahedra), so the Fin-4 vertex list is vacuously defined. No lemmas are invoked.
why it matters
Feeds edgeHeavyClass, which packages this complex (with the matching shell signature at level $n\ge 1$) as a point of ExactPathClass $n$ via the GlobalEquivalent quotient. That class is the concrete edge-heavy witness inside the tick-phase substrate schema: derived phase $2\pi\cdot\mathrm{tick}/8$, non-circular equidistribution guards, and the bridge from mass-balanced Fin-8 fibers to shell-amplitude vanishing by eighth-root orthogonality.
In the Recognition forcing chain this sits under the eight-tick octave (T7) infrastructure used by Gap 2 residual work. It does not itself flip continuum-and-measure closure; the module keeps TypedResidual strengthened tick-balance and analytic OscillatoryTail (R4) open. The decoy raw-complexity tick is separately shown ShellConstant (dead); this witness is the combinatorial seed for the live escape path via signature vertex-count mod 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.