autCard_toExact
plain-language theorem explainer
Automorphism groups of a bounded complex and of its cap-forgotten exact image have equal finite cardinality. Seven-Gaps gravity authors cite this when moving the $1/|\mathrm{Aut}|$ symmetry factor across the capped-to-exact-shell bridge. The proof is a one-line `Nat.card_congr` on the existing automorphism equivalence.
Claim. For any natural number $B$ and any bounded complex $K$ of cap $B$, $\lvert\mathrm{Aut}(K)\rvert = \lvert\mathrm{ExactAut}(\mathrm{toExact}(K))\rvert$: the number of bounded automorphisms of $K$ equals the number of exact automorphisms of the exact complex obtained by forgetting the cap.
background
Module P2.3 builds the carrier bridge between capped (bounded) complexes and exact-shell complexes that underlies CapShellCompatibility. At cap $B$, a bounded complex carries incidence data with $n_V,n_E,n_T\le B$; forgetting the three cap proofs yields an exact complex of the same type, via the map that drops $B$ from the target type while keeping edge and tetrahedron vertex data.
Automorphisms on the bounded side are relabelings of vertices, edges, and tets that preserve incidence. On the exact side, ExactAut is the type of exact self-relabelings of an exact complex. The upstream equivalence autEquivToExact states that these two groups carry exactly the same relabeling data: the three component equivalences of a bounded automorphism are already an exact automorphism of the forgotten complex, and conversely.
The bridge is designed so both directions preserve incidence and relabeling witnesses, descend to the quotient carriers, and are inverse there. Cardinality of the automorphism group is the discrete ingredient of the labeled class measure $1/|\mathrm{Aut}|$.
proof idea
One-line term proof. Apply Nat.card_congr to the type equivalence autEquivToExact K : Aut K ≃ ExactAut (toExact K). Finite cardinality is invariant under type equivalence, so the two automorphism sets have equal Nat.card. No further case analysis or induction.
why it matters
This is the cardinality half of the measure bridge in Seven Gaps P2.3. Immediately downstream, mu_eq_exactMu_toExact unfolds the two symmetry-factor measures and rewrites by this equality, so labeled $1/|\mathrm{Aut}|$ weights agree under cap forgetting. That fact lifts to the quotient in shellAutCard_capToShell (automorphism cardinality of a represented exact-shell class matches the capped representative).
Both feed the P2.3 closer capShellCompatibility: every exact-shell phase transports to a capped phase family satisfying the missing ZqContinuumBlocker.CapShellCompatibility, by reindexing the finite quotient sum along the carrier equivalence against exactComplexityCutoff. The module assumes no continuum limit, substrate phase, or physical interpretation; only discrete carrier and measure agreement. Framework role is local to the gravity seven-gaps stack, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.