ExactComplex
plain-language theorem explainer
An exact-size combinatorial 3-complex is a labeled incidence structure with precisely v vertices, e edges, and t tetrahedra, and no upper-bound caps on those counts. Gravity path-sum work cites it as the cap-free configuration type underlying exact complexity shells. The declaration is a bare structure: two incidence maps and nothing else.
Claim. For natural numbers $v$, $e$, and $t$, an exact complex of signature $(v,e,t)$ consists of an edge-incidence map $E\colon \{0,\ldots,e-1\}\to \{0,\ldots,v-1\}^2$ and a tetrahedron-incidence map $T\colon \{0,\ldots,t-1\}\to \{0,\ldots,v-1\}^4$. There are no size inequalities and no embedding into a capped ambient class.
background
The Seven Gaps gravity stack organizes the quotient-class path-sum configuration space into exact complexity shells and studies a Gaussian-UV-regularized shell series. Module honesty rules are binding: the regulator $\exp(-\rho n^2)$ is inserted by hand, the phase is an arbitrary class-invariant parameter, and regulator removal ($\rho\to 0^+$) remains a named open.
An exact complex is the cap-free configuration type: fixed finite index sets for vertices, edges, and tets, with abstract incidence only. Upstream geometry supplies concrete incidence tables of the same shape (Freudenthal cube edge and tet vertex lists); those are specializations, not part of the abstract type. The companion bounded complex carries cap inequalities $n_V,n_E,n_T\le B$; exact complexes deliberately omit those inequalities so cross-cap identification cannot arise.
Complexity of a labeled complex is the sum of the three counts. Exact shells group complexes by that integer complexity, then quotient by relabeling of the three index sets.
proof idea
No proof: this is a structure declaration. The data are exactly two fields, the edge-incidence map edgeVerts : Fin e → Fin v × Fin v and the tet-incidence map tetVerts : Fin t → Fin 4 → Fin v. Downstream code treats the pair as raw incidence data via the equivalence that sends a complex to (edgeVerts, tetVerts) and rebuilds by the structure constructor.
why it matters
Exact complexes are the Stage-1 carrier for the exact-shell path-sum program in this module. Automorphisms are exact self-relabelings; the discrete-gravity measure on a labeled complex is $1/|\mathrm{Aut}|$. Finiteness of each exact path class, the shell entropy bound $\mathrm{card}\le (n+1)^{12(n+1)}$, and the regulated shell series all sit on this type.
The CapShellBridge maps attach a cap $B\ge n$ to an exact complex of shell index $n$, send exact relabelings to bounded relabelings, and prove that forgetting the cap recovers the original exact-shell class. That bridge is how exact shells talk to the older capped configuration space without importing cap artifacts into the shell definition.
Nothing here is continuum physics: complexity is not mesh refinement, and the module flips no FullTheoryLedger continuum flag. The type only clears the combinatorial ground for the UV-regularized shell sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.