emptyClass_ne_pointClass
plain-language theorem explainer
The empty-complex and one-point triangulation classes at complexity cap 2 are distinct elements of the relabeling quotient. Anyone citing the B=2 phase-pairing witness needs this to keep the two unit-mass classes separate in sums and pairings. The proof is a short quotient exactness argument: equality would yield a vertex bijection Fin 0 ≃ Fin 1, which is empty.
Claim. At complexity cap $B=2$, the relabeling class of the empty complex (zero vertices) is not equal to the relabeling class of the one-point complex (one vertex, no edges or tetrahedra). Equivalently, there is no relabeling isomorphism between those two bounded complexes, since that would require a bijection $\mathrm{Fin}\,0\simeq\mathrm{Fin}\,1$.
background
Lane D3 of the Seven Gaps program works on the quotient-first path sum Zq: bounded complexes up to a complexity cap $B$ are identified by relabeling isomorphisms, and the measure is pushed to triangulation classes. Two complexes are equivalent when a nonempty set of relabelings exists between them; classes are the corresponding quotient elements.
The empty complex at any cap has zero vertices, edges, and tetrahedra. The one-point complex at cap 2 has a single vertex and no incidence. Their classes (emptyClass, pointClass) are the two concrete unit-mass witnesses used later for an explicit phase model that pairs phase $0$ on the empty class against phase $\pi$ elsewhere.
Relabeling preserves the vertex count, so any isomorphism would supply a bijection of vertex index types. That is the only geometric fact needed here.
proof idea
Term-mode proof by contradiction. Assume the two classes are equal. Quotient exactness for the relabeling setoid yields an equivalence of the underlying complexes, hence a nonempty relabeling. From that relabeling extract a vertex equivalence vEquiv : Fin 0 ≃ Fin 1. Applying the inverse to the unique point of Fin 1 produces an element of Fin 0, which Fin.elim0 rules out.
why it matters
This is the discreteness hinge for the non-vacuous $B=2$ phase-pairing witness in the module. Downstream, two_le_totalClassMass_two sums unit masses over {emptyClass, pointClass} and needs the classes distinct so the Finset insert is valid and the sum equals 2; that makes totalClassMass 2 - 2 nonnegative. witnessPairing_disj uses the same inequality to show the witness pairing sends the empty class outside the paired family (to the point class). witnessPaired_mass then records that the paired mass is exactly 2.
Together those facts discharge the pairing hypotheses of the general cancellation theorems at fixed cap, giving the kernel chain $|Z_q| \le \mathrm{totalClassMass},2 - 2 < \mathrm{totalClassMass},2$. The continuum limit of the path sum remains open; this lemma only locks the finite $B=2$ witness arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.