onePointComplex
plain-language theorem explainer
The one-point bounded complex at complexity cap 2: a single vertex with empty edge and tetrahedron sets. It is the concrete representative of the one-point triangulation class used in the B=2 phase-pairing witness for the quotient-first path sum. Defined as an abbreviation so the size fields reduce during elaboration; incidence maps are vacuous eliminators on empty index types.
Claim. The one-point configuration at cap $2$ is the bounded complex with one vertex, zero edges, and zero tetrahedra. The edge- and tetrahedron-incidence maps are the unique maps out of the empty index types, and the size bounds $1 \le 2$, $0 \le 2$, $0 \le 2$ hold.
background
This module equips the quotient-first object $Z_q$ with an explicit oscillatory phase model on labeled configurations that descends to triangulation classes. At fixed complexity cap $B$, the phased sum is a finite sum with a proved modulus bound by total class mass. The continuum limit remains open.
A bounded complex at cap $B$ packages finite vertex, edge, and tetrahedron counts (each at most $B$) together with incidence maps. The empty complex (zero vertices) and the one-point complex (one vertex, no incidence) are the two simplest configurations at $B=2$. Both carry unit symmetry factor and serve as the concrete pairing witnesses for exact opposite-phase cancellation.
The abbreviation form ensures that the numeric size fields reduce during typeclass and quotient elaboration when this object is quoted as a representative.
proof idea
Definitional construction, not a proof. The structure fields are set to $n_V=1$, $n_E=0$, $n_T=0$. The three size inequalities are the elementary facts $1\le 2$ and $0\le 2$. Edge and tetrahedron incidence are elim0 on the empty finite types Fin 0, which is the unique map out of the empty type. No geometric lemmas are invoked.
why it matters
This is the representative that defines the one-point triangulation class at cap 2, and that class is half of the explicit $B=2$ pairing witness. Downstream: the automorphism group is a subsingleton (trivial symmetry), so the symmetry factor equals 1; the witness phase model assigns phase $\pi$ (hence weight $-1$) on this class and phase $0$ on the empty class. Those two unit-mass opposite-phase terms cancel exactly, discharging the pairing hypotheses and yielding the strict improvement $|Z_q| \le \mathrm{totalClassMass}-2 < \mathrm{totalClassMass}$ at $B=2$.
In the Seven Gaps lane this is the non-vacuity anchor for conditional cancellation on the quotient-first path sum: the general pairing theorems are finite-sum arithmetic under an exact-opposite hypothesis, and this configuration (with the empty complex) is where that hypothesis is discharged concretely. Continuum cancellation remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.