eulerChar
plain-language theorem explainer
Defines the cubical Euler characteristic of a finite cell set as the alternating sum χ(K) = Σ_c (-1)^{dim c}. Cosmology and topology readers cite it as the parameter-free readout of recognition foam (the digital analogue of the cosmic-web genus). The body is a one-line Finset sum; all content lives in the downstream valuation and box-normalization lemmas.
Claim. For a type of cells $\alpha$, a dimension map $\mathrm{dim}:\alpha\to\mathbb{N}$, and a finite cell set $K\subseteq\alpha$, the Euler characteristic is $\chi(K)=\sum_{c\in K}(-1)^{\dim c}\in\mathbb{Z}$. On a cubical complex this is the alternating cell count $N_0-N_1+N_2-\cdots$.
background
Phase 18 of the cosmology stack supplies a parameter-free topological readout of the assembled recognition foam: the cubical Euler characteristic of a digital region, the recognition analogue of the cosmic-web genus statistic. Phase 15 builds the many-domain foam from the birth law; Phase 17 freezes the super-horizon part. This definition is the quantity that foam_topology.py evaluates on that structure.
Cells carry a dimension function $\mathrm{dim}$, and $K$ is any finite set of such cells (vertices, edges, squares, cubes, ...). The classical formula is the alternating sum of occupancy counts by dimension, $\chi=N_0-N_1+N_2-N_3$ in 3-D. Two structural facts, proved later in the module, make the number meaningful without a fitted scale: a filled $d$-box always has $\chi=1$ (contractible normalization), and $\chi$ is a valuation under union and intersection (inclusion-exclusion).
The Finset parameter is conventionally named $K$; that name collides with several unrelated constants elsewhere in the monolith (bridge ratio $\varphi^{1/2}$, curvature functionals, ledger kernels). None of those enter the definition.
proof idea
Pure definition: the body is the Finset sum $\sum_{c\in K}(-1)^{\dim c}$ with integer powers. No lemmas are applied. Downstream results discharge the empty case by simp, the valuation identity by Finset sum algebra, and the box normalizations by direct polynomial expansion (ring).
why it matters
This is the single primitive that every FoamTopology theorem instantiates. Immediate consumers include: empty-complex vanishing ($\chi(\emptyset)=0$); the valuation identity $\chi(A\cup B)+\chi(A\cap B)=\chi(A)+\chi(B)$ and its disjoint-union corollary; the 1-D/2-D/3-D filled-box normalizations that force $\chi=1$ independent of side lengths; the freeze-out drop $\chi(I\cup O)=\chi(O)+1$ when a contractible inner ball is erased; and the excursion endpoints (vacuum $\chi=0$, full blob $\chi(K)$). Outside the module it feeds TopologicalInvariant in TopologyFromRS.
In the framework narrative it is the law-level object behind the numeric Euler curve that separates polar (single contractible domain, $\chi=1$) from Thue-Morse foam (simply-connected dust with $\chi=b_0$). Deviations from 1 measure genuine topology (extra components, tunnels $b_1$, voids $b_2$), never mere size, which is why the box normalization and valuation lemmas sit immediately downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.