shellAutCard_eq_of_classMu_eq
plain-language theorem explainer
Equal class measures on two exact path classes at the same shell force equal shell automorphism cardinalities. Gravity and Gap-2 antipodal-matching arguments cite this when partitioning classes into Aut-fiber buckets. The proof inverts the identity that class measure equals one over Aut-card, using positivity of the cards.
Claim. For any shell index $n$ and exact path classes $c,d$ at that shell, if the class measures agree ($\mu(c)=\mu(d)$), then the shell automorphism cardinalities agree: $\lvert\mathrm{Aut}\rvert(c)=\lvert\mathrm{Aut}\rvert(d)$.
background
This module banks the Aut-fiber parity-blocker surface for the Gap-2 antipodal design route. An Aut-fiber bucket collects exact path classes in one shell that share the same shell automorphism cardinality. The combinatorial gate for a free antipodal matching is that, from some shell onward, every such bucket has even class count; an infinite family of odd buckets is the terminal obstruction.
The local measure on an exact path class is tied to the Aut-card by the sibling identity that the class measure equals the reciprocal of the shell Aut-cardinality. Exact path classes live in a fixed shell $n$; the Aut-card is a positive natural number (cast to $\mathbb{R}$ in the reciprocal). That positivity is supplied by the exact Aut-card positivity lemma on a representative of the class.
Upstream scaffolding in the SevenGaps stack (antipodal balance bridge, cap-shell bridge, exact shell gauge UV) sets the Fin-8 tick and continuum residual context in which these buckets are later matched by a $+4$ tick shift between low and high hemispheres.
proof idea
Apply the sibling identity that class measure equals one over shell Aut-card to both $c$ and $d$. Cast exact Aut-card positivity on representatives to get strict positivity of both real cards, hence nonzero denominators. Rewrite the hypothesis $\mu(c)=\mu(d)$ as equality of the two reciprocals, then invoke div_eq_div_iff and symmetrize to equate the real cards. Finish by exact_mod_cast back to naturals.
why it matters
Equal Aut-cards are the membership predicate for Aut-fiber buckets. Downstream, shiftBucketEquiv builds a bucket self-equivalence from a tail antipodal shift: the shift must preserve Aut-card so that the subtype of the bucket is well-defined. That equivalence is the bridge from a mu-preserving $+4$ tick shift (low/high Fin-8 hemispheres) to even bucket cardinality, i.e. the implication TailAntipodalShift $\Rightarrow$ TailAutFiberEven.
In the Recognition Gravity Gap-2 program this is design-critical API for the antipodal route (session 4B), not a continuum close: the infinite TailAutFiberParityBlocker remains open, and nothing here flips gap2_continuum_and_measure. It sits in the discrete Fin-8 / eight-tick register geometry rather than the T5–T8 forcing chain itself, but it is the bookkeeping step that makes parity of Aut-fibers a well-posed obstruction to antipodal matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.