twoPoint_orbitCard
plain-language theorem explainer
The gauge orbit of the two-point complex on two vertices has cardinality one. Hostile-probe and Gap-2 measure work cite it when checking that a constant labeled weight fails gauge counting on that class. The proof is orbit-stabilizer plus the known automorphism order two and a factorial size count that forces the product equal to two.
Claim. For the two-point complex on $2$ vertices (no edges, no triangles), the cardinality of its gauge orbit equals $1$. Equivalently, orbit-stabilizer gives $|\mathrm{orbit}|\cdot|\mathrm{Aut}|=2!\,0!\,0!$ with $|\mathrm{Aut}|=2$, hence $|\mathrm{orbit}|=1$.
background
This module is a hostile probe of the Gap-2 measure derivation: it stress-tests principle B-iii (wrong labeled weight), axiom-print hygiene, load-bearing premises, and blocker/certificate wiring. The local objects are bounded complexes and their gauge orbits under the residual labeling symmetry used in the Gap-2 census measure.
gaugeOrbitCard counts distinct gauge images of a complex. The two-point complex on parameter $2$ is the minimal nonempty test case: two vertices, zero edges, zero triangles. Upstream, orbitCard_mul_autCard is the orbit-stabilizer identity relating orbit size to automorphism order and the factorial product of the complex's size data; autCard_twoPointComplex fixes $|\mathrm{Aut}|=2$ for this complex. The projector scalar $\mu$ appears only downstream when class mass is compared to the Gibbs weight.
proof idea
Term/tactic hybrid, four steps. Instantiate orbit-stabilizer on the two-point complex of size $2$ to obtain $|\mathrm{orbit}|\cdot|\mathrm{Aut}|=n_V!,n_E!,n_T!$. Rewrite the automorphism factor via the specialized lemma that $|\mathrm{Aut}|=2$. With sizes $n_V=2$, $n_E=0$, $n_T=0$, norm_num on Nat.factorial collapses the right-hand side to $2$. omega then forces the orbit cardinality to $1$.
why it matters
Supplies the orbit size needed by wrong_labeled_weight_fails_gaugeCounting, the B-iii control in this hostile probe. That parent shows the constant labeled weight $1$ fails the gauge-counting principle: on the two-point class the fibre size (hence class mass under weight $1$) is $1$, while the target measure coefficient is $\mu=1/2$. Without orbit card $=1$, the numerical mismatch is not pinned. In the broader Seven Gaps gravity stack this is a minimal sanity check that gauge orbits are counted correctly before claiming uniqueness of the Gibbs/class-mass measure among invariant weights. It does not itself force $\phi$, the eight-tick octave, or $D=3$; it is local combinatorial support for the measure-derivation no-go.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.