edgeHeavyClass
plain-language theorem explainer
Packages the edge-heavy labeled complex of signature (1,n,0) as an exact-path class in shell n (n≥1). Gravity and QG residual work cite it as the concrete witness that signature-vertex tick escapes shell-constant phase. Construction is a pair: the shell signature plus the global-equivalence quotient of that complex.
Claim. For each integer $n\ge 1$, the edge-heavy exact-path class in shell $n$ is the pair consisting of the shell signature $(1,n,0)$ and the global-equivalence class of the labeled complex with one vertex, $n$ edges, and zero tetrahedra (all edge endpoints at that vertex).
background
Wave C1 R2 banks an exact-shell tick-phase enrichment schema. An exact-path class at complexity $n$ is a pair: a shell signature together with a global-equivalence class of exact labeled complexes of that signature. No bounded-complexity cap appears in the type.
The edge-heavy complex is the concrete labeled object at signature $(1,n,0)$: one vertex, $n$ edges looping on it, no tetrahedra. The matching shell signature packages those counts and the shell-max identity $\max(1,n,0)=n$ forced by $n\ge 1$.
Dead classes (shell-constant and eventually-zero phase) live in the Zq shell-balance blocker. Escape needs intra-shell tick variance. The eight-tick API is only a Fin-8 trace hypothesis; equidistribution content is independent Prop material in this module.
proof idea
Definitional packaging, not a proof. Form the dependent pair whose first component is the shell signature $(1,n,0)$ and whose second is the quotient class of the edge-heavy labeled complex under global equivalence. Both ingredients are prior defs; the body is a single constructor application.
why it matters
Supplies the concrete class used by the signature-vertex tick witness. Downstream, the tick on this class evaluates definitionally to $1\bmod 8$, and evaluating the shell-constant claim at $n=2$ on this class yields a contradiction (tick $1$ vs tick $2$), proving the derived phase is not shell-constant.
That escape is the THEOREM-level concrete witness named in the module doc: signature vertex-count mod 8 leaves both dead classes. It sits inside the Gap2 residual DAG (R2 / CORE 2 PHASE), feeding the eight-tick octave structure (T7) without claiming continuum or measure closure. OscillatoryTail for this witness and strengthened late-block tail cancellation remain open; this def does not flip gap2 continuum-and-measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.