instSubsingletonAutOnePoint
plain-language theorem explainer
Any two automorphisms of the one-point bounded complex (one vertex, no edges or tets) are equal, so Aut is a subsingleton. Gravity and path-sum authors cite this when fixing the symmetry factor of the one-point class at cap B=2. The proof is pure index-type uniqueness: Fin 1 is a subsingleton and the edge/tet index types are empty.
Claim. Let $K$ be the one-point configuration at complexity cap $2$ (one vertex, zero edges, zero tetrahedra). Then $\mathrm{Aut}(K)$ is a subsingleton: any two relabeling automorphisms of $K$ coincide.
background
Lane D3 of the Seven Gaps program equips the quotient-first path sum $Z_q$ with an explicit oscillatory phase model on labeled configurations, descending to triangulation classes. At fixed complexity cap the phased sum is a finite sum with a modulus bound by total class mass; under a pairing hypothesis opposite phases cancel exactly and beat the triangle inequality. The non-vacuity witness at $B=2$ pairs the empty complex with the one-point class, both needing unit symmetry factor.
A relabeling is a triple of bijections on vertex/edge/tet index sets commuting with incidence. Automorphisms are self-relabelings: $\mathrm{Aut}(K) := \mathrm{Relabel}(K,K)$. The one-point complex is the bounded complex with $n_V=1$, $n_E=n_T=0$. Its vertex indices are $\mathrm{Fin},1$ (a subsingleton); edge and tet indices are empty.
proof idea
Construct the Subsingleton instance by showing any two automorphisms $a,b$ are equal via Relabel.ext. The three component equivalences are identified by Equiv.ext: on vertices, Subsingleton.elim equates the two maps $\mathrm{Fin},1\to\mathrm{Fin},1$; on edges and tets, the domain is empty so elim0 discharges both sides. No incidence identities need checking beyond what Relabel.ext already packages.
why it matters
The $B=2$ phase-pairing witness in this module needs both the empty complex and the one-point class to have unit symmetry factor so that the paired masses cancel cleanly and $|Z_q|\le\mathrm{totalClassMass}-2$ is strict and nonnegative. This instance is the Aut-side half of that unit-symmetry claim for the one-point configuration (the companion theorem on unit symmetry factor sits immediately below). It is pure finite-combinatorial bookkeeping inside the gravity path-sum stack, not a continuum or dynamical statement; the continuum limit of $Z_q$ remains open per the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.