GlobalEquivalent
plain-language theorem explainer
Two exact complexes of fixed signature (v,e,t) are globally equivalent precisely when an exact relabeling exists between them: bijections of vertex, edge, and tetrahedron indices that commute with incidence. Anyone building the exact-shell path-sum quotient or class measures cites this relation. The body is a one-line definition as nonemptiness of the exact-relabel type.
Claim. Fix $v,e,t\in\mathbb{N}$. For exact complexes $K,K'$ with exactly $v$ vertices, $e$ edges and $t$ tetrahedra, $K$ is globally equivalent to $K'$ if and only if there exists an exact relabeling $K\to K'$ (bijections of the three index sets commuting with the edge and tetrahedron incidence maps).
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps) and studies a Gaussian-UV-regularized path sum. An exact complex of signature $(v,e,t)$ is a cap-free combinatorial complex: incidence data edgeVerts : Fin e → Fin v × Fin v and tetVerts : Fin t → Fin 4 → Fin v, with no bound inequalities. Because there is no cap, the cross-cap identification pathology of bounded complexes cannot arise.
An exact relabeling is a triple of bijections on the vertex, edge, and tetrahedron index sets that intertwine those incidence maps. It is defined independently of the capped PathSumMeasure.Relabel, so the equivalence lives purely on each fixed-signature fiber. Relabelings between different signatures are impossible: a vertex equivalence Fin v ≃ Fin v' forces $v=v'$ by cardinality.
The module is explicit that the regulator and the phase/action are mathematical parameters, not derived continuum physics; regulator removal remains a named open.
proof idea
Pure definitional abbreviation: global equivalence is the proposition that the type of exact relabelings from $K$ to $K'$ is inhabited. No tactics, no lemmas. Downstream, the setoid instance packages reflexivity, symmetry, and transitivity via the explicit ExactRelabel.refl, symm, and trans constructors on that same relabel type.
why it matters
This is the Stage-1 equivalence relation that turns each exact signature into a genuine setoid (exactSetoid), so exact path classes and shell entropy bounds are well-defined. It is the invariance relation for the per-class measure: exactMu_congr shows $\mu$ depends only on the global-equivalence class (mirroring capped mu_congr), and classMu_le_one descends the bound to classes.
Downstream bridges use it to identify capped triangulation classes with exact-shell images: classMu_capToShell and shellAutCard_capToShell both open a quotient induction by producing a global-equivalence witness between Quotient.out and toExact K. Certified tick recipes and lifted phases also thread through this relation. In the Seven Gaps ledger this closes the shell-structure half of the exact UV path sum; it does not touch continuum-limit or regulator-removal flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.