ShellsUpTo
plain-language theorem explainer
Disjoint union of exact complexity shells of index at most B: pairs (n, class) with n in {0,...,B} and class an exact path class of complexity n. Gravity/SevenGaps authors cite it as the exact-shell side of the capped-quotient carrier equivalence. Defined as a dependent sum over Fin(B+1), so the shell range is off-by-one-safe and finite.
Claim. For each natural number $B$, write $\mathrm{ShellsUpTo}(B)$ for the type of pairs $(n,c)$ where $n\in\{0,\ldots,B\}$ and $c$ is a combinatorially distinct exact complex of complexity exactly $n$ (an exact path class). Equivalently, the disjoint union of exact complexity shells through shell $B$.
background
Module P2.3 of the Seven Gaps gravity stack builds the missing carrier equivalence behind CapShellCompatibility. At a fixed cap $B$, a bounded complex has unique exact complexity $\max(n_V,n_E,n_T)\le B$. Exact complexes live in uncapped shells; bounded complexes carry three inequality proofs that the counts sit under $B$.
ExactPathClass n is the exact complexity shell S1b: the disjoint union, over shell signatures of total complexity $n$, of the quotient of exact labeled complexes by global equivalence. No BoundedComplex B appears in that definition. Complexity itself is the shell coordinate $\max(n_V,\max(n_E,n_T))$.
The outer index uses Fin(B+1) so shell labels run through $0,\ldots,B$ without an off-by-one. The module then maps both ways, preserving incidence data and relabeling witnesses, and descends to the two quotient carriers.
proof idea
Pure type abbreviation: dependent sum $\Sigma, n:\mathrm{Fin}(B+1),,\mathrm{ExactPathClass},n$. No proof obligations. The local noncomputable Fintype instance on TriangulationClass B sits beside it only to state class sums later; it is not part of this definition.
why it matters
This is the exact-shell carrier in the headline equivalence capShellEquiv: bounded quotient classes at cap $B$ are identified with the disjoint union of exact shells $0,\ldots,B$. Forward and backward maps (boundedToShell, shellToCap, capToShell) and their inverse laws are typed against it.
Reindexing the finite quotient sum along that equivalence yields phasedZq_eq_exactComplexityCutoff: the phased capped sum equals the exact-shell cutoff through $B$. The bridge preserves automorphism cardinality and the $1/|\mathrm{Aut}|$ class measure. No continuum limit, convergence claim, or physical substrate phase is assumed; the object is purely combinatorial scaffolding for the Seven Gaps finite-sum identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.