exactComplex_card_le
plain-language theorem explainer
When an exact complex has at most n+1 vertices, edges, and tetrahedra, the number of labeled incidence configurations is at most (n+1)^{6(n+1)}. Gravity path-sum work cites this as the per-signature labeled entropy bound feeding the shell cardinality estimate. The proof rewrites the exact card formula and bounds the edge and tet labeling factors separately by elementary power inequalities.
Claim. Let $v,e,t,n\in\mathbb{N}$ with $v\le n+1$, $e\le n+1$, and $t\le n+1$. Then the number of exact combinatorial complexes with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra (incidence maps $\mathrm{Fin}\,e\to\mathrm{Fin}\,v\times\mathrm{Fin}\,v$ and $\mathrm{Fin}\,t\to\mathrm{Fin}\,4\to\mathrm{Fin}\,v$) satisfies $\lvert\mathrm{ExactComplex}(v,e,t)\rvert\le(n+1)^{6(n+1)}$.
background
This module packages the quotient-class path-sum configuration space into exact complexity shells (no size caps in the shell type) and studies a Gaussian-UV-regulated path sum. Honesty constraints are explicit: the regulator $\exp(-\rho n^2)$ is inserted by hand, the phase is a free class function, and regulator removal remains open.
An exact complex of signature $(v,e,t)$ is a pure incidence structure: edge endpoints in $\mathrm{Fin},v\times\mathrm{Fin},v$ and tetrahedron vertices $\mathrm{Fin},4\to\mathrm{Fin},v$, with no ambient bound $B$. Relabeling is defined independently of the capped BoundedComplex story, so cross-cap identification issues do not arise.
The labeled count factors as edge labelings times tet labelings. With $v\le n+1$, there are at most $(v^2)^e$ edge maps and $(v^4)^t$ tet maps. The present bound converts those size hypotheses into a uniform polynomial-exponential majorant in $n$ alone, which Stage 1 needs before quotienting by relabeling.
proof idea
Start from the exact cardinality identity (card equals $(v\cdot v)^e\cdot(v^4)^t$). Bound the edge factor: $(v\cdot v)^e\le((n+1)^2)^e=(n+1)^{2e}\le(n+1)^{2(n+1)}$ by $v\le n+1$, $e\le n+1$, and monotonicity of powers. Bound the tet factor: $(v^4)^t\le((n+1)^4)^t=(n+1)^{4t}\le(n+1)^{4(n+1)}$ the same way. Multiply the two inequalities and add exponents: $2(n+1)+4(n+1)=6(n+1)$. Pure Nat arithmetic; no geometry or physics enters.
why it matters
This is the labeled half of Stage 1 shell entropy (S1c). Downstream, exactPathClass_card_le multiplies it by the number of shell signatures ($\le(n+1)^3$) and uses that quotient card is at most labeled card, obtaining $\mathrm{card}(\mathrm{ExactPathClass},n)\le(n+1)^{12(n+1)}$. That shell entropy bound is what makes the Gaussian-regulated shell series summable for every $\rho>0$.
In the Seven Gaps gravity program this is combinatorial bookkeeping, not continuum physics: the module flips no continuum-limit ledger flag, and regulator removal stays open. The bound is still load-bearing: without a uniform majorant on labeled exact complexes, the shell-resummed UV path sum cannot be shown summable.
It also supports the bridge from capped complexes via complexity agreement of the exact image, keeping capped and exact counting languages interchangeable at the complexity level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.