twoPointAutEquiv
plain-language theorem explainer
An explicit group equivalence identifying Aut of the two-vertex edgeless complex with the product of index permutations (Fin 2 ≃ Fin 2) × (Fin 0 ≃ Fin 0) × (Fin 0 ≃ Fin 0). Anyone computing |Aut| on the two-point witness cites this. The map is the componentwise projection of the Aut structure fields; inverse rebuilds Aut with vacuous edge/tet commutation proofs via elim0.
Claim. For every integer $B \ge 2$, the automorphism group of the two-vertex edgeless bounded complex (two vertices, zero edges, zero tetrahedra) is equivalent, as a type, to $(\mathrm{Fin}\,2 \simeq \mathrm{Fin}\,2) \times (\mathrm{Fin}\,0 \simeq \mathrm{Fin}\,0) \times (\mathrm{Fin}\,0 \simeq \mathrm{Fin}\,0)$: an automorphism is exactly a triple of permutations of the vertex, edge, and tetrahedron index sets, with no further constraints.
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance, positivity, and normalization alone force the path-sum weight $w(K)=1/|\mathrm{Aut}(K)|$. The module answers no: several distinct measures satisfy the named invariance axioms. The concrete separator is the two-vertex edgeless configuration twoPointComplex at any cap $B\ge 2$, with $n_V=2$, $n_E=0$, $n_T=0$.
An automorphism of a bounded complex is a triple of equivalences on the vertex, edge, and tetrahedron index sets that commute with the incidence data (edge endpoints and tetrahedron faces). When there are no edges and no tetrahedra, those commutation obligations are empty. The Aut type therefore collapses to the unrestricted product of the three index-permutation groups.
The Aut structure itself comes from the path-sum measure infrastructure (PathSumMeasure.Aut). The two-point complex is an abbreviation so that the size fields reduce during elaboration, which keeps the equivalence definitionally clean.
proof idea
Definitional equivalence, not a tactic proof. Forward map sends an automorphism $a$ to the triple $\langle a.v\mathrm{Equiv},, a.e\mathrm{Equiv},, a.t\mathrm{Equiv}\rangle$. Inverse rebuilds an Aut record from a triple $p$ by setting the three equivalence fields to $p$'s components and discharging the two commutation fields with e.elim0 and t.elim0 (both index types are empty). Left and right inverses are rfl. No external lemmas are invoked; the content is the observation that empty incidence data makes Aut free on the index permutations.
why it matters
This equivalence is the computational engine behind autCard_twoPointComplex, which concludes $|\mathrm{Aut}(\mathrm{twoPoint})|=2$ (identity and vertex swap) by transporting cardinality across the equivalence and evaluating $\mathrm{card}(\mathrm{Fin},2\simeq\mathrm{Fin},2)\cdot 1\cdot 1=2$. That cardinality feeds mu_twoPointComplex ($\mu=1/2$) and the headline no-go mu_not_determined_by_invariance: the symmetry-factor measure and the uniform measure both obey the named invariance axioms yet disagree at the two-point configuration.
In the broader Recognition gravity stack this is a kernel witness, not a physical law. It kills the claim that invariance alone selects $1/|\mathrm{Aut}|$ on the scoped path-sum class, and it keeps open the substrate-derivation frontier (gluing, orbit-stabilizer, or richer structure that might restore uniqueness). No T0–T8 forcing step is settled here; the result is local to measure selection on combinatorial complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.