instSubsingletonAutEmpty
plain-language theorem explainer
The automorphism group of the empty bounded complex is a subsingleton for every bound B: any two self-relabelings coincide. Path-sum and symmetry-factor arguments cite this to pin |Aut(empty)| = 1 and the unit normalization w(empty) = 1. The proof is a direct Subsingleton package: Relabel.ext plus uniqueness of equivalences on empty Fin types via elim0.
Claim. For every natural number $B$, $\mathrm{Aut}(\emptyset_B)$ is a subsingleton: if $\varphi,\psi$ are automorphisms of the empty bounded complex of bound $B$ (bijections of its vertex, edge, and tet index sets commuting with incidence), then $\varphi=\psi$.
background
This module (Seven Gaps, Lane D1) is a kernel no-go: relabeling invariance plus positivity and normalization do not single out the symmetry-factor path-sum weight $\mu=1/|\mathrm{Aut}|$. The named axiom package includes unit normalization on the empty configuration, so the automorphism group of that configuration must be controlled.
A BoundedComplex B is a finite labeled complex with vertex/edge/tet counts at most $B$. The empty complex has all three counts zero. A Relabel between complexes is a triple of index bijections (vertices, edges, tets) commuting with incidence; Aut K is the self-relabelings of $K$.
Upstream, emptyComplex B is the canonical zero inhabitant, and Aut is abbreviated as Relabel K K. The parameter $B$ is the same bound used elsewhere as an interface size; it does not affect emptiness of the three index types.
proof idea
Build the Subsingleton instance by exhibiting equality of any two automorphisms. Apply Relabel.ext to reduce to equality of the three component equivalences. Each component is an equivalence Fin 0 ≃ Fin 0; extend by Equiv.ext and discharge the unique element of Fin 0 with elim0. No nontrivial combinatorial content: emptiness forces the bijections.
why it matters
This instance is the algebraic reason the empty configuration has trivial symmetry. The immediate sibling theorem records $|\mathrm{Aut}(\mathrm{empty})|=1$, which feeds the unit normalization $\mu(\mathrm{empty})=1$ used inside InvarianceAxioms and the concrete witnesses (muMeasure, uniformMeasure, muSqMeasure, muPowMeasure).
In the Lane D1 story, the no-go headline is that several distinct weights satisfy the same invariance-type axioms; the empty complex anchors the shared normalization so the separation can be read off elsewhere (notably the two-point edgeless complex with $|\mathrm{Aut}|=2$). The declaration does not itself decide uniqueness of $\mu$; it only locks the empty orbit so the underdetermination argument is well-posed. Richer axioms (gluing, orbit-stabilizer, substrate structure) remain the open frontier for restoring uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.