ExactRelabel
plain-language theorem explainer
Exact relabeling is the isomorphism type for two exact-size complexes with the same (v,e,t) signature: permutations of vertex, edge, and tetrahedron indices that intertwine the incidence maps. Gravity and path-sum authors cite it as the cap-free gauge equivalence on labeled complexes. It is a pure structure definition (no proof body), independent of the capped PathSumMeasure.Relabel.
Claim. For two exact complexes $K,K'$ with the same counts $(v,e,t)$ of vertices, edges, and tetrahedra, an exact relabeling is a triple of bijections $\sigma_V:\mathrm{Fin}\,v\simeq\mathrm{Fin}\,v$, $\sigma_E:\mathrm{Fin}\,e\simeq\mathrm{Fin}\,e$, $\sigma_T:\mathrm{Fin}\,t\simeq\mathrm{Fin}\,t$ such that edge endpoints transform as $K'.\mathrm{edgeVerts}(\sigma_E(i))=(\sigma_V\times\sigma_V)(K.\mathrm{edgeVerts}(i))$ and tetrahedron vertices as $K'.\mathrm{tetVerts}(\sigma_T(i))(j)=\sigma_V(K.\mathrm{tetVerts}(i)(j))$.
background
The module builds exact complexity shells for the quotient-class path sum: configurations of fixed combinatorial size, with a hand-inserted Gaussian UV factor $\exp(-\rho n^2)$, and no claim that $\rho\to 0^+$ is physical. Honesty tags keep regulator removal and continuum limits open.
An exact complex of signature $(v,e,t)$ is a labeled incidence structure with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra: maps $\mathrm{edgeVerts}:\mathrm{Fin},e\to\mathrm{Fin},v\times\mathrm{Fin},v$ and $\mathrm{tetVerts}:\mathrm{Fin},t\to\mathrm{Fin},4\to\mathrm{Fin},v$, with no size-cap inequalities. Because there is no cap, the cross-cap identification issues of bounded complexes do not arise.
Exact relabeling is the structure morphism for that type: index bijections commuting with incidence. It is defined independently of the capped PathSumMeasure relabeling, so shell-level gauge equivalence never embeds into a bounded class.
proof idea
No proof: this is a structure declaration. The data are three equivalences on the finite index types plus two commuting diagrams (edge endpoints and tet vertex lists). Downstream lemmas supply identity, inverse, and composite relabelings; extensionality reduces equality of relabelings to equality of the three equivalences.
why it matters
Exact relabeling is the raw gauge arrow for Stage 1 shell structure. Automorphisms are self-relabelings (ExactAut K := ExactRelabel K K); global equivalence is the existence of such a relabeling; exactSetoid packages refl/symm/trans into a genuine setoid on each exact signature, so exact path classes and the $1/|\mathrm{Aut}|$ class measure are well-defined.
Cap–shell bridge maps transport the same data: an exact relabeling becomes a bounded relabeling after caps are attached, and bounded automorphisms match exact automorphisms of the cap-forgotten complex. Complexity congruence and shell Fintype/entropy bounds sit on this equivalence.
In the Seven Gaps program this is combinatorial gauge structure only. It does not derive a physical action, remove the Gaussian regulator, or flip continuum-limit ledger flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.