exactPathClass_card_le
plain-language theorem explainer
The exact complexity shell of size n has at most (n+1)^(12(n+1)) combinatorially distinct classes. Anyone bounding the Gaussian-UV path-sum shell term cites this entropy estimate. The proof multiplies a cubic signature count by a labeled-complex bound per signature, then loosens the total exponent to 12(n+1).
Claim. For every natural number $n$, the number of combinatorially distinct exact complexes of complexity exactly $n$ satisfies $\lvert \mathrm{ExactPathClass}(n)\rvert \le (n+1)^{12(n+1)}$.
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 the shell-resummed path sum with a hand-inserted Gaussian UV regulator $\exp(-\rho n^2)$. The action/phase is an arbitrary class-invariant parameter; regulator removal and continuum limits are explicitly open and not claimed here.
Complexity of a labeled complex is the total of vertices, edges, and tetrahedra. An exact complexity shell collects classes whose complexity is exactly $n$. Concretely, $\mathrm{ExactPathClass}(n)$ is the disjoint union, over shell signatures $(v,e,t)$ with $v+e+t=n$, of the quotient of the exact labeled class by global relabeling equivalence. No bounded-complex cap type appears in that definition.
Upstream counting inputs are the bound on the number of shell signatures and the bound on labeled exact complexes of fixed signature. The quotient cardinality is at most the labeled cardinality because the canonical map to the quotient is surjective.
proof idea
Fix $n$. For each shell signature $s$, the fiber cardinality (classes with that signature) is at most the labeled exact-complex count: surjectivity of $\mathrm{Quotient.mk}$ gives $\mathrm{card}(\mathrm{Quotient})\le\mathrm{card}(\mathrm{ExactComplex})$, and exactComplex_card_le supplies $\mathrm{card}(\mathrm{ExactComplex})\le(n+1)^{6(n+1)}$ from the Fin bounds on $v,e,t$.
Rewrite $\mathrm{card}(\mathrm{ExactPathClass},n)$ as a sum over signatures via Nat.card_sigma. Bound the sum by the constant fiber bound, factor out $\mathrm{card}(\mathrm{ShellSig},n)\cdot(n+1)^{6(n+1)}$, apply shellSig_card_le to replace the signature count by $(n+1)^3$, combine exponents $3+6(n+1)$, and finish with $3+6(n+1)\le 12(n+1)$ via omega.
why it matters
This is Stage 1c of the exact-shell Gaussian-UV program: the shell entropy bound that makes the regulated series controllable. Downstream, norm_zRSUVShell_le_entropy multiplies the per-class modulus bound by this cardinality estimate, yielding $|Z_n|\le e^{-\rho n^2}(n+1)^{12(n+1)}$, which feeds summability for every $\rho>0$.
The status structure ExactShellGaugeUVStatus records entropy_bound_proved, and exactShellGaugeUVStatus_grounded ties that flag to the universal quantification of this inequality. In the Seven Gaps gravity ledger this is combinatorial scaffolding for a mathematical UV regulator, not derived continuum physics: continuum-limit and regulator-removal flags stay false by design.
Within Recognition Science gravity work, the bound is the discrete entropy control that lets shell-resummed path sums converge before any continuum or physical-action claim is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.