classMu_capToShell
plain-language theorem explainer
At any complexity cap B, the class measure of a capped triangulation class equals the representative measure of that class after transport to the exact-shell carrier. Continuum-blocker and finite-sum reindexing proofs cite this when moving 1/|Aut| weights between the two quotient carriers. The argument inducts on the quotient and chains measure congruences through exact and relabeling equivalences.
Claim. For every natural number $B$ and every triangulation class $q$ at cap $B$, if $q$ is sent to an exact-shell pair by the cap-to-shell carrier map, then the class measure of the shell component equals the representative measure $\mu$ of a chosen representative of $q$.
background
Module P2.3 builds the missing carrier bridge between two finite quotient presentations of complexes at a complexity cap $B$. A bounded complex at cap $B$ 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 maps keep incidence data and relabeling witnesses, so they descend to inverse equivalences of the capped and exact-shell quotient carriers.
The class measure is the $1/|\mathrm{Aut}|$ weight on a quotient class; the representative measure $\mu$ is the same weight evaluated on a concrete complex. The bridge is required to preserve automorphism cardinality, hence these measures. No continuum limit, convergence claim, or physical substrate phase is assumed: only finite combinatorial carriers and their quotients by exact and relabeling setoids.
proof idea
Induct on the triangulation class $q$ via Quotient.inductionOn, reducing to a concrete bounded complex $K$. Form the exact-setoid class of toExact K and extract a global exact equivalence between its Quotient.out and toExact K. Separately, the relabeling quotient supplies an ordinary equivalence between Quotient.out of the capped class and $K$.
Unfold the cap-to-shell and class-measure definitions, rewrite the left-hand side with classMuOn_out, then run a three-step calc: exact measure is invariant under the global exact equivalence, equals $\mu(K)$ by the exact-to-bounded measure identity, and finally equals $\mu$ of the capped representative by relabeling congruence of $\mu$.
why it matters
This is the measure half of the capped-to-exact carrier bridge. Downstream, phasedZq_eq_exactComplexityCutoff reindexes the finite phased capped sum along the carrier equivalence and needs measure preservation so weights match; that equality is packaged as capShellCompatibility, the P2.3 closer that supplies the missing ZqContinuumBlocker.CapShellCompatibility hypothesis for every exact-shell phase.
In the Seven Gaps gravity stack the result is bookkeeping, not new physics: it lets exact-shell phases transport to capped PhaseModels and makes the cutoff through shell $B$ identical to the capped quotient sum. It does not itself touch continuum interpretation, alpha, or the forcing chain T0–T8; it only discharges the combinatorial measure identity those later arguments quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.