shellAutCard_capToShell
plain-language theorem explainer
At any finite cap B, the shell automorphism count of the exact-shell image of a capped triangulation class equals the automorphism cardinality of a representative of that class. Gravity and continuum-blocker arguments cite this to move the 1/|Aut| class measure across the capped-to-shell carrier. The proof is a short quotient induction chaining two equivalence-induced Aut congruences through the labeled-to-exact automorphism identity.
Claim. Fix a natural number cap $B$ and a triangulation class $q$ at that cap (a relabeling-quotient of bounded complexes with complexity $\le B$). Writing $\mathrm{capToShell}(q)$ for the carrier map into an exact shell, the shell automorphism cardinality of the shell component equals $\lvert\mathrm{Aut}(\overline{q})\rvert$, where $\overline{q}$ is any chosen representative of $q$.
background
Module P2.3 builds the missing carrier bridge between capped (bounded-complexity) triangulation quotients and exact-shell carriers used by ZqContinuumBlocker.CapShellCompatibility. At cap $B$, a bounded complex has unique exact complexity $\max(n_V,n_E,n_T)\le B$; conversely an exact complex in shell $n\le B$ becomes bounded by reattaching the three cap proofs. Both directions keep incidence data and relabeling witnesses, so they descend to inverse maps on the two quotient carriers.
The bridge is required to preserve automorphism cardinality, hence the class measure $1/\lvert\mathrm{Aut}\rvert$. Upstream, autCard_toExact already equates $\lvert\mathrm{Aut}(K)\rvert$ for a bounded complex $K$ with $\lvert\mathrm{ExactAut}(\mathrm{toExact},K)\rvert$ via an explicit Aut equivalence. The present statement lifts that identity from labeled complexes to the capped quotient, comparing shell Aut card after capToShell with Aut card of Quotient.out of the class.
No continuum limit, target-sum equality, or physical phase interpretation is assumed here; only finite combinatorial Aut counts on the two carriers.
proof idea
Term-mode proof by Quotient.inductionOn on the capped class $q$, reducing to a labeled bounded complex $K$. Form the exact-setoid class of toExact K and extract a global equivalence $r$ between its Quotient.out and toExact K from Quotient.out_eq. Separately extract a relabeling equivalence $s$ between Quotient.out of the relabel class of $K$ and $K$ via PathSum.equivalent_of_mk_eq.
Unfold capToShell, boundedToShell, and shellAutCard. A three-step calc then runs: Aut card of the exact out-representative equals Aut card of toExact K by Nat.card_congr r.autCongr; that equals Aut card of $K$ by symmetry of autCard_toExact K; that equals Aut card of the relabel out-representative by symmetry of Nat.card_congr s.autCongr.
why it matters
This is the quotient-level Aut-preservation step inside the capped-to-exact-shell bridge. Downstream it feeds capShellCompatibility, the P2.3 closer: every exact-shell phase transports to a capped phase family satisfying the missing ZqContinuumBlocker.CapShellCompatibility hypothesis, via equality of the phased $Z_q$ sum with exactComplexityCutoff.
Without matching Aut cards, the $1/\lvert\mathrm{Aut}\rvert$ class measures would disagree after reindexing the finite quotient sum along the carrier equivalence, and the continuum-blocker compatibility would stay open. The module explicitly avoids claiming target-sum equality, convergence, substrate phase, or a physical continuum reading; those sit further downstream once the carrier and measure bridge is in place.
In the broader Seven Gaps gravity stack this is pure combinatorial bookkeeping on triangulation quotients, not a forcing-chain (T0–T8) identity, but it is the measure-preserving hinge that lets capped and exact-shell phase models talk to each other.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.