ext
plain-language theorem explainer
Two exact-complex relabelings of the same signature are equal once their vertex, edge, and tetrahedron bijections agree. Anyone working with the setoid of exact complexes or with automorphism counts on complexity shells will cite this. The proof is a short injectivity argument through the triple of equivalences.
Claim. Let $K,K'$ be exact complexes of fixed signature $(v,e,t)$, and let $r,s$ be relabeling isomorphisms $K\to K'$ (bijections of vertex, edge, and tetrahedron indices that commute with incidence). If the three component bijections of $r$ and $s$ coincide, then $r=s$ as relabelings.
background
This module builds the configuration space for the Recognition Science path sum as exact complexity shells: combinatorial complexes with fixed vertex, edge, and tetrahedron counts and no size caps. An exact complex carries only incidence data (edge endpoints and tetrahedron vertices). A relabeling between two exact complexes of the same signature is a triple of bijections on those index sets that intertwine the incidence maps.
The module treats these relabelings as the morphisms of a setoid (global equivalence on each fixed signature). Extensionality of that structure is needed so that equality of morphisms is determined by the three component equivalences alone, not by proof-irrelevant commuting witnesses.
The surrounding development is deliberately mathematical: Gaussian UV regulation of the shell path sum is inserted by hand, the phase is a free class function, and continuum or regulator-removal claims remain open.
proof idea
Map each relabeling to the triple of its vertex, edge, and tetrahedron equivalences. Apply injectivity of that forgetful map into the product of equivalence types. Unfold the map and rewrite with the three given component equalities; the commuting diagrams are propositional and drop out of the equality.
why it matters
Exact-shell path sums weight each global equivalence class by the reciprocal automorphism order. That quotient only makes sense once relabelings form a well-behaved equivalence relation with extensional equality of morphisms. This lemma closes the structure side of that setoid (alongside reflexivity, symmetry, and transitivity of exact relabelings) so that shell cardinality bounds, class measures, and the regulated series $Z_{\mathrm{RS}}^{\mathrm{UV}}$ can treat classes as ordinary mathematical objects.
No FullTheoryLedger continuum flag is flipped here: the module still marks regulator removal and physical continuum limits as open. The result is pure combinatorial hygiene inside Stage 1 shell structure, not a derivation of gravity or of the action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.