exactComplex_card_eq
plain-language theorem explainer
At fixed signature (v,e,t), the number of exact combinatorial complexes equals (v²)^e·(v⁴)^t: one ordered vertex pair per edge and one 4-tuple per tetrahedron. Path-sum shell entropy bounds and Burnside mass formulas cite this as the labeled count before gauge quotient. Proof transfers cardinality through the raw incidence-code equivalence, then applies standard Fin/function/product card lemmas.
Claim. For all $v,e,t\in\mathbb{N}$, the number of exact-size combinatorial complexes with exactly $v$ vertices, $e$ edges and $t$ tetrahedra equals $(v\cdot v)^e\cdot(v^4)^t$.
background
An exact complex of signature $(v,e,t)$ is a cap-free incidence structure: a map from $e$ edge indices to ordered pairs in a $v$-vertex set, together with a map from $t$ tetrahedron indices to 4-tuples of vertices. There are no size inequalities in the type, so the cross-cap identification issues of bounded complexes cannot arise.
This module organizes the quotient-class path-sum configuration space into exact complexity shells and studies a Gaussian-UV-regularized path sum. Honesty constraints are binding: 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 a named open.
The counting identity rests on a finite code equivalence that identifies each exact complex with the raw pair of incidence maps (edge labels times tet labels). That equivalence is definitional and bijective on the nose.
proof idea
One short term proof. Rewrite the card via Fintype.card_congr along the code equivalence exactCodeEquiv, which sends an exact complex to the product of its edge-vertex map and tet-vertex map. Then simp with the standard lemmas Fintype.card_prod, Fintype.card_fun, and Fintype.card_fin expands:
- $|\mathrm{Fin},e\to\mathrm{Fin},v\times\mathrm{Fin},v|=(v\cdot v)^e$,
- $|\mathrm{Fin},t\to(\mathrm{Fin},4\to\mathrm{Fin},v)|=(v^4)^t$.
No combinatorial case split is needed; the count is pure finite-type arithmetic on the incidence code.
why it matters
This is the exact labeled entropy at a fixed shell signature, Stage 1 of the seven-gaps shell structure. Downstream, exactComplex_card_le turns it into the uniform bound $|\mathrm{ExactComplex},v,e,t|\le(n+1)^{6(n+1)}$ whenever $v,e,t\le n+1$, which feeds the shell entropy estimate on exact path classes.
It also supplies the numerator in burnsideMass_eq_pow: Burnside mass equals the labeled count divided by $v!,e!,t!$. That mass lower-bounds shell mass in shellMass_lower ($\mathrm{shellMass},n\ge n^{3n}$), used in regulator-removal no-go arguments.
Within Recognition gravity, this is bookkeeping for the discrete configuration space of the path sum, not a continuum or physical action claim. It does not touch T0–T8 forcing, RCL, or the alpha band; it only closes the labeled-count step needed before gauge quotient and UV-regulated summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.