sum_card_relabel
plain-language theorem explainer
For any fixed exact complex of signature (v,e,t), the sum over all target complexes of the number of relabeling isomorphisms equals the full gauge volume v!·e!·t!. Gravity and combinatorial-gauge workers cite it as the counting identity that exhausts the triple group before orbit-stabilizer. The proof is a short calc: sigma-card, congruence via the relabeling-sigma equivalence, then the factorial count of RelabelTriple.
Claim. Fix nonnegative integers $v,e,t$ and an exact complex $K$ with exactly $v$ vertices, $e$ edges and $t$ tetrahedra. Then $\sum_{K'} |\mathrm{ExactRelabel}(K,K')| = v!\, e!\, t!$, where the sum runs over all exact complexes $K'$ of the same signature and $\mathrm{ExactRelabel}(K,K')$ is the set of incidence-preserving bijections of the three index sets.
background
The ambient module is the Seven Gaps regulator-removal no-go: it shows that 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 obtained by Burnside/orbit-stabilizer on exact (cap-free) complexes.
An ExactComplex of signature $(v,e,t)$ is a combinatorial complex with exactly $v$ vertices, $e$ edges and $t$ tetrahedra, given by incidence maps and no cap inequalities. An ExactRelabel between two such complexes is a triple of bijections on the vertex, edge and tetrahedron index sets that intertwines the incidence data. The full labeled gauge group is the product of symmetric groups on those three index sets (the relabeling triple), whose cardinality is $v!,e!,t!$.
Upstream, relabelSigmaEquiv identifies the sigma-type of all relabelings out of a fixed base complex with that triple group, realizing the group as a torsor over the fibers. The present sum is the global counting form of that identification.
proof idea
Term-mode calc chain with four equalities. First, Nat.card_sigma.symm rewrites the sum of fiber cardinalities as the cardinality of the dependent sum $\Sigma_{K'},\mathrm{ExactRelabel}(K,K')$. Second, Nat.card_congr along the inverse of relabelSigmaEquiv K transports that sigma-type onto RelabelTriple v e t. Third, Nat.card_eq_fintype_card switches to Fintype.card. Fourth, relabelTriple_card evaluates the triple as $v!,e!,t!$. No induction or case split; pure finite-cardinality transport.
why it matters
This is the global counting step in the shell-mass / Burnside route of the zero-phase regulator-removal no-go. Downstream, orbitCard_mul_autCard rewrites through the orbit-restricted form and obtains the exact orbit-stabilizer identity: orbit size times automorphism count equals $v!,e!,t!$ for every labeled complex. That identity feeds sum_classMuOn_eq_card_div_factorials, which equates the sum of per-class measures $1/|\mathrm{Aut}|$ over the quotient to the labeled count divided by the gauge volume, and thence the shell-mass lower bound that diverges as $n^{3n}$.
In the module narrative this closes the "exhausts the triple group" half of the torsor picture before fiberwise orbit-stabilizer. It does not touch oscillatory phases: the headline no-go remains zero-phase only; nonzero-phase regulator removal stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.