autCard_emptyComplex
plain-language theorem explainer
The automorphism group of the empty bounded complex has cardinality one for every bound B. Anyone checking unit-normalization of the symmetry-factor path-sum measure cites this fact. The proof is a one-line appeal to uniqueness of the card of a singleton type (via the empty-complex automorphism Subsingleton instance).
Claim. For every natural number $B$, the automorphism group of the empty bounded complex of bound $B$ is a singleton: $\lvert\mathrm{Aut}(\emptyset_B)\rvert = 1$.
background
Lane D1 of the Seven Gaps gravity stack asks whether relabeling invariance, positivity, and normalization alone force the path-sum weight $w(K)=1/\lvert\mathrm{Aut}(K)\rvert$. The module answers no: several distinct weights satisfy the named invariance axioms.
A labeled complex $K$ of bound $B$ has automorphism group $\mathrm{Aut}(K)$ defined as the type of relabelings of $K$ onto itself. The empty complex $\emptyset_B$ is the canonical configuration with no vertices or incidences. The symmetry-factor measure is $\mu(K)=1/\lvert\mathrm{Aut}(K)\rvert$; unit normalization demands $\mu(\emptyset_B)=1$, which reduces to $\lvert\mathrm{Aut}(\emptyset_B)\rvert=1$.
Upstream, $\mathrm{Aut}$ is already known to be nonempty (the identity relabeling) and, for the empty complex, a Subsingleton instance is available in this module.
proof idea
Term-mode one-liner: apply Nat.card_unique. That lemma returns cardinality one once the type is both nonempty and a Subsingleton. Nonemptiness of every Aut K is the identity-relabeling instance; the empty-complex Subsingleton is the sibling instance instSubsingletonAutEmpty. No further case analysis is required.
why it matters
Feeds directly into mu_emptyComplex, which unfolds $\mu$ and rewrites by this cardinality to conclude $\mu(\emptyset_B)=1$. That equality discharges the unit-normalization clause of InvarianceAxioms, so the symmetry-factor measure is admitted as one of the three (in fact infinitely many) witnesses that invariance alone underdetermines the path-sum measure.
The headline no-go is mu_not_determined_by_invariance: $\mu$ and the uniform weight both satisfy the named axioms yet disagree on the two-point edgeless complex. Establishing $\lvert\mathrm{Aut}(\emptyset)\rvert=1$ is the empty-configuration half of that normalization bookkeeping. It does not restore uniqueness of $\mu$; the open substrate-derivation frontier (gluing, orbit-stabilizer, richer structure) remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.