Cosmology Foam Topology Euler Char Freeze Out Drop

The freeze-out drop

The Euler characteristic is a number that describes the shape of a space by counting its parts: for a grid of cells it is the count of vertices, minus edges, plus squares, minus cubes, and so on. A solid block, no matter its size, always gives 1. That size-independence is what makes the number a topological invariant: it detects holes and voids, not bigness. A hollow ring gives 0, and a hollow shell gives 2.

In Recognition Science, the framework models the early universe as a foam of discrete regions assembled by a forced birth law. The declaration eulerChar_freezeOut_drop proves a simple fact about this foam. If the assembled positive region splits into two separate parts, an inner ball and an outer frozen foam, and the inner ball is contractible (meaning it has the Euler characteristic of a point, namely 1), then erasing that inner ball lowers the total Euler characteristic by exactly one. In symbols: χ(I ∪ O) = χ(O) + 1. The theorem is proved in the framework's machine-checked library of formal theorems, with no fitted parameters.

The fact matters because it gives a clean, parameter-free readout of what happens at a cosmic freeze-out. The framework's Phase 17 freezes the super-horizon part of the assembled foam. The theorem says that this freeze-out, by homogenizing the inner region to the vacuum, drops the foam's Euler characteristic by precisely one. This is the law-level statement behind a numeric drop seen in the framework's cosmology scripts. It is a topological signature that separates different assembly laws: a single contractible domain reads 1, while a fragmented dust reads its component count.

The theorem does not claim that any particular physical foam exists, nor does it say that the real cosmic web has a specific Euler characteristic. It establishes a conditional identity: if the foam splits as described and the inner ball is contractible, then the drop is exactly one. The theorem also does not claim that the closed relaxation dynamics can sustain structure; in fact, a separate proved result in the same module shows that the closed dynamics erases all topology, driving a sponge to the vacuum. Sustained cosmic-web structure in this account requires the open driven law, and that necessity is the gap between the trivial endpoint and a sponge.

/-- **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 (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 (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 theorem does not claim that any particular physical foam exists. The theorem does not claim that the real cosmic web has a specific Euler characteristic. The theorem does not claim that the closed relaxation dynamics can sustain structure.

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: