instFintypeExactPathClass
plain-language theorem explainer
For every natural number n, the exact complexity shell of level n is a finite type: only finitely many combinatorially distinct exact complexes have complexity exactly n. Path-sum and shell-entropy arguments in the Seven Gaps gravity stack cite this as Stage 1b. The proof is a one-line appeal to finiteness of the underlying sigma-quotient type via Fintype.ofFinite.
Claim. For every $n \in \mathbb{N}$, the exact complexity shell of level $n$ (the disjoint union, over shell signatures of complexity $n$, of the quotients of exact labeled complexes by global relabeling equivalence) carries a finite-type structure.
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-regularized path sum. Honesty constraints are explicit: the regulator $\exp(-\rho n^2)$ is inserted by hand, the action/phase is a free parameter on classes, and regulator removal ($\rho \to 0^+$) remains open.
Complexity of a complex is the max of its vertex, edge, and tetrahedron counts; that integer is the shell coordinate. The exact complexity shell at level $n$ is defined as $\Sigma_{s : \mathrm{ShellSig}, n}, Q_s$, where $Q_s$ is the quotient of the exact labeled class with signature $s$ by the global-equivalence setoid. No bounded-complex cap type appears in that definition.
Stage 1 of the module proves shell structure: complexity is relabeling-invariant, the exact setoid is genuine, each shell is a Fintype, a polynomial entropy bound holds, and every shell is inhabited (witness: $n$ isolated vertices, with no simpliciality claim).
proof idea
One-line wrapper. The instance is obtained by Fintype.ofFinite _, transferring a prior Finite instance on ExactPathClass n (the sigma over shell signatures of the global-equivalence quotient) into a Fintype instance. No new combinatorial counting is performed here; finiteness of the sigma-quotient is taken as already established and packaged for card and summation APIs.
why it matters
This is THEOREM (S1b) in the module's Stage 1 checklist: each exact complexity shell is a finite type. Downstream, ExactShellGaugeUVStatus records shell_structure_proved as grounded partly on this instance together with complexity congruence, the exact setoid, shell-index uniqueness, and the relax map to exact complexes.
Finiteness is the gate for the shell entropy bound $\lvert\mathrm{ExactPathClass}, n\rvert \le (n+1)^{12(n+1)}$ and for well-defined per-class measures and regulated shell terms. Without a Fintype on each shell, the Gaussian-UV shell series and its summability for every $\rho > 0$ cannot even be stated in the Lean card/summation style used here.
It does not touch continuum physics: complexity cutoff is not mesh refinement, continuum-limit flags stay false, and no FullTheoryLedger flag is flipped. The result is pure combinatorial bookkeeping inside the Seven Gaps gravity path-sum stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.