exactRelabelToBounded
plain-language theorem explainer
An exact-complex relabeling (vertex, edge, and tetrahedron bijections that commute with incidence) remains a bounded-complex relabeling once the three cap inequalities are reattached. Anyone building the capped-quotient to exact-shell carrier equivalence cites this field-wise transfer. The body is a pure structure copy: the same equivalences and commutation witnesses work after the backward labeled map that attaches the cap.
Claim. Fix $n \le B$ and a shell signature $s$ of index $n$. Let $K,K'$ be exact complexes of signature $s$ (exact vertex, edge, and tetrahedron counts with incidence data and no cap inequalities). Any exact relabeling $r:K\simeq K'$ induces a bounded relabeling between the two bounded complexes obtained by attaching the three cap-$B$ proofs to $K$ and $K'$ respectively; the induced maps on vertices, edges, and tetrahedra, and the incidence-commutation witnesses, are those of $r$.
background
The module builds the missing carrier equivalence behind CapShellCompatibility (Seven Gaps, P2.3). At a fixed cap $B$, a bounded complex has unique exact complexity $\max(n_V,n_E,n_T)\le B$. Conversely, an exact complex living in shell $n\le B$ becomes a bounded complex by reattaching the three cap proofs. Both directions carry incidence data and relabeling witnesses, so they descend to the two quotient carriers and are inverse there.
An exact complex is the cap-free configuration type: exactly $v$ vertices, $e$ edges, $t$ tetrahedra, with abstract incidence and no cap inequalities. An exact relabeling is a triple of bijections on those index sets that commute with edge and tetrahedron incidence. The sibling backward map attaches a cap $B$ to an exact complex whose shell index is at most $B$, producing a bounded complex with the same incidence data and the three inequalities filled by the shell bound and $n\le B$.
Bounded relabelings are the corresponding isomorphisms on the capped side. The present definition is the functoriality statement for that backward map on morphisms.
proof idea
Definitional structure construction, not a tactic proof. The target is a bounded relabeling between the two images under the backward labeled map. Each field is taken verbatim from the given exact relabeling: vertex equivalence, edge equivalence, tetrahedron equivalence, edge-incidence commutation, and tetrahedron-incidence commutation. No new equalities are proved; the same witnesses remain valid after the cap proofs are attached because the underlying incidence data are unchanged.
why it matters
This is the morphism half of the backward carrier map. The immediate parent is the backward map on one exact-signature quotient: that definition lifts the object map through the exact setoid by sending related exact complexes to related bounded classes, and the soundness obligation is exactly an instance of this relabeling transfer.
Together with the object map and the forward direction, the bridge preserves automorphism cardinality and therefore the $1/|\mathrm{Aut}|$ class measure. An arbitrary exact-shell phase then transports to a phase model at every cap, and reindexing the finite quotient sum along the carrier equivalence yields equality with the exact-complexity cutoff whose shell range is $B+1$. No continuum limit, convergence claim, or physical substrate interpretation is assumed; the work is purely combinatorial carrier equivalence inside the Seven Gaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.