autCard_congr
plain-language theorem explainer
Gauge-equivalent bounded complexes have equal automorphism-group order: a relabeling induces a conjugation bijection on Aut. Anyone deriving the 1/|Aut| path-sum measure from orbit/pair counting, or transporting |Aut| across glued or twin presentations, cites this. The proof unpacks the equivalence to a concrete relabeling and applies the induced Aut bijection to finite cardinalities.
Claim. Let $K$ and $K'$ be bounded complexes on the same bound $B$. If $K$ and $K'$ are equivalent (there exists a relabeling witness between them), then $|\mathrm{Aut}(K)| = |\mathrm{Aut}(K')|$.
background
This module sits in the Seven Gaps gauge-preflight layer. Path-sum gravity usually postulates the symmetry factor $\mu(K)=1/|\mathrm{Aut}(K)|$. Here that factor is derived from pure counting: the gauge orbit size (number of labeled complexes equivalent to $K$), the pair count (labeled copy plus concrete relabeling witness), and the class mass (orbit size over pair count) on the triangulation quotient.
Equivalence of bounded complexes means existence of a relabeling: a structure-preserving bijection of vertices, edges, and tetrahedra. Automorphisms are self-relabelings; their cardinality is the discrete stabilizer that later becomes the denominator of $\mu$. The module already records that relabeling witnesses between equivalent complexes form a torsor over $\mathrm{Aut}(K)$, so pair count factors as orbit size times $|\mathrm{Aut}|$.
For the class mass to be well-defined on the quotient, every counting ingredient must be independent of the labeled representative. Automorphism order is the stabilizer piece of that class-function package.
proof idea
Short term-mode proof. From the equivalence hypothesis, extract a concrete relabeling $r:K\to K'$. The relabeling API supplies an automorphism conjugation bijection $\mathrm{Aut}(K)\simeq\mathrm{Aut}(K')$ (the same autCongr used in the path-sum measure layer). Finite cardinality is invariant under type equivalence, so $\mathrm{Nat.card}$ of the two Aut types agree. No induction or case split.
why it matters
Representative independence of $|\mathrm{Aut}|$ is required before the gauge mass can descend to triangulation classes. Immediately downstream, pair-count congruence rewrites pair count via the orbit-stabilizer factorization and applies this lemma together with orbit-card congruence, so gauge volume is a class function.
Further parents live in Gap 2: dust/bouquet gluing multiplies automorphism orders only after transporting across a cone-equivalence; the dust-twin wreath identity $|\mathrm{Aut}(A\sqcup A)|=2|\mathrm{Aut} A|^2$ likewise rewrites through an equivalence; and the label-erasure obstruction (no locally additive real cost realizes $\log|\mathrm{Aut}|$) uses the same transport on twin dust. Together these close the counting side of the derivation that the class mass equals $1/|\mathrm{Aut}|$, the discrete-gravity convention the module set out to justify rather than postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.