pointClass
plain-language theorem explainer
Names the relabeling-isomorphism class of the one-vertex, zero-edge complex at complexity cap 2. Gravity and path-sum arguments cite it as one of the two unit-mass witness classes that discharge the B=2 phase-pairing non-vacuity. The body is a one-line quotient constructor applied to the labeled one-point complex.
Claim. Let $\mathcal{T}_2$ be the set of combinatorially distinct triangulations of complexity at most $2$ (the quotient of labeled bounded complexes by vertex/edge/triangle relabeling). Write $[K]$ for the class of a labeled complex $K$. Define the one-point class as $[K_\bullet]$, where $K_\bullet$ has one vertex and no edges or triangles.
background
Lane D3 equips the quotient-first path sum $Z_q$ with an oscillatory phase model at fixed complexity cap $B$. Configurations are first labeled (BoundedComplex B), then identified up to combinatorial relabeling. The relation is the setoid relabelSetoid B (reflexive/symmetric/transitive via identity, inverse, and composite relabelings), and TriangulationClass B is the corresponding quotient: combinatorially distinct triangulations.
The labeled seed is the one-point complex at cap 2: one vertex, zero edges, zero triangles, with the size bounds 1 ≤ 2 and 0 ≤ 2. Its class is the object defined here. The empty (vertex-free) class is the other witness; together they feed the explicit phase model that puts phase $0$ on vertex-free configurations and phase $\pi$ elsewhere.
Upstream, the ratio-orbit constant two only supplies the numeric cap $B=2$ in the type. Finiteness of the quotient and the measure/symmetry factor $\mu$ live in the path-sum measure layer; this definition merely pins one concrete class used by the pairing witness.
proof idea
Definitional one-liner: form the quotient element by applying Quotient.mk for relabelSetoid 2 to the labeled onePointComplex. No tactics, no lemmas beyond the constructors of the setoid and the bounded-complex abbrev.
why it matters
This class is half of the concrete $B=2$ non-vacuity witness for conditional phase cancellation on $Z_q$. Downstream it appears in: distinctness from the empty class (no bijection $\mathrm{Fin},0\simeq\mathrm{Fin},1$); unit symmetry factor $\mu(\mathrm{out})=1$; witness phased weight $-1$ under the model with phase $\pi$ on positive vertex count; the constant pairing map sending every class to this one; paired mass exactly $2$; and the inequality $2\le\mathrm{totalClassMass},2$ that makes $|Z_q|\le\mathrm{totalClassMass}-2$ nonnegative and strictly better than the triangle bound.
In the module's kernel chain, the empty and one-point classes discharge the pairing hypotheses at fixed cap, giving $|Z_q,2,w|\le\mathrm{totalClassMass},2-2<\mathrm{totalClassMass},2$. The continuum limit of the path sum remains open; this object only closes the finite-cap witness arithmetic. It sits in the gravity/Seven-Gaps lane rather than the T0–T8 forcing chain, but it is the combinatorial seed that makes the stated pairing hypothesis non-empty at $B=2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.