emptyComplex
plain-language theorem explainer
The empty combinatorial complex at any size cap B: zero vertices, edges, and tetrahedra, with vacuous incidence maps. It is the canonical basepoint of every BoundedComplex B, used to prove Nonempty, to normalize the symmetry-factor measure mu(empty)=1, and as the trivial automorphism case in the path-sum invariance no-go. Construction is by zero bounds and Fin 0 elimination.
Claim. For every natural number $B$, there is a bounded complex with $n_V = n_E = n_T = 0$, size inequalities $0 \le B$, and incidence maps out of the empty index types $\mathrm{Fin}\,0$ (defined by elimination).
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{RS}$ on a scoped configuration class at fixed lattice scale. The substrate fixes edge length at the minimum mesh, so configurations are combinatorial and equilateral (CDT-style). Geometric data lives only in incidence maps.
BoundedComplex B packages at most $B$ vertices, edges, and tetrahedra together with abstract incidence: edgeVerts : Fin nE → Fin nV × Fin nV and tetVerts : Fin nT → Fin 4 → Fin nV, mirroring ReggeTriangulation3D with the metric field dropped and an explicit size cap. It is a MODEL superclass: it contains all bounded triangulations but also non-simplicial incidence data.
The empty complex is the zero object in that class. Because every field is zero or a map from an empty type, it inhabits BoundedComplex B for every $B$ and immediately yields Nonempty (BoundedComplex B).
proof idea
Definitional construction, not a tactic proof. Set nV = nE = nT = 0. Discharge the three size inequalities by Nat.zero_le B. Define edgeVerts and tetVerts by elim0 on the empty index types Fin 0, so there are no incidence obligations to check. The companion instance Nonempty (BoundedComplex B) is the singleton pair of this value.
why it matters
Basepoint for the whole path-sum stack. Downstream, autCard_emptyComplex proves $|\mathrm{Aut}(\mathrm{empty})| = 1$ via the Subsingleton instance on empty index bijections, and mu_emptyComplex gives $\mu(\mathrm{empty}) = 1$, discharging unit-normalization for the symmetry-factor measure. That fact feeds muSqMeasure_satisfies and muPowMeasure_satisfies, which show that $1/|\mathrm{Aut}|^2$ and the countable power family meet every named InvarianceAxioms clause used in the measure-invariance no-go.
Also used as emptyComplex_isSimplicial and as emptyClass in the $Z_q$ phase structure. In the module's honest status list, finiteness of BoundedComplex B discharges the count-finiteness content of the assumed growthBase field of PathSumUVBound.AdmissibleTriangulationFamily; the empty complex is the seed that makes the class nonempty before the code equivalence and Fintype transfer. It does not itself close the open exponential-growth semantics for exact simplicial subclasses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.