emptyClass
plain-language theorem explainer
Names the empty triangulation (zero vertices, edges, triangles) as a point of the relabeling quotient at complexity cap 2. Downstream phase-structure and pairing theorems cite it as one of the two unit-mass witness classes. The body is a one-line quotient constructor applied to the empty bounded complex.
Claim. Let $\mathrm{emptyClass}$ be the equivalence class of the empty bounded complex (zero vertices, edges, and triangles) in the set of combinatorially distinct triangulations at complexity cap $B=2$, i.e. the quotient of labeled complexes by relabeling isomorphism.
background
Lane D3 of the Seven Gaps program studies phase structure on the quotient-first path sum $Z_q$. Configurations are labeled bounded complexes (vertex/edge/triangle counts at most a fixed cap $B$), and two complexes are identified when a relabeling isomorphism exists. The quotient type is the set of triangulation classes: combinatorially distinct shapes up to renaming.
The empty complex is the zero-count inhabitant of every bounded class: $n_V=n_E=n_T=0$ with the trivial bound proofs. Relabeling isomorphism is a proved equivalence relation (reflexive, symmetric, transitive via identity, inverse, and composite relabelings), so the quotient map is well-defined.
This module equips those classes with an oscillatory phase model so that phased weights $\exp(i\theta)$ have unit modulus and the phased $Z_q$ is a finite sum with a modulus bound by total class mass. Concrete cancellation at $B=2$ needs named witness classes; the empty class is the first of them.
proof idea
One-line definition: apply the quotient constructor for the relabeling setoid at cap 2 to the empty bounded complex at cap 2. No tactics or lemmas beyond the upstream definitions of the empty complex, the relabeling setoid, and the triangulation-class abbreviation.
why it matters
This is the first concrete point in the $B=2$ non-vacuity witness chain for phased path sums. Downstream results use it to prove: the empty class is distinct from the one-point class (no bijection $\mathrm{Fin},0\simeq\mathrm{Fin},1$); its representative symmetry factor is 1; the witness phase model assigns phase 0 and weight $+1$ on it; the pairing family is the singleton ${\mathrm{emptyClass}}$ mapped to the one-point class with exact opposite phases.
Those facts discharge the pairing hypotheses so that $|Z_q,2|$ is strictly below the triangle bound by the paired mass 2, and $2\le\mathrm{totalClassMass},2$ makes the improved bound nonnegative. The continuum limit of the Seven Gaps program remains open; this definition only anchors the finite-cap structure theorems and the explicit cancellation witness at cap 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.