actRelabel
plain-language theorem explainer
Canonical witness that a relabeling triple σ takes an exact complex K to its pushforward act(σ,K) by incidence-preserving index equivalences. Cited wherever the relabeling gauge acts on labeled shell data en route to the Burnside shell-mass identity. Construction is definitional: unpack σ into vertex/edge/tet equivalences and cancel symm-apply on the incidence maps.
Claim. For any relabeling triple $\sigma$ (independent permutations of the vertex, edge, and tetrahedron index sets of signature $(v,e,t)$) and any exact complex $K$ of that signature, there is a canonical exact-relabeling witness from $K$ to the pushforward complex $\mathrm{act}(\sigma,K)$ whose three component equivalences are exactly the three factors of $\sigma$, and which intertwines edge and tetrahedron incidence data.
background
This module is the kernel no-go for regulator removal of the Gaussian-regulated RS path sum at zero phase. The quantitative engine is a shell-mass identity: the sum of per-class measures $1/|\mathrm{Aut}|$ over the quotient equals the labeled count divided by the full relabeling gauge volume $v!\cdot e!\cdot t!$. That identity is proved by realizing the relabeling-triple group as a torsor over the sigma of all relabelings out of a fixed base complex.
A relabeling triple is the product of the three symmetric groups on the vertex, edge, and tetrahedron index sets. An exact complex packages the incidence data (which vertices bound each edge, which vertices bound each tetrahedron). The pushforward action applies the three permutations to that incidence data. An exact-relabeling witness is a triple of equivalences together with the two commutation identities that say incidence is preserved.
The present definition supplies the tautological witness from $K$ to its own pushforward under $\sigma$: the equivalences are just the factors of $\sigma$ itself.
proof idea
Definitional structure instance, not a multi-step argument. The three equivalence fields are the three projections of $\sigma$. The edge-commutation obligation reduces, after unfolding the pushforward, to an identity of the form $\mathrm{map}(\sigma_v,\sigma_v)\circ E\circ(\sigma_e^{-1}\circ\sigma_e)=\mathrm{map}(\sigma_v,\sigma_v)\circ E$, discharged by Equiv.symm_apply_apply. The tetrahedron-commutation obligation is the same one-line cancellation on the tet incidence map.
why it matters
This is the forward map of the total torsor relabelSigmaEquiv: every triple $\sigma$ produces the pair $(\mathrm{act}(\sigma,K),\mathrm{actRelabel},\sigma,K)$, and every relabeling pair arises from exactly one triple. That torsor is the first step of the Burnside/orbit-stabilizer route to the shell-mass identity (sum_classMuOn_eq_card_div_factorials), which in turn feeds the shell-mass lower bound and the headline zero-phase no-go (not_hasZRSRegulatorRemoval_zeroPhase).
Without a concrete witness that pushforward really is an exact relabeling, the sigma type of relabelings out of a fixed base cannot be identified with the factorial gauge volume $v!\cdot e!\cdot t!$. The definition is therefore load-bearing infrastructure for the proved kernel no-go, while remaining silent on the still-open oscillatory-phase removal question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.