instFintypeExactQuotient
plain-language theorem explainer
At fixed signature (v,e,t), the quotient of exact complexes by global relabeling is a finite type, via noncomputable enumeration. Anyone writing finite sums of per-class measures over that gauge quotient needs this instance. The proof is a one-line lift from the existing Finite instance through Fintype.ofFinite.
Claim. For all $v,e,t\in\mathbb{N}$, the quotient of exact complexes of signature $(v,e,t)$ by the global-relabeling setoid admits a noncomputable finite enumeration (a $\mathrm{Fintype}$ structure).
background
This module is the kernel no-go for regulator removal at zero phase: the Gaussian-regulated path sum $Z_{\mathrm{RS},\mathrm{uv}}$ has no $\rho\to 0^+$ limit when the phase is identically zero. The argument routes through shell masses, which are sums of per-class measures $1/|\mathrm{Aut}|$ over the gauge quotient of exact complexes.
An exact complex of signature $(v,e,t)$ is a labeled combinatorial shell object. Global equivalence is the relation generated by relabelings of vertices, edges, and types; exactSetoid packages that relation as a genuine setoid (refl/symm/trans via explicit relabelings). The quotient is therefore the space of exact shells up to gauge.
The per-class measure classMuOn is the descent of the labeled measure to that quotient (via Quotient.lift). Finite sums and cardinalities over the quotient require a Fintype instance; finiteness itself is already supplied by a sibling Finite instance.
proof idea
One-line wrapper: apply Fintype.ofFinite to the already-established Finite structure on the same quotient. No new combinatorial argument appears here; enumeration is noncomputable classical choice from finiteness.
why it matters
Shell-mass identities in this module equate the sum of per-class measures over the quotient to the labeled count divided by the full relabeling volume $v!,e!,t!$. Those sums are only well-typed once the quotient is a finite type. The same finiteness underwrites the Burnside/orbit-stabilizer route (torsor equivalence, orbit-card splitting, fiber sums) that proves shell-mass divergence and, with positivity at zero phase, the headline refutation $\neg\mathrm{HasZRSRegulatorRemoval}(\mathrm{zeroPhase})$.
This instance is infrastructure, not a physics claim: it does not touch oscillatory phases (still open) and does not itself bound shell mass. It simply makes the discrete gauge quotient summable in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.