AutFiberBucket
plain-language theorem explainer
For fixed complexity n and cardinality a, the equal-automorphism fiber collects exact path classes whose shell automorphism group has size exactly a. Gravity Gap-2 work cites it as the bucket type on which eventual evenness (or infinite odd obstruction) is stated. The body is a plain subtype of the exact complexity shell.
Claim. For $n,a\in\mathbb{N}$, write $\mathrm{AutFiberBucket}(n,a)$ for the type of exact path classes $c$ of complexity exactly $n$ such that the automorphism cardinality of a representative equals $a$. Equivalently, the fiber of the map $c\mapsto |\mathrm{Aut}(\mathrm{out}\,c)|$ over the value $a$ inside the exact complexity shell of level $n$.
background
The ambient object is the exact complexity shell: combinatorially distinct exact complexes of complexity exactly $n$, formed as a disjoint union over shell signatures of quotients of labeled exact complexes by global equivalence. No bounded-cap type enters that shell.
On each class $c$, shellAutCard is the finite cardinality of the exact automorphism group of a chosen representative, and the per-class measure classMu is its reciprocal. Classes with the same automorphism cardinality therefore share the same class measure; the fiber packages that level set as a type.
This module banks the Gap-2 R4 antipodal-design surface: equal-automorphism buckets, eventual even bucket cardinality as a combinatorial gate for free antipodal matching, and an infinite-family odd-bucket obstruction that would kill any inhabited tail antipodal shift.
proof idea
Definitional subtype: the carrier is ${c:\mathrm{ExactPathClass},n\mid \mathrm{shellAutCard},c=a}$. Finiteness is immediate from Subtype.finite once the ambient exact shell is finite in the ambient library. No algebraic identity is proved at this declaration; later lemmas equip the bucket with tick maps and shift equivalences.
why it matters
Parent uses are the parity gate and blocker: eventual even cardinality of every Aut-bucket (TailAutFiberEven), the infinite odd-bucket obstruction (TailAutFiberParityBlocker), the implication that a tail antipodal $+4$ tick shift forces eventual even buckets, and the converse that the blocker rules out any inhabited tail antipodal shift. Private helpers (bucketTau, shiftBucketEquiv) thread a Fin-8 tick through the bucket so that a mu-preserving $+4$ shift bijects low/high hemispheres and forces even card.
In the Gap-2 antipodal route this is the design-critical fiber on which matching is either free (even) or credit-blocked (odd infinitely often). It does not close the continuum-and-measure gap; the infinite blocker remains open, with only external finite parity probes measured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.