relabelTriple_card
plain-language theorem explainer
The full relabeling gauge group at signature (v,e,t) has order v! e! t!. Anyone counting labeled complexes modulo vertex/edge/tetrahedron permutations cites this as the gauge volume. The proof multiplies the three symmetric-group orders via product cardinality.
Claim. For all natural numbers $v,e,t$, the set of triples of bijections $(\mathrm{Sym}(v)\times\mathrm{Sym}(e)\times\mathrm{Sym}(t))$ is finite of cardinality $v!\,e!\,t!$.
background
In the Seven Gaps regulator-removal module, exact complexes are labeled by finite vertex, edge, and tetrahedron index sets of sizes $v$, $e$, and $t$. The full gauge group of pure relabelings is the product of the three symmetric groups on those index sets (the relabeling triple). Its order is the gauge volume that appears in the shell-mass identity: the sum of $1/|\mathrm{Aut}|$ over unlabeled classes equals the labeled count divided by $v!,e!,t!$.
That identity is the Burnside/orbit-stabilizer route used to show shell mass diverges, which in turn refutes regulator removal of the Gaussian-regulated path sum at zero phase. The present lemma is the elementary counting step that pins the denominator.
proof idea
Three local facts: $|\mathrm{Sym}(n)|=n!$ for $n\in{v,e,t}$, each obtained by rewriting the card of equivalences of $\mathrm{Fin},n$ against the identity equivalence and using $|\mathrm{Fin},n|=n$. Then apply product cardinality twice to the triple product type and finish by ring normalization of the product of factorials.
why it matters
Feeds sum_card_relabel, which states that summing the number of exact relabelings out of a fixed base complex over all target complexes exhausts the triple group. That sum is the first half of the shell-mass identity (labeled count over gauge volume) used throughout the zero-phase no-go: shell mass is unbounded because labeled entropy beats the factorial gauge volume on the diagonal signature $(n,n,n)$. Without this cardinality, the orbit-stabilizer splitting and the lower bound $\mathrm{shellMass},n\ge n^{3n}$ do not close. The module still leaves oscillatory (nonzero-phase) regulator removal open; this lemma is phase-independent bookkeeping only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.