instFiniteExactRelabel
plain-language theorem explainer
Any two exact complexes of the same signature admit only finitely many relabeling isomorphisms. Gravity and combinatorial-gauge arguments that count orbits or apply Burnside need this finiteness off the diagonal Aut case. The proof injects the witness type into the finite triple of vertex/edge/tet index bijections.
Claim. For any signature $(v,e,t)$ and any two exact complexes $K,K'$ of that signature, the type of exact relabelings $K\to K'$ is finite.
background
This module sits in the Seven Gaps gravity stack and establishes a kernel no-go: the Gaussian-regulated quotient path sum $Z_{\mathrm{RS},\mathrm{uv}}$ has no $\rho\to 0^+$ limit at zero phase. The quantitative engine is a shell-mass identity via Burnside/orbit-stabilizer: summing $1/|\mathrm{Aut}|$ over quotient classes equals the labeled count divided by the full relabeling gauge volume $v!,e!,t!$.
An exact complex is a cap-free combinatorial complex with exactly $v$ vertices, $e$ edges and $t$ tetrahedra, given by incidence maps on finite index sets. An exact relabeling between two such complexes is a triple of bijections of those index sets that intertwines the incidence data. The automorphism group is the diagonal case (relabelings of a complex onto itself).
Finiteness of the diagonal was already available; the present instance extends it to arbitrary pairs $K,K'$. Upstream, toEquivTriple_injective records that a relabeling is uniquely determined by (and injects into) its triple of index bijections, each of which ranges over a finite symmetric group.
proof idea
One-line instance: apply Finite.of_injective to the map that sends an exact relabeling to its underlying triple of index equivalences, using injectivity of that map (ExactRelabel.toEquivTriple_injective). The codomain is a product of finite types (Equiv (Fin v) (Fin v), and likewise for edges and tets), hence finite; an injective image of a finite type is finite.
why it matters
Shell-mass and orbit-counting arguments in this module treat the full sigma of relabelings out of a fixed base complex, not only automorphisms. Finiteness of every fiber ExactRelabel K K' is the typeclass fact that lets cardinalities, orbit-stabilizer (orbitCard_mul_autCard), the torsor equivalence with ExactAut, and the Burnside identity sum_classMuOn_eq_card_div_factorials be stated in Lean without partiality.
That identity feeds the lower bound shellMass n \ge n^{3n} on the single signature $(n,n,n)$, which forces shell-mass divergence and the headline refutation $\neg\mathrm{HasZRSRegulatorRemoval}(\mathrm{zeroPhase})$. The instance itself is scaffolding-level infrastructure rather than a physics claim: it generalizes diagonal finiteness of ExactAut so the gauge-volume denominators $v!,e!,t!$ are well-defined for every pair of exact complexes.
No downstream edges are recorded on the page; sibling lemmas (orbitCard, sum_card_relabel, relabelSigmaEquiv, torsorEquiv) are the natural consumers inside the same no-go chain. Oscillatory (nonzero-phase) regulator removal remains open and is untouched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.