boundedToShell_congr
plain-language theorem explainer
Relabel-equivalent bounded complexes at a fixed cap map to the same exact-shell representative. Anyone building the capped-to-shell quotient bridge or transporting phases across carriers cites this congruence. The proof peels both complexes, matches counts by the relabeling witness, kills proof fields by subsingleton, and finishes with nested Sigma.ext plus Quotient.sound.
Claim. Fix a cap $B \in \mathbb{N}$ and two bounded complexes $K, K'$ of complexity at most $B$. If $K$ and $K'$ are related by a bounded relabeling (incidence-preserving bijections on vertices, edges, and tetrahedra), then the forward map sending a bounded complex to its exact-shell class yields the same shell representative for $K$ and for $K'$.
background
Module P2.3 of the Seven Gaps gravity stack builds the carrier equivalence behind CapShellCompatibility. At a fixed cap $B$, a bounded complex packages finite vertex, edge, and tetrahedron counts together with incidence data and three proofs that each count is at most $B$. An exact complex in shell $n \le B$ is the same incidence data without those cap proofs.
The forward labeled map boundedToShell forgets the three cap certificates and records the exact complexity $n = \max(n_V,\max(n_E,n_T))$, landing in the exact-shell carrier ShellsUpTo B. Equivalence of bounded complexes is witnessed by a relabeling: bijections on the three index sets that commute with the edge and tet incidence maps.
Because the shell carrier is itself a quotient by exact-complex relabeling, any map out of labeled bounded complexes must be shown invariant under bounded relabeling before it can descend. That is exactly the role of this lemma. No continuum limit, target-sum identity, or physical phase interpretation is assumed here; only combinatorial carrier data.
proof idea
Destructure both bounded complexes into their count fields, incidence maps, and cap proofs. Unpack the Equivalent hypothesis to a concrete relabeling record $r$. Three named lemmas (relabel_nV_eq, relabel_nE_eq, relabel_nT_eq) give equality of the three counts; cases on those equalities aligns the types.
The three cap-proof fields are then identified by Subsingleton.elim (proof irrelevance of the $\le B$ propositions) and likewise eliminated by cases. The goal reduces to equality of nested dependent pairs. Two nested Sigma.ext steps discharge the count components by rfl. The remaining shell-class component is settled by heq_of_eq and Quotient.sound, feeding $r$'s three bijections and the two commutation witnesses as the exact-complex equivalence certificate.
why it matters
This is the congruence obligation that lets the forward map descend to quotient classes. Downstream, capToShell is defined as Quotient.lift boundedToShell with this lemma as the well-definedness proof, producing the forward half of the capped-quotient to exact-shell carrier bridge.
It is also the invariance step inside phaseModelAtCap: an arbitrary exact-shell phase is pulled back to a PhaseModel on the labeled bounded carrier by evaluating on boundedToShell K, and this lemma rewrites the phase under bounded relabeling so the model is well-defined.
Together these feed the reindexing argument that equates the finite quotient sum at cap $B$ with exactComplexityCutoff phase B (shell range $B+1$), closing the combinatorial half of CapShellCompatibility. The module explicitly assumes no continuum interpretation; the bridge only preserves automorphism cardinality and the $1/|\mathrm{Aut}|$ class measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.