instFiniteExactQuotient
plain-language theorem explainer
For fixed vertex, edge, and tetrahedron counts, the quotient of exact labeled complexes by global relabeling is a finite type. Gravity and path-sum arguments cite this when treating exact complexity shells as discrete configuration spaces. The proof is a one-line appeal to the standard finiteness of quotients of finite types.
Claim. For all $v,e,t\in\mathbb{N}$, the quotient of the type of exact complexes with those vertex, edge, and tetrahedron counts by the global-relabeling setoid is a finite type.
background
This module builds the path-sum configuration space as exact complexity shells (no size caps in the shell definition) and studies a Gaussian UV-regulated shell 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 $\rho\to 0^+$ remains open.
An exact complex with signature $(v,e,t)$ is a labeled complex whose vertex, edge, and tetrahedron counts equal those three naturals. Complexity of a bounded complex is $\max(n_V,n_E,n_T)$, the shell coordinate. Global equivalence is the relabeling relation on a fixed signature; exactSetoid packages it as a genuine setoid (refl/symm/trans via explicit relabelings).
The quotient by that setoid is the space of unlabeled exact classes at fixed $(v,e,t)$. Finiteness of that quotient is the discrete bookkeeping step before orbit-stabilizer and shell cardinality bounds.
proof idea
One-line wrapper: apply Mathlib's Quotient.finite to the exact setoid. That lemma only needs the carrier ExactComplex v e t to be finite, which it is (finite labeled data at fixed counts). No custom case analysis.
why it matters
Stage 1 of the module's proved shell structure (tagged S1b in the source): each exact signature quotient is finite, so exact shells are legitimate finite configuration spaces for the regulated path sum. Downstream, orbitCard_mul_autCard in RegulatorRemovalNoGo uses this finiteness in the exact orbit-stabilizer identity: orbit size times automorphism count equals the full gauge volume $v!,e!,t!$ for every labeled complex.
That identity is the combinatorial backbone for class measures $1/|\mathrm{Aut}|$ and for any later no-go or comparison about removing the UV regulator. Nothing here touches continuum limits, mesh refinement, or physical action derivation; those stay open or red in the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.