ExactPathClass
plain-language theorem explainer
The exact complexity shell at level n is the set of combinatorially distinct exact complexes whose complexity is exactly n. It is the disjoint union, over shell signatures with max count n, of exact labeled complexes modulo global relabeling. Anyone building shell-resummed path sums or transporting phases to capped carriers cites this type. The body is a one-line sigma-plus-quotient packaging, not a proof.
Claim. For each $n \in \mathbb{N}$, the exact complexity shell is $\bigsqcup_{s} \bigl(\mathrm{ExactComplex}(v_s,e_s,t_s)/{\sim}\bigr)$, where $s$ runs over shell signatures $(v_s,e_s,t_s)$ with each count at most $n$ and $\max(v_s,e_s,t_s)=n$, and $\sim$ is global relabeling equivalence on exact labeled complexes. No size-cap carrier appears.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells with no size caps in the shell definition, then studies a Gaussian-UV-regulated shell series. Honesty tags: the regulator $\exp(-\rho n^2)$ is inserted by hand; the phase is an arbitrary class-invariant parameter; regulator removal remains a named open.
A shell signature at level $n$ is a triple $(v,e,t)$ of vertex, edge, and tetrahedron counts, each at most $n$, with maximum exactly $n$, packaged in finite types so the signature space is finite. Exact complexes of fixed counts $(v,e,t)$ carry the global-relabeling relation, which is a genuine setoid (reflexive, symmetric, transitive via explicit relabelings).
The exact shell is the dependent sum of those quotients over all signatures at level $n$. Complexity is the max of the three counts; the shell collects every combinatorial type whose complexity is exactly $n$, without any bounded-complex cap.
proof idea
Definitional packaging only. The type is the sigma type of a shell signature $s$ together with an element of the quotient of exact complexes of counts $(\mathrm{sig}V,s,\mathrm{sig}E,s,\mathrm{sig}T,s)$ by the exact setoid (global equivalence). No tactics or lemmas fire; the meaning is entirely in the upstream setoid and signature abbreviations.
why it matters
This is Stage 1b of the exact-shell program: the carrier on which shell entropy bounds, Fintype instances, per-class measures $1/|\mathrm{Aut}|$, and the regulated shell series live. Downstream, CapShellBridge transports arbitrary phases on exact shells to capped carriers (phaseModelAtCap, capPhaseFamily), proves finite-sum reindexing (phasedZq_eq_exactComplexityCutoff), and closes the missing CapShellCompatibility blocker. Automorphism cardinalities and shell-up-to sums are indexed on this type.
In the Seven Gaps gravity stack it separates exact combinatorial shells from capped triangulation classes, so UV-regulated path sums can be stated without smuggling mesh caps into the configuration space. It does not flip continuum-limit or FullTheoryLedger flags; those stay open by module protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.