autCard_twoPointComplex
plain-language theorem explainer
The automorphism group of the two-vertex edgeless bounded complex has cardinality exactly 2 (identity and vertex swap). Gravity and path-sum measure workers cite it as the concrete witness that separates the symmetry-factor weight from the uniform weight. The proof transports the Aut type along an explicit equivalence to a product of finite permutation groups and evaluates the resulting Fintype cardinalities.
Claim. For every integer bound $B \ge 2$, if $K$ is the two-vertex edgeless configuration with zero edges and zero tetrahedra under that bound, then the cardinality of its automorphism group satisfies $|\mathrm{Aut}(K)| = 2$.
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance, positivity, and normalization alone force the path-sum weight to be the symmetry-factor measure $\mu = 1/|\mathrm{Aut}|$. The module answers no: several inequivalent weights satisfy the named invariance axioms, so uniqueness fails.
A BoundedComplex B is a finite labeled complex with vertex, edge, and tetrahedron counts capped by $B$. Its automorphism group Aut is the type of self-relabelings. The two-point witness is the edgeless complex with two vertices and no edges or tetrahedra (available whenever $B \ge 2$).
Upstream, twoPointAutEquiv identifies that Aut group with the full triple of index permutations $(S_2 \times S_0 \times S_0)$, because the absence of edges and tetrahedra makes the commutation constraints vacuous. That equivalence is the bridge used here.
proof idea
Term-mode cardinality computation. Rewrite Nat.card along the type equivalence twoPointAutEquiv, so the Aut group becomes $(S_2 \times S_0 \times S_0)$. Pass to Fintype.card of the product, then apply Fintype.card_equiv on the identity equivalences of Fin 2 and Fin 0, and evaluate Fintype.card_fin. Close with norm_num on the resulting factorial arithmetic: $2! \cdot 0! \cdot 0! = 2$.
why it matters
This is the numerical hinge of the Lane D1 no-go. Downstream, mu_twoPointComplex unfolds the symmetry-factor measure and rewrites with this theorem to obtain $\mu(K) = 1/2$ on the two-point witness, while the uniform weight is $1$ there. That strict inequality feeds the headline mu_not_determined_by_invariance: both candidates obey the named invariance axioms yet disagree pointwise.
In the broader Recognition gravity stack, path-sum measures enter the discrete gravity and seven-gap analysis. The module is explicit that a richer axiom set (gluing, orbit-stabilizer, substrate structure) might restore uniqueness; that remains the open substrate-derivation frontier. The present result only kills the claim that invariance alone selects $1/|\mathrm{Aut}|$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.