mu_eq_exactMu_toExact
plain-language theorem explainer
For any bounded complex at cap B, the labeled symmetry-factor measure equals the exact-shell measure of its cap-forgotten image. Continuum-blocker and gravity bookkeeping cite this when moving 1/|Aut| weights across the capped-to-exact carrier bridge. The proof unfolds both measure definitions and rewrites by automorphism-cardinality preservation.
Claim. For every natural number $B$ and every bounded complex $K$ of cap $B$, the labeled symmetry-factor measure of $K$ equals the exact-shell measure of the complex obtained by forgetting the three cap bounds on $K$.
background
The module builds the missing carrier equivalence behind CapShellCompatibility (Seven Gaps, P2.3). At cap $B$, a bounded complex has a 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 the two quotient carriers and are inverse there.
The bridge is required to preserve automorphism cardinality and therefore the labeled $1/|\mathrm{Aut}|$ class measure. Upstream, automorphism-cardinality preservation states that $|\mathrm{Aut}(K)|$ equals $|\mathrm{ExactAut}|$ of the cap-forgotten image; the two measure definitions are the corresponding reciprocal symmetry factors on the bounded and exact sides.
No target-sum equality, convergence claim, substrate phase, or physical continuum reading is assumed at this layer.
proof idea
Short term proof. Unfold the two measure definitions (each is the labeled symmetry factor built from automorphism cardinality). The goals then differ only by those cardinalities, so rewrite with the upstream automorphism-cardinality preservation lemma, itself Nat.card_congr of the automorphism equivalence induced by cap forgetting.
why it matters
Feeds the quotient-level measure preservation theorem: the class measure on the exact-shell image equals the capped representative measure. That step lets finite quotient sums reindex along the carrier equivalence against the exact-complexity cutoff of range $B+1$, which is the equality demanded by the continuum blocker.
In the Recognition gravity stack this is bookkeeping infrastructure for discrete triangulation weights, not a forcing-chain landmark (T0–T8). It closes the measure half of the capped-quotient to exact-shell bridge so phase models transport cleanly at every cap. The module explicitly withholds continuum or physical interpretation; those remain separate claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.