shellAutCard
plain-language theorem explainer
Defines the automorphism count of an exact-shell path class by taking a representative exact complex and counting its exact self-relabelings. Gravity and Seven-Gaps authors cite it when matching 1/|Aut| class weights across the capped and exact-shell carriers. The body is a one-line definition via quotient out and Nat.card.
Claim. For $n\in\mathbb{N}$ and an exact complexity shell class $c$ (a shell signature together with a global-equivalence class of exact labeled complexes of complexity exactly $n$), the shell automorphism cardinality is $\lvert\mathrm{Aut}(K)\rvert$, where $K$ is any chosen representative exact complex of that class.
background
The CapShellBridge module builds the carrier equivalence behind CapShellCompatibility: at a bound $B$, bounded complexes with exact complexity at most $B$ correspond to exact complexes in shells $n\le B$, carrying incidence data and relabeling witnesses both ways. Those maps descend to inverse equivalences of the two quotient carriers and are meant to preserve automorphism cardinality, hence the $1/|\mathrm{Aut}|$ class measure.
An exact path class at shell $n$ is a pair of a shell signature of complexity $n$ and a quotient of exact labeled complexes by global equivalence; no cap type appears. The exact automorphism group of a labeled exact complex $K$ is the type of exact relabelings of $K$ onto itself (always nonempty via the identity, and finite).
This definition packages that finite count at the level of an exact-shell class by reading off a representative.
proof idea
Pure definition, not a proof. From an exact path class $c$, project to the quotient component, take Quotient.out to obtain a concrete exact complex, form its exact automorphism type ExactAut, and return Nat.card of that type. No lemmas are applied; well-definedness up to the later bridge theorems is deferred.
why it matters
The bridge must preserve automorphism cardinality so that reindexing the finite quotient sum along the carrier equivalence equates the capped phase model sum with exactComplexityCutoff phase B (shell range $B+1$). Downstream, shellAutCard_capToShell states quotient-level automorphism preservation: the shell automorphism card of the image under capToShell equals the ordinary Aut card of a capped-class representative. Without this named count on the exact-shell side, that equality has no left-hand side. The module assumes no target-sum equality, continuum limit, or physical continuum reading; it only supplies the combinatorial carrier and measure bridge for Seven Gaps P2.3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.