classMu_eq_one_div_shellAutCard
plain-language theorem explainer
For every exact path class on a finite shell, the per-class measure equals the reciprocal of that class's shell automorphism cardinality. Gravity Gap2 workers cite it when converting measure equalities into Aut-bucket equalities for the antipodal parity blocker. The proof unpacks the quotient lift and reduces to the discrete-gravity definition μ(K)=1/|Aut K|.
Claim. For every $n\in\mathbb{N}$ and every exact path class $c$ on shell $n$, the per-class measure satisfies $\mu(c)=1/|\mathrm{Aut}(c)|$, where $|\mathrm{Aut}(c)|$ is the automorphism cardinality of a representative exact complex of $c$.
background
This module banks the Aut-fiber parity-blocker API for the Gap2 antipodal design route: equal-Aut-card classes form buckets inside one exact shell, and eventual even bucket cardinality is the combinatorial gate for a free antipodal matching.
An exact labeled complex $K$ carries the discrete-gravity symmetry factor $\mathrm{exactMu}(K)=1/|\mathrm{ExactAut},K|$. That measure is constant on exact-relabeling equivalence, so it descends by quotient lift to a per-class measure $\mathrm{classMuOn}$, and thence to $\mathrm{classMu}$ on an $\mathrm{ExactPathClass}$. Separately, $\mathrm{shellAutCard},c$ is defined as $\mathrm{Nat.card}(\mathrm{ExactAut}(\mathrm{Quotient.out},c.2))$, the Aut order of a chosen representative.
The present identity says these two presentations agree: the class measure is exactly the reciprocal of the shell Aut card.
proof idea
Destructure $c=\langle s,q\rangle$. The goal becomes $\mathrm{classMuOn}(\mathrm{sig},s),q=1/|\mathrm{ExactAut}(\mathrm{Quotient.out},q)|$.
Use $\mathrm{Quotient.out_eq}$ to replace $q$ by the class of its out-representative. Unfold $\mathrm{classMuOn}$ and apply $\mathrm{Quotient.lift_mk}$ to land on $\mathrm{exactMu}(\mathrm{Quotient.out},q)$. That definition is definitionally $1/\mathrm{Nat.card}(\mathrm{ExactAut},\cdot)$, matching the unfolded $\mathrm{shellAutCard}$. The calc is three rewrites; no external arithmetic lemmas.
why it matters
Immediate parent is $\mathrm{shellAutCard_eq_of_classMu_eq}$: equal class measures force equal shell Aut cards, via this reciprocal identity plus positivity of Aut cardinality. That implication is the bridge from mu-preserving maps (e.g. a proposed $+4$ tick antipodal shift) into equal-Aut buckets, which the module packages as $\mathrm{AutFiberBucket}$.
In the Gap2 R4 antipodal design, even Aut-bucket cardinality is the gate for a free antipodal matching ($\mathrm{TailAutFiberEven}$); an infinite family of odd buckets is the credit-bearing obstruction ($\mathrm{TailAutFiberParityBlocker}$). Without identifying measure with $1/|\mathrm{Aut}|$, mu-equality would not control bucket size. The identity is pure discrete-gravity bookkeeping (standard $\mu=1/|\mathrm{Aut}|$ convention) and does not itself flip $\mathrm{gap2_continuum_and_measure}$; the infinite parity blocker remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.