module module moderate

`IndisputableMonolith.Cosmology.FoamTopology`

Defines the Euler characteristic of a finite cell set as the alternating sum over dimensions, and proves its elementary identities for cubical complexes. Cosmology and discrete-geometry workers cite it when tracking topology of recognition foam (voids, holes, freeze-out). The module is mostly definition plus short algebraic lemmas on empty sets, unions, filled boxes, and single defects.

claimFor a finite set $K$ of cells, $\chi(K) = \sum_{c \in K} (-1)^{\dim c}$. On a cubical complex this is $N_0 - N_1 + N_2 - \cdots$. The module records $\chi(\emptyset)=0$, the inclusion-exclusion identity $\chi(A\cup B)+\chi(A\cap B)=\chi(A)+\chi(B)$, values on filled $d$-boxes, the drop under a single 2D hole or 3D void, and excursion bookkeeping used in foam freeze-out.

background

Recognition Science treats spatial structure as a discrete recognition foam whose topology is tracked by cell counts in a cubical complex. The natural invariant is the Euler characteristic $\chi$, the alternating sum of the numbers of cells by dimension. The module doc fixes the combinatorial definition $\chi(K)=\sum_{c\in K}(-1)^{\dim c}$, matching the quantity computed by the cosmogenesis foam-topology script.

Sibling lemmas specialize this to empty complexes, disjoint and overlapping unions, filled boxes in dimensions 1--3 (where $\chi=1$), and complexes with a single 2-hole or 3-void. Freeze-out and excursion lemmas record how $\chi$ changes when cells are removed or when the foam is scanned over a full excursion. The ambient setting is $D=3$ spatial dimensions forced by the T8 step of the unified forcing chain.

proof idea

This is primarily a definition module with short algebraic lemmas, not a deep proof development. The core object is the weighted sum over cells. Empty-set and disjoint-union identities are immediate from the sum. The general union identity is inclusion-exclusion on the indicator of membership. Filled-box and one-defect evaluations are finite enumerations of cell counts by dimension. Freeze-out and excursion statements package those evaluations into the bookkeeping forms needed downstream.

why it matters in Recognition Science

Foam topology supplies the discrete Euler data that cosmology layers use when relating recognition-cell complexes to large-scale structure, void statistics, and freeze-out of topological defects. In the RS framework it sits under the Cosmology domain and supports any argument that needs $\chi$ of a cubical foam rather than a continuum manifold. It is consistent with T8 ($D=3$) and with the eight-tick discrete time structure, both of which fix the cell dimensions that enter the alternating sum. Parent consumers are expected among cosmogenesis and defect-dynamics results that import these $\chi$ evaluations; the module itself has no further upstream Lean dependencies beyond Mathlib.

scope and limits

Does not define continuum or smooth manifold Euler characteristic.
Does not prove topological invariance beyond finite cubical cell sets.
Does not derive physical void abundances or power spectra.
Does not force $D=3$; that is assumed from the broader chain.
Does not address infinite or non-cubical complexes.

declarations in this module (12)

def eulerChar L72
theorem eulerChar_empty L76
theorem eulerChar_union_add_inter L84
theorem eulerChar_disjoint_union L96
theorem eulerChar1D_filledBox L110
theorem eulerChar2D_filledBox L117
theorem eulerChar3D_filledBox L127
theorem eulerChar2D_oneHole L149
theorem eulerChar3D_oneVoid L159
theorem eulerChar_freezeOut_drop L173
theorem eulerChar_excursion_empty L208
theorem eulerChar_excursion_all L217