Cosmology Foam Topology

The topology of the cosmic foam

Cosmology foam topology is the study of the large-scale shape of the universe's structure: whether matter is distributed as one connected blob, a web of filaments and walls, or a scattered dust of isolated islands. Astronomers quantify this shape with the Euler characteristic, a number that counts the essential features of a shape. For a solid object, the Euler characteristic is 1, no matter how large it is. A shape with a tunnel through it, like a donut, has Euler characteristic 0. A hollow shell has Euler characteristic 2. These values are topological invariants: they do not change under stretching or bending, only under tearing or gluing.

The standard way to compute the Euler characteristic is as an alternating sum of cell counts. In a digital grid, this is χ = N₀ − N₁ + N₂ − N₃, where N₀ is the number of occupied vertices, N₁ the unit edges, N₂ the unit squares, and N₃ the unit cubes. The power of this formula is that it is size-independent: a filled box of any dimensions has χ = 1. This means any deviation from 1 in a measured region indicates genuine topology: extra connected components, tunnels, or enclosed voids, not mere size. The framework's machine-checked library of formal theorems proves this normalization for one, two, and three dimensions, and proves the inclusion-exclusion property that makes the Euler characteristic additive over separate regions.

In Recognition Science, the framework models the universe as a discrete record of recognition events, and the assembled structure of over-dense regions is called the foam. The framework's library proves that the Euler characteristic of this foam is a meaningful readout with no fitted scale. The key theorems are: a filled box has χ = 1; the Euler characteristic is additive over disjoint regions, so k separated solid domains read χ = k; removing a single interior vertex from a filled box in 2-D gives χ = 0, the signature of a tunnel; and in 3-D it gives χ = 2, the signature of an enclosed void. These results pin the three primitive topologies the readout reports: blob (χ = 1), hole (χ = 0), and void (χ = 2).

The framework's library also proves a freeze-out theorem: when an inner ball is erased from a foam, the total Euler characteristic drops by exactly one. This is the law-level statement behind the numeric drop in χ across the recognition front. More strikingly, the library proves that the closed forced relaxation dynamics erases all topology. Any connected world driven to consensus ends either as an empty vacuum (χ = 0) or a single blob (χ = 1). Every handle and enclosed void is gone. This is the law-level fact behind the observation that sustained cosmic-web structure requires the open driven law, not the closed relaxation.

The practical consequence is a topological signature that separates different laws of structure formation. The polar law assembles a single contractible domain (χ = 1), while a Thue-Morse foam fragments into a dust whose χ equals its component count, with no tunnels and no voids. The Euler curve χ(R) as the world grows is a parameter-free diagnostic that distinguishes these scenarios. The framework's library provides the exact, machine-checked foundation for this readout, turning a classical topological statistic into a precise tool for comparing cosmogenesis models.

/-- **THEOREM (3-D normalization).** A filled box of `(a+1)×(b+1)×(c+1)` lattice points
has Euler characteristic `N₀ − N₁ + N₂ − N₃ = 1`, INDEPENDENT of `a, b, c`. The cell
counts are `N₀ = (a+1)(b+1)(c+1)`; `N₁ = a(b+1)(c+1) + (a+1)b(c+1) + (a+1)(b+1)c` (edges
along the three axes); `N₂ = ab(c+1) + a(b+1)c + (a+1)bc` (squares in the three coordinate
planes); `N₃ = abc` (unit cubes). A solid box, however large, is topologically a point,
so in the numeric readout any deviation of `χ` from `1` measures genuine topology, never
size. -/
theorem eulerChar3D_filledBox (a b c : ℤ) :
    (a + 1) * (b + 1) * (c + 1)
      - (a * (b + 1) * (c + 1) + (a + 1) * b * (c + 1) + (a + 1) * (b + 1) * c)
      + (a * b * (c + 1) + a * (b + 1) * c + (a + 1) * b * c)
      - a * b * c = 1 := by ring

