exactSetoid
plain-language theorem explainer
Global equivalence of exact-size combinatorial complexes (fixed vertex, edge, and tetrahedron counts) is a setoid: reflexive, symmetric, and transitive via explicit index relabelings. Anyone building the exact complexity shell or the per-class path-sum measure cites this as the quotient relation. The proof packages reflexivity, symmetry, and transitivity of ExactRelabel into Mathlib's Setoid structure.
Claim. For every triple of natural numbers $(v,e,t)$, the relation "there exists an exact relabeling isomorphism" on the type of exact combinatorial complexes with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra is an equivalence relation, hence defines a setoid on that type.
background
This module organizes the path-sum configuration space into exact complexity shells with no size caps, and studies a Gaussian-UV-regularized shell sum. An ExactComplex v e t is a cap-free labeled complex: incidence data for exactly $v$ vertices, $e$ edges, and $t$ tetrahedra, with no bound inequalities. Because there is no cap, the cross-cap identification issues of bounded complexes cannot arise.
An exact relabeling is a triple of bijections of the vertex, edge, and tetrahedron index sets that commute with the incidence maps. Two complexes of the same signature are globally equivalent when such a relabeling exists; different signatures cannot be related, since a vertex bijection forces equal vertex counts.
The local Stage-1 goal is to make each exact signature into a genuine quotient type so that shell classes, automorphism counts, and the per-class measure $1/|\mathrm{Aut}|$ are well-defined without embedding into any capped type.
proof idea
One-line packaging of the three setoid laws already proved for exact relabelings. Reflexivity sends each complex $K$ to the witness ExactRelabel.refl K. Symmetry unwraps a nonempty relabeling and applies symm. Transitivity unwraps two successive nonempty relabelings and composes them with trans. The resulting triple is the iseqv field of Mathlib's Setoid on ExactComplex v e t, with relation GlobalEquivalent.
why it matters
This is the Stage-1 setoid theorem named in the module doc: without it there is no exact-shell quotient. Downstream, ExactPathClass n is the disjoint union over shell signatures of Quotient (exactSetoid ...), and the shell entropy bound exactPathClass_card_le counts those quotients. The per-class measure classMuOn is the lift of the labeled measure along this setoid.
The CapShellBridge uses the same setoid to move between capped triangulation classes and exact shells: exactClassToCap is a Quotient.lift over exactSetoid, while classMu_capToShell and shellAutCard_capToShell prove measure and automorphism-card preservation after Quotient.mk (exactSetoid ...).
In the broader Seven Gaps program this is pure combinatorial scaffolding for the regulated path sum. It does not touch continuum limits, regulator removal (HasZRSRegulatorRemoval stays open), or any FullTheoryLedger flag. It sits upstream of the Gaussian-UV summability results, not of the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.