orbitCard_mul_autCard
plain-language theorem explainer
Orbit size times automorphism order equals the full relabeling gauge volume v!·e!·t! for every labeled exact complex of signature (v,e,t). Anyone running the Burnside route to the shell-mass identity in the zero-phase regulator no-go cites this exact orbit-stabilizer form. The proof is a two-line rewrite: orbit card equals the summed relabeling-fiber cards, which total the factorial product.
Claim. For every labeled exact complex $K$ of signature $(v,e,t)$, the product of its orbit cardinality under the relabeling action with the order of its automorphism group equals the full gauge volume: $|\mathrm{Orb}(K)|\cdot|\mathrm{Aut}(K)|=v!\,e!\,t!$.
background
The ambient module is the kernel no-go for regulator removal of the Gaussian-regulated quotient path sum at zero phase. Exact complexes are the labeled combinatorial objects of fixed signature $(v,e,t)$; the gauge group is the product of symmetric groups acting by independent relabelings of the three index sets, so the full gauge volume is $v!,e!,t!$.
An orbit is the set of all complexes reachable from a fixed labeled $K$ by relabeling; the stabilizer is the automorphism group of label-preserving symmetries of $K$. Sibling constructions realize the space of all relabeling triples out of a fixed base as a torsor over the sigma-type of outgoing relabelings, so fiberwise orbit-stabilizer applies. The typed automorphism group and labeled complex type come from the ExactShellGaugeUV layer.
proof idea
Two-line term proof. Rewrite the left-hand side by the identity that orbit cardinality equals the sum of fiber cardinalities of the relabeling sigma-type over the orbit. Then apply the global counting lemma that those fiber cards, summed over all relabelings of $K$, equal the full factorial product $v!,e!,t!$. The composition is exact orbit-stabilizer for every labeled complex.
why it matters
Fiberwise orbit-stabilizer step in the Burnside route to the shell-mass identity. Downstream, the headline identity equates the sum of per-class measures $1/|\mathrm{Aut}|$ over the quotient to the labeled count divided by $v!,e!,t!$, by splitting the relabeling torsor with this lemma and summing orbits. That identity feeds the lower bound $\mathrm{shellMass},n\ge n^{3n}$ and the zero-phase no-go: the regulated path sum has no $\rho\to 0^+$ limit because shell masses diverge and every term is nonnegative. Phase-independent combinatorics; oscillatory removal remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.