autCard_pos
plain-language theorem explainer
For any bounded combinatorial complex K, the automorphism group Aut(K) has positive finite cardinality. Gravity and path-sum authors cite this to justify the symmetry factor μ(K)=1/|Aut(K)| and the positivity of gauge orbit volumes. The proof is a one-line appeal to Nat.card_pos, using the preexisting Nonempty instance from the identity relabeling.
Claim. For every bound $B\in\mathbb{N}$ and every bounded complex $K$ of size at most $B$, the set of automorphisms of $K$ (relabelings of $K$ onto itself) satisfies $0 < |\mathrm{Aut}(K)|$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for the scoped recognition partition function $Z_{RS}$. Configurations are members of BoundedComplex B: combinatorial incidence data with at most $B$ vertices, edges, and tetrahedra, metric dropped, edge length fixed at the substrate mesh (CDT-style).
An automorphism of a labeled complex $K$ is a relabeling of $K$ onto itself. The type Aut K is defined as that self-relabeling set. The identity relabeling supplies a Nonempty instance, so the group is never empty. The module already proves the ambient configuration class is a Fintype, so automorphism sets inherit finiteness.
The path-sum measure uses the standard symmetry factor $\mu(K)=1/|\mathrm{Aut}(K)|$. Positivity of the cardinality is the arithmetic prerequisite for $0<\mu(K)\le 1$ and for well-defined gauge volumes built from orbit-stabilizer counting.
proof idea
One-line term proof: apply Nat.card_pos. That lemma needs a nonempty finite type; finiteness comes from the Fintype infrastructure on bounded complexes and relabelings, and nonemptiness is the instance ⟨Relabel.refl K⟩ already registered on Aut K. No further case analysis.
why it matters
This is the elementary positivity step that makes the symmetry-factor measure honest. Downstream, mu_pos and mu_le_one cast the same fact to reals and conclude $0<\mu(K)\le 1$; pairCount_pos in ExactShellGaugePreflight multiplies it with orbit-cardinality positivity to get a positive gauge volume via orbit-stabilizer.
In the module's status list this underwrites the proved block: finite nonempty Aut groups, a well-defined $\mu$, and the finite path sum $Z B w=\sum_K \mu(K),w(K)$ with modulus bounds. It does not close the OPEN nonuniform substrate-derived measure flagged by pathSumMeasureStatus; it only secures the uniform $1/|\mathrm{Aut}|$ convention used for the scoped $Z_{RS}$ statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.