eulerChar_excursion_all
plain-language theorem explainer
If every cell of a finite complex K satisfies the over-density predicate, the positive excursion set equals K, so their Euler characteristics agree. Foam-topology readers cite this as the blob endpoint: full consensus yields a single topologically trivial region. The proof is a one-line rewrite that the filter is the identity on K.
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 and $p(c)$ holds for every $c\in K$, then $\chi(K\cap\{c:p(c)\})=\chi(K)$, where $\chi(S)=\sum_{c\in S}(-1)^{\dim c}$.
background
Phase 18 of the cosmology stack reads out the cubical Euler characteristic of the assembled recognition foam: for a finite cell set $K$, $\chi(K)=\sum_{c\in K}(-1)^{\dim c}$, the alternating sum of occupied vertices, edges, faces, and cubes. That quantity is the recognition analogue of the cosmic-web genus statistic computed by the numeric foam-topology scripts.
Two structural facts make the readout scale-free. A filled $d$-box has $\chi=1$ independent of side lengths (contractible normalization), and $\chi$ is a valuation: $\chi(A\cup B)+\chi(A\cap B)=\chi(A)+\chi(B)$. Deviations of $\chi$ from $1$ therefore measure genuine topology (extra components, tunnels $b_1$, enclosed voids $b_2$), never mere size.
The positive excursion set is the subset of cells satisfying an over-density predicate $p$ (strictly positive consensus $\sigma>0$). This lemma treats the endpoint where every cell of $K$ is over-dense, so the excursion coincides with $K$ itself.
proof idea
One-line rewrite. The hypothesis $\forall c\in K,, p(c)$ is exactly the side condition of Finset.filter_true_of_mem, which rewrites $K.\mathrm{filter}, p$ to $K$. Substituting into both sides of the goal makes the two Euler sums identical. No property of $\dim$ or of the alternating-sum definition is used beyond that equality of the underlying finsets.
why it matters
Doc-comment labels this the blob endpoint of the excursion analysis: full over-density makes the positive set a single contractible blob, with $\chi(K)$ and (for a filled box) $\chi=1$, hence no handles and no enclosed voids. The matching empty-excursion sibling covers the opposite consensus endpoint; together they pin the topology at both extremes of the density cut.
Downstream, the freeze-out simplification eulerChar_freezeOut_drop sits in the same module: when an assembled positive region splits as a contractible inner ball plus outer foam, erasing the inner ball drops $\chi$ by exactly one. The excursion endpoint supplies the trivial-topology side of that Phase-17 homogenization story. In the broader RS chain this is pure combinatorial topology on the foam assembled after the birth law and eight-tick structure, not a new forcing step, but it is the parameter-free topological signature that separates polar versus Thue-Morse cosmogenesis in the numeric readout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.