exactAutCard_pos
plain-language theorem explainer
Every exact-size combinatorial complex has a nonempty finite automorphism group, so its automorphism cardinality is strictly positive. Discrete-gravity path-sum arguments cite this to justify the symmetry factor μ = 1/|Aut| as a well-defined positive real. The proof is a one-line application of Nat.card_pos, using the identity relabeling as the witness of nonemptiness.
Claim. For every exact-size complex $K$ with $v$ vertices, $e$ edges and $t$ tetrahedra, the cardinality of its automorphism group (exact self-relabelings) satisfies $0 < |\mathrm{Aut}(K)|$.
background
This module builds the configuration space of the Recognition Science path sum as exact complexity shells: labeled complexes with fixed vertex/edge/tetrahedron counts and no size caps. An ExactComplex v e t carries incidence maps for edges and tetrahedra on finite index sets; two such complexes are identified by exact relabelings (bijections of the three index sets commuting with incidence).
The automorphism type of a fixed labeled complex $K$ is the set of exact relabelings of $K$ onto itself. That type is inhabited by the identity relabeling, and it is finite because it injects into the product of the three finite symmetric groups on the index sets. The discrete-gravity convention then sets the per-complex measure to $\mu(K) = 1/|\mathrm{Aut}(K)|$.
The surrounding Stage-2 theorems need $|\mathrm{Aut}(K)| \ge 1$ as a real inequality before they can form $\mu$, prove $0 < \mu \le 1$, and sum class measures by Burnside/orbit-stabilizer.
proof idea
One-line term proof: apply Nat.card_pos. Mathlib's lemma requires the type to be nonempty and finite. Nonemptiness is the instance that supplies the identity exact relabeling (ExactRelabel.refl K). Finiteness is the companion instance that injects automorphisms into the finite triple of index permutations. No further case analysis is needed.
why it matters
This is the positivity hinge for the exact-shell measure. Immediately downstream, exactMu_pos and exactMu_le_one cast the inequality to reals and conclude $0 < \mu(K) \le 1$. The same positivity is reused when equal class measures force equal shell automorphism cards (shellAutCard_eq_of_classMu_eq) and in the headline Burnside identity that equates the sum of per-class measures to the labeled count divided by the full gauge volume $v!,e!,t!$ (sum_classMuOn_eq_card_div_factorials).
In the Seven Gaps program this sits in Stage 2 of the Gaussian-UV-regularized path sum: shells are Fintype, the per-class measure is well-defined on quotients, and the regulated series converges for every $\rho > 0$. It does not touch regulator removal (HasZRSRegulatorRemoval remains open) and flips no continuum-limit ledger flag. The identity-automorphism fact is elementary group theory, but without it the symmetry-factor measure is not even a positive real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.