eulerChar_excursion_empty
plain-language theorem explainer
If no cell of a finite complex K is over-dense, the positive excursion set is empty and its cubical Euler characteristic is zero. Cosmologists tracking the recognition foam's topology cite this as the vacuum endpoint of the consensus excursion. The proof is a one-line rewrite: the filter is empty, and the empty complex has χ = 0.
Claim. Let $\dim$ assign a dimension to each cell and let $p$ be a decidable predicate on cells. If $K$ is a finite set of cells such that $\neg p(c)$ for every $c \in K$, then the Euler characteristic of the positive excursion $\{c \in K : p(c)\}$ vanishes: $\chi(K|_{p}) = 0$.
background
Phase 18 of the cosmogenesis stack reads out the topology of the assembled recognition foam via the cubical Euler characteristic. For a finite cell set $K$ with dimension map $\dim$, one defines $\chi(K) = \sum_{c \in K} (-1)^{\dim c}$, the alternating sum of occupied 0-, 1-, 2-, and 3-cells that the numeric foam-topology script computes.
Two structural facts make the readout scale-free: a filled $d$-box always has $\chi = 1$ (contractible normalization), and $\chi$ is a valuation under unions and intersections. The positive excursion set is the filter of cells satisfying an over-density predicate $p$ (classically $p(c) :\Leftrightarrow 0 < f(c)$ for a consensus field $f$). The empty complex is already known to satisfy $\chi(\emptyset) = 0$.
This lemma treats the vacuum endpoint of that excursion: when the consensus is identically zero on $K$, no cell is over-dense, so the filtered region collapses to the empty complex.
proof idea
One-line rewrite proof. The hypothesis that every member of $K$ fails $p$ is exactly the premise of Mathlib's Finset.filter_false_of_mem, which rewrites $K.\mathrm{filter}, p$ to $\emptyset$. The simp lemma that the empty complex has Euler characteristic zero then finishes the goal.
why it matters
In the Recognition foam story, the closed forced relaxation drives the consensus field to vacuum. This theorem records that the topological readout follows: the positive excursion disappears and $\chi$ drops to zero, erasing handles and voids alike. It is the vacuum counterpart of the blob endpoint (every cell over-dense yields a single contractible component).
Downstream, the freeze-out simplification uses the same Euler calculus: when an inner contractible ball is homogenized away from an outer frozen foam, $\chi$ drops by exactly one. The vacuum endpoint supplies the $\chi = 0$ base case that makes those endpoint comparisons well-defined. Within the module's parameter-free topological readout, it closes the $\sigma = 0$ side of the consensus excursion without any fitted scale, matching the Phase-17 freeze-out narrative that structure is erased to vacuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.