shellToCap_boundedToShell
plain-language theorem explainer
Forgetting the three cap bounds on a bounded complex at level B, then reattaching them, recovers the original relabeling class. Anyone building or citing the capped-to-exact-shell carrier bridge in Seven Gaps P2.3 needs this right-inverse identity. The proof is a direct Quotient.sound with the identity relabeling on vertices, edges, and tetrahedra; incidence data is unchanged.
Claim. For any natural number $B$ and any bounded complex $K$ at cap $B$, forgetting $K$'s three cap proofs and then reattaching them returns the original class of $K$ in the relabeling quotient of bounded complexes at $B$.
background
In Seven Gaps P2.3 this module builds the missing carrier equivalence behind CapShellCompatibility. At cap $B$, a bounded complex is a triangulation whose vertex, edge, and tetrahedron counts each satisfy $\le B$, witnessed by three inequality proofs. An exact-shell complex records a precise shell index $n\le B$ without those proofs.
Two maps connect the carriers: forget the cap (bounded complex to exact shell) and reattach the three bounds (exact shell into the capped quotient). Both keep the original incidence data (edge endpoints, tetrahedron vertices) and the relabeling witnesses, so they descend to the two quotient carriers. The module states they are inverse there, which is what legitimates transporting automorphism counts and the $1/|\mathrm{Aut}|$ class measure across the bridge.
No target-sum equality, continuum limit, substrate phase, or physical interpretation is assumed at this layer.
proof idea
The goal is equality of two classes in the relabeling quotient, so the proof applies Quotient.sound and exhibits an explicit relabeling witness. That witness is the identity equivalence on vertices, on edges, and on tetrahedra. Edge commutation reduces to the claim that Prod.map of the identity leaves the ordered endpoint pair of each edge unchanged, discharged by cases on the pair. Tetrahedron commutation is definitional reflexivity at each corner index. Nothing combinatorial is rewritten: forget-then-reattach leaves the underlying incidence structure literally identical, so the identity is a valid relabeling.
why it matters
This is the right-inverse half of the carrier equivalence that CapShellBridge supplies for ZqContinuumBlocker.CapShellCompatibility. Its sole recorded parent is the left-inverse law on bounded quotient classes, proved by quotient induction and a one-line appeal to this theorem. Together the two inverses justify reindexing finite quotient sums along the carrier map, so a capped phase sum equals the exact-complexity cutoff at shell range $B+1$. The bridge preserves automorphism cardinality and hence the $1/|\mathrm{Aut}|$ class measure. It is pure discrete carrier work inside the Gravity/SevenGaps stack; continuum or physical claims sit downstream and are explicitly not assumed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.