instFintypeTriangulationClass
plain-language theorem explainer
For each bound B, the quotient of labeled bounded complexes by relabeling is finitely enumerable. Anyone writing a class sum over combinatorially distinct triangulations needs this instance. The construction is a one-line lift of the already-proved finiteness of that quotient to a Fintype structure via ofFinite.
Claim. For every natural number $B$, the set of triangulation classes of bound $B$ (labeled bounded complexes modulo relabeling isomorphism) carries a finite-type structure: it is finitely enumerable in the noncomputable sense.
background
In the Seven Gaps gauge-preflight setting, PathSumMeasure postulates the discrete-gravity symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$. This module instead derives that factor from pure gauge counting: orbit size (labeled copies equivalent to $K$), pair count (copy-plus-relabeling-witness volume), and the class mass defined as labeled copies per unit gauge volume.
A triangulation class is the quotient of the labeled scoped complexes of bound $B$ by the relabeling setoid. The module already records that this quotient is finite. Class sums such as $Z=\sum_c \mathrm{orbitCard}(c)\cdot\mathrm{gaugeOrbitMass}(c)\cdot w(\mathrm{rep},c)$ are only stateable once the quotient is treated as a finite type, so an enumeration instance is required even though the underlying finiteness theorem does the real work.
proof idea
One-line wrapper: apply Fintype.ofFinite to the prior finiteness result on the triangulation-class quotient. No new combinatorial argument; the instance only packages that finiteness into the typeclass Lean needs for finite sums and cardinality notation over classes.
why it matters
The instance is scaffolding for the class-sum form of the path measure, where the $1/|\mathrm{Aut}|$ weight is replaced by the counting-derived gauge orbit mass. Downstream, CapShellBridge reuses the same pattern for shells up to $B$ (exact path classes indexed by complexity at most $B$), so shell-level sums inherit the finite enumeration.
Within the gravity Seven Gaps program this is bookkeeping, not a physical claim: it lets the derivation theorem (counting mass equals $\mu$) and the diagnostic identity $Z=\sum_c \mathrm{orbitCard},c\cdot\mathrm{gaugeOrbitMass},c\cdot w(\mathrm{rep},c)$ be written as genuine finite sums. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it only makes the discrete-gravity class calculus well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.