/-- **THEOREM.** Over disjoint cell sets the Euler characteristic is additive:
`χ(A ∪ B) = χ(A) + χ(B)`. So `k` separated locked domains contribute `k` times their
Euler characteristic; with the box normalization of §2, `k` disjoint solid domains read
`χ = k`, recovering the connected-component count. -/
theorem eulerChar_disjoint_union {α : Type*} [DecidableEq α] (dim : α → ℕ)
    {A B : Finset α} (h : Disjoint A B) :
    eulerChar dim (A ∪ B) = eulerChar dim A + eulerChar dim B := by
  classical
  have hbase := eulerChar_union_add_inter dim A B
  have hinter : A ∩ B = (∅ : Finset α) := Finset.disjoint_iff_inter_eq_empty.mp h
  rw [hinter, eulerChar_empty, add_zero] at hbase
  exact hbase

/-- **THEOREM (2-D hole detector).** A filled rectangle with one strictly-interior vertex removed
has `χ = 0`: deleting the vertex (`N₀ −= 1`), its `4` incident edges, and its `4` incident squares
drops `χ` from `1` to `0`, the invariant of an annulus with one tunnel (`b₁ = 1`). Meaningful for
`a, b ≥ 2` (so a strictly-interior vertex exists); the identity itself holds for all `a, b`. -/
theorem eulerChar2D_oneHole (a b : ℤ) :
    ((a + 1) * (b + 1) - 1)
      - ((a * (b + 1) + (a + 1) * b) - 4)
      + (a * b - 4) = 0 := by ring

/-- **THEOREM (3-D void detector).** A filled box with one strictly-interior vertex removed has
`χ = 2`: deleting the vertex (`N₀ −= 1`), its `6` incident edges, `12` incident squares, and `8`
incident cubes raises `χ` from `1` to `2`, the invariant of a hollow shell with one enclosed void
(`b₂ = 1`). Meaningful for `a, b, c ≥ 2` (so a strictly-interior vertex exists); the identity
itself holds for all `a, b, c`. -/
theorem eulerChar3D_oneVoid (a b c : ℤ) :
    ((a + 1) * (b + 1) * (c + 1) - 1)
      - ((a * (b + 1) * (c + 1) + (a + 1) * b * (c + 1) + (a + 1) * (b + 1) * c) - 6)
      + ((a * b * (c + 1) + a * (b + 1) * c + (a + 1) * b * c) - 12)
      - (a * b * c - 8) = 2 := by ring

/-- **THEOREM (freeze-out simplification, abstract form).** If the assembled positive
region splits as a disjoint union of an inner ball `I` and an outer frozen foam `O`, and
the inner ball is contractible (`χ(I) = 1`, the §2 normalization), then erasing the inner
ball (the Phase-17 homogenization to the vacuum) lowers the total Euler characteristic by
exactly one: `χ(I ∪ O) = χ(O) + 1`. This is the law-level statement behind the numeric
drop in `χ` across the recognition front. -/
theorem eulerChar_freezeOut_drop {α : Type*} [DecidableEq α] (dim : α → ℕ)
    {I O : Finset α} (hdisj : Disjoint I O) (hI : eulerChar dim I = 1) :
    eulerChar dim (I ∪ O) = eulerChar dim O + 1 := by
  rw [eulerChar_disjoint_union dim hdisj, hI]
  ring

/-- **THEOREM (vacuum endpoint).** If no cell of `K` is over-dense (`¬ p c` for every `c ∈ K`, the
`σ = 0` consensus `f ≡ 0` under `p c := 0 < f c`), the positive excursion set `K.filter p` is empty
and its Euler characteristic is `0`. The closed forced relaxation erases the structure to the
vacuum. -/
theorem eulerChar_excursion_empty {α : Type*} (dim : α → ℕ) (p : α → Prop) [DecidablePred p]
    (K : Finset α) (h : ∀ c ∈ K, ¬ p c) :
    eulerChar dim (K.filter p) = 0 := by
  rw [Finset.filter_false_of_mem h, eulerChar_empty]

What this page does not claim

The framework does not claim that the Euler characteristic alone determines the full topology of the cosmic web; it reports only the three primitive topologies (blob, hole, void). The framework does not claim that the closed relaxation dynamics is a model of actual cosmic evolution; it is a law-level fact about the mathematical dynamics, not a physical process. The framework does not claim that the Thue-Morse foam is the unique dust-like structure; it is one example that the readout distinguishes.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/FoamTopology.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: