instSubsingletonAutOneEdge
plain-language theorem explainer
The automorphism group of a two-vertex complex carrying a single directed edge is trivial. Gap-2 measure arguments that contrast Aut-counts with ledger site-symmetry counts cite this fact: the directed edge has |Aut|=1 while the edgeless pair has |Aut|=2. The proof forces every automorphism to fix both endpoints via ordered edge-commutation, then collapses the edge and tet bijections by singleton index types.
Claim. For every bound $B\ge 2$, the automorphism group of the bounded complex with two vertices and one directed edge (from vertex $0$ to vertex $1$) is a singleton: any two automorphisms are equal.
background
Gap 2 (R2) asks whether a recognition measure can be read off the site symmetry of a recognition ledger, i.e. from how many relabelings of the vertex site type leave ledger cost unchanged. Orbit-stabilizer would convert such a count into masses $1/|\mathrm{Aut}|$. The module shows that route is blind at the smallest nontrivial size.
A Relabel between bounded complexes is a triple of bijections on vertex, edge, and tetrahedron indices that commute with incidence. In particular edge_comm equates ordered endpoint pairs after the vertex map. Aut(K) is the monoid of self-relabelings of $K$. The complex twoPointOneEdge is the two-vertex, one-edge, zero-tet complex (a single directed edge $0\to 1$).
Because edge_comm sees ordered pairs, orientation is visible to Aut but invisible to a symmetric ledger cost on vertex sites. That mismatch is the obstruction this instance feeds.
proof idea
Build Subsingleton by showing any two automorphisms $a,b$ are equal. First prove a key lemma: every automorphism $c$ has c.vEquiv = Equiv.refl (Fin 2). Apply c.edge_comm at the unique edge index $0$; after Prod.map simplification, injectivity of ordered pairs forces c.vEquiv 0 = 0 and c.vEquiv 1 = 1. Extend by fin_cases on Fin 2.
Conclude with Relabel.ext: the vertex components agree by the key lemma; the edge components agree by Subsingleton on Fin 1; the tet components agree vacuously on Fin 0 via elim0.
why it matters
This instance is the Aut half of the Gap-2 site-blindness no-go. The module shows that every recognition ledger on a two-element site is fixed by the transposition (symmetric zero-diagonal cost), so the site-symmetry count is always $2$. Meanwhile Aut distinguishes the edgeless pair ($|\mathrm{Aut}|=2$) from the directed edge ($|\mathrm{Aut}|=1$, proved here and recorded by the sibling cardinality theorem). Gauge counting wants masses $1/2$ and $1$; no measure that factors through site-symmetry count can supply both.
The result licenses a precise import demand: any derivation of the open measure obligation must bring structure that separates those two complexes (orientation-carrying ledger refinement, or sites on simplices rather than vertices alone). It does not close the measure obligation itself; it kills one natural premise shape. Framework context is the gravity seven-gaps program, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.