eulerChar_empty
plain-language theorem explainer
The empty cell set has cubical Euler characteristic zero. Cosmology and foam-topology arguments cite it as the base case for additivity and for vacuum endpoints of excursion sets. The proof is a one-line simplification of the alternating sum definition.
Claim. For any dimension assignment $\mathrm{dim}:\alpha\to\mathbb{N}$, the Euler characteristic of the empty finite set of cells is zero: $\chi(\emptyset)=0$.
background
Phase 18 of the Recognition foam pipeline supplies a parameter-free topological readout of the assembled many-domain structure: the cubical Euler characteristic of a digital region, the RS analogue of the cosmic-web genus statistic.
The Euler characteristic of a finite set of cells is the alternating sum $\chi(K)=\sum_{c\in K}(-1)^{\dim c}$. On a cubical complex this is $N_0-N_1+N_2-N_3$, the quantity computed by the cosmogenesis foam-topology script. Two structural facts make the numeric readout meaningful without fitted scale: filled boxes normalize to $\chi=1$ independent of side lengths, and $\chi$ is a valuation (inclusion-exclusion), hence additive on disjoint unions.
The empty-complex identity is the zero base case of that valuation. Downstream, disjoint-union additivity recovers component counts for separated locked domains, and the vacuum endpoint of positive excursions is exactly the empty filter.
proof idea
One-line term/tactic proof: unfold eulerChar and simplify. The sum over the empty Finset is definitionally $0$ in $\mathbb{Z}$, so no further lemmas are required.
why it matters
This is the zero anchor for the combinatorial core of foam topology. It is invoked inside eulerChar_disjoint_union: once inclusion-exclusion is known, disjointness forces $A\cap B=\emptyset$, and this theorem turns $\chi(A\cup B)+\chi(\emptyset)=\chi(A)+\chi(B)$ into plain additivity, so $k$ separated solid domains read $\chi=k$.
It is also the last step of eulerChar_excursion_empty: if no cell is over-dense, the positive excursion filter is empty and $\chi$ of that filter is $0$, the vacuum endpoint of forced relaxation. Together with the filled-box normalizations ($\chi=1$ for contractible solid regions), these facts let the Phase-15/17 foam readout separate polar birth (single contractible domain) from Thue-Morse dust (component-count $\chi$) without scale parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.