autCard_twoPointOneEdge
plain-language theorem explainer
The automorphism group of the two-vertex complex with a single directed edge is trivial: its cardinality is 1. Gravity and gauge-counting arguments cite this when the symmetry-factor measure on that complex is fixed at 1, and when contrasting directed-edge Aut counts against ledger site symmetry. The proof is a one-line appeal to uniqueness of the automorphism (Subsingleton).
Claim. For every bound $B\ge 2$ (and $B\ge 1$ on edges), if $K$ is the bounded complex with two vertices and one directed edge from vertex $0$ to vertex $1$, then $|\mathrm{Aut}(K)|=1$.
background
Gap 2 (R2) asks whether a recognition ledger's site symmetry can supply the gauge-counting measure. The natural move is orbit-stabilizer: read $1/|\mathrm{Aut}|$ off how many site relabelings leave ledger cost fixed. The module shows that route is blind at the smallest nontrivial size.
A recognition ledger on a two-element site type is a symmetric zero-diagonal cost matrix, hence fixed by the transposition. Meanwhile two two-vertex complexes disagree on automorphism count: the edgeless pair has $|\mathrm{Aut}|=2$, while the single directed edge has $|\mathrm{Aut}|=1$, because edge comparison uses ordered endpoint pairs and a symmetric cost cannot see orientation.
The complex here is exactly that directed edge: two vertices, one edge $0\to 1$, no triangles, inside a bound $B\ge 2$. Aut is the automorphism type of a bounded complex; the claim is its cardinality.
proof idea
One-line term proof: Nat.card_unique. A sibling Subsingleton instance on the automorphism type of this one-edge complex supplies uniqueness, so the cardinality of a unique type is 1. No case analysis or explicit enumeration appears in the body.
why it matters
This is the Aut half of the directed-edge witness in the Gap-2 no-go. Downstream, mu_twoPointOneEdge unfolds the symmetry-factor measure and rewrites with this equality to conclude $\mu=1$ on the directed edge. Together with the edgeless pair (where Aut has order 2), that pins the target masses $1$ and $1/2$ that any correct gauge count must hit.
The module headline is that ledger site symmetry cannot separate those two complexes: both have site-symmetry count 2, so no measure factoring through site symmetry can match gauge counting. Any derivation must import orientation-carrying structure or simplex sites rather than vertex-only ledger cost. This theorem is the concrete Aut fact that makes the directed-edge side of that contrast hold. It does not close the open measure obligation; it kills one candidate premise shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.