sigma_relabel_ext
plain-language theorem explainer
Two pairs (target exact complex, relabeling witness) out of a fixed base are equal once the witness vertex, edge, and tetrahedron index bijections agree; the target is forced by the commutation equations. Anyone building the total torsor of exact-complex relabelings cites this extensionality. The proof recovers the target edge and tet maps from those equations, then applies exact-complex and relabel extensionality.
Claim. Fix an exact complex $K$ of signature $(v,e,t)$. Let $p=(K',r)$ and $q=(K'',s)$ be pairs in which $r$ (resp. $s$) is an exact relabeling $K\to K'$ (resp. $K\to K''$). If the three index bijections of $r$ and $s$ agree on vertices, edges, and tetrahedra, then $p=q$.
background
This module sits in the Seven Gaps gravity stack and proves a kernel no-go: the Gaussian-regulated quotient path sum has no $\rho\to 0^+$ limit at zero phase. The quantitative engine is a shell-mass identity obtained by realizing the relabeling-triple group as a torsor over the sigma of all exact relabelings out of a fixed base complex, then applying orbit-stabilizer fiberwise.
An exact complex of signature $(v,e,t)$ is a labeled combinatorial complex with $v$ vertices, $e$ edges, and $t$ tetrahedra together with incidence data. An exact relabeling between two such complexes is a triple of index bijections (vertices, edges, tetrahedra) that intertwines those incidence maps: edge-commutation and tet-commutation. The total relabeling sigma packages every pair (target complex, witness relabeling) out of a fixed base $K$.
The sibling lemma exactComplex_ext says two exact complexes are equal once their edge and tet incidence maps agree pointwise. The present result lifts that to the sigma: equal witness bijections force equal targets, hence equal pairs.
proof idea
Destructure $p=(K_1,r_1)$ and $q=(K_2,r_2)$. To show $K_1=K_2$, apply exact-complex extensionality. For edges: evaluate each witness's edge-commutation at the inverse edge index, cancel the inverse-apply, and transport along the assumed equality of vertex and edge bijections. For tetrahedra: the same pattern with tet-commutation and the vertex/tet bijections. After substituting $K_1=K_2$, finish by congruence of Sigma.mk and exact-relabel extensionality on the three equal bijections.
why it matters
This is the uniqueness half of the total torsor. Downstream, relabelSigmaEquiv builds the bijection between the full relabeling-triple group and the sigma of all relabelings out of a fixed base: pushforward of a triple is the forward map, and the inverse sends a pair to its witness triple; the right-inverse is exactly this theorem applied at rfl on all three components.
That torsor is the first step of the Burnside/orbit-stabilizer route to the shell-mass identity (sum_classMuOn_eq_card_div_factorials): labeled count over $v!\cdot e!\cdot t!$ equals the sum of $1/|\mathrm{Aut}|$ over quotient classes. Shell-mass unboundedness then kills absolute/positive-term regulator removal at zero phase (not_hasZRSRegulatorRemoval_zeroPhase). Oscillatory phases remain open; this lemma is purely combinatorial and phase-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.