edgeHeavySig
plain-language theorem explainer
Builds the shell signature (1, n, 0) at level n ≥ 1: one vertex slot, n edges, zero triangles, with max equal to n. Gravity/Gap2 authors cite it as the combinatorial type of the edge-heavy complex. The body is a direct subtype package: Fin witnesses plus a three-line max identity.
Claim. For every natural number $n \ge 1$, the triple $(v,e,t) = (1,n,0)$ is a shell signature at level $n$: each count lies in $\{0,\ldots,n\}$ and $\max(1,\max(n,0)) = n$.
background
A shell signature at level $n$ is a triple $(v,e,t)$ of vertex, edge, and triangle counts, each at most $n$, with $\max(v,e,t)=n$. It is packaged as a subtype of $\mathrm{Fin}(n+1)^3$ so the type is finite. The name "edge-heavy" means the edge coordinate saturates the level: $e=n$, while $v=1$ and $t=0$.
This module banks Wave C1 R2: exact-shell tick-phase enrichment. Exact path classes are already GlobalEquivalent quotients (sigma over shell signatures of the exact-setoid quotient), so a tick map into $\mathrm{Fin},8$ is well-posed on classes. Dead classes (shell-constant and eventually-zero phase) are blocked elsewhere; escape needs intra-shell tick variance.
Upstream, ShellSig is the finite signature type; the single-edge complex (two vertices, one edge, zero triangles) is the geometric prototype that this signature generalizes at level $n$.
proof idea
Term-mode subtype construction. The triple is assembled as Fin elements: $1$ (via omega), $n$ (strictly below $n+1$), and $0$ (positive successor). The residual proof obligation is $\max(1,\max(n,0))=n$. Rewrite $\max(n,0)=n$, then apply the right-max identity under the hypothesis $1\le n$. No external lemmas beyond Nat max facts.
why it matters
Feeds edgeHeavyClass, which wraps this signature with the quotient of the edge-heavy complex to produce an ExactPathClass n. That class is the concrete combinatorial witness used later in the module to escape both dead phase classes (shell-constant and eventually-zero) via signature vertex-count mod 8.
In the Recognition Gravity Gap2 chain, this is scaffolding for the tick-phase substrate: eight-tick equidistribution and shell-amplitude vanishing sit downstream of having non-dead classes inside each shell. It does not itself touch the continuum/measure gap flip, the strengthened late-block residual, or the still-open oscillatory tail (R4) for the signature-vertex witness. Landmark contact is the eight-tick octave (T7) as Fin-8 phase, not as an equidistribution theorem (that content is separate Props in this module).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.