exactComplexity
plain-language theorem explainer
Assigns to every exact-size combinatorial complex a single natural number: the maximum of its vertex, edge, and tetrahedron counts. Gravity path-sum work cites it as the shell index that partitions the configuration space without size caps. The body is the three-argument max on the signature triple.
Claim. For an exact combinatorial complex with signature $(v,e,t)$ (exactly $v$ vertices, $e$ edges, $t$ tetrahedra, no size caps), its complexity is $\max(v,\max(e,t))$. The value depends only on the signature, not on incidence data.
background
This module rebuilds the quotient-class path-sum configuration space as exact complexity shells: no size caps appear in the shell definition. An exact complex is a structure with incidence maps for edges and tetrahedra at fixed counts $(v,e,t)$, deliberately free of the cross-cap identification issues that plague capped complexes.
Complexity here is the shell level used to grade configurations before the Gaussian UV regulator $\exp(-\rho n^2)$ is applied to the shell series. Sibling material already shows that the older capped complexity is relabeling-invariant; the exact version is defined so the same grading works without embedding into a bound $B$.
The module is explicit that the regulator is mathematical (not derived physics), the phase is a free invariant parameter, and regulator removal $\rho\to 0^+$ remains an open named hypothesis. Nothing here claims a continuum limit.
proof idea
Pure definition: ignore the complex datum and return $\max(v,\max(e,t))$. No lemmas, no tactics. Downstream uniqueness proofs simply unfold this definition and rewrite along signature equalities.
why it matters
Feeds the no-double-counting theorem: an exact complex can inhabit shell $n$ only when $n$ equals this complexity, so each configuration sits in exactly one shell. Combined with global equivalence living on a fixed signature, abstract complexes are not counted twice in the shell-resummed path sum.
Also bridges capped and exact pictures: the exact complexity of the image of a bounded complex equals the capped complexity, so entropy bounds and shell Fintype instances transfer cleanly.
In the Seven Gaps gravity stack this is Stage 1 shell structure under the honest protocol: it organizes the configuration space for the regulated series $Z_{\mathrm{RS}}^{\mathrm{uv}}$ without flipping continuum-limit ledger flags. It does not touch T0–T8 forcing, RCL, or the alpha band; it is combinatorial bookkeeping for the path-sum measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.