Cosmology Foam Topology Euler Char1 D Filled Box

A filled box counts as one

The Euler characteristic is a number that describes the shape of a space by counting its features: vertices, edges, faces, and so on. For a finite cubical complex, it is the alternating sum of cell counts, χ = N₀ − N₁ + N₂ − N₃ (occupied vertices, minus unit edges, plus unit squares, minus unit cubes). This single number is a topological invariant: it stays the same under continuous deformation, so a solid region, however large, has the Euler characteristic of a point.

The one-dimensional case is the simplest. A filled segment of a+1 lattice points has a unit edges, so its Euler characteristic is (a+1) − a = 1. This identity, proved in the framework's machine-checked library of formal theorems as eulerChar1D_filledBox, holds for every integer a. The length of the segment cancels out exactly, leaving only the number 1. The same pattern extends to higher dimensions: a filled rectangle in two dimensions and a filled box in three dimensions also have Euler characteristic 1, independent of their side lengths.

This size-independence is what makes the Euler characteristic useful as a readout. In the framework's cosmology module, a numeric script computes χ on an assembled digital region, the recognition analogue of the cosmic-web genus statistic. Because a solid blob always reads χ = 1, any deviation from 1 measures genuine topology: extra connected components, tunnels (b₁), or enclosed voids (b₂), never mere size. A single contractible domain reads χ = 1, while k disjoint solid domains read χ = k, recovering the component count.

The framework proves two supporting facts that make the readout well-defined. First, the Euler characteristic is a valuation: χ(A ∪ B) + χ(A ∩ B) = χ(A) + χ(B) for any two finite cell sets, so it is additive over disjoint unions. Second, the closed forced relaxation dynamics erases topology: a sponge fed to the closed dynamics decays to the vacuum (χ = 0) or a single blob (χ = 1), with every handle and enclosed void gone. Sustained cosmic-web structure requires the open driven law, not the closed relaxation.

In plain terms, the declaration eulerChar1D_filledBox establishes a normalization: a filled segment is topologically equivalent to a point. This is the baseline against which the framework's foam topology readout measures structure. It does not claim that any particular cosmic-web foam has χ = 1, nor that the Euler characteristic alone determines the full topology of a region, nor that the framework's numerical simulations are Lean-verified. The box normalization is a theorem; the foam's actual χ values are computed numerically.

/-- **THEOREM (1-D normalization).** A filled segment of `a + 1` lattice points (so `a`
unit edges) has Euler characteristic `N₀ − N₁ = (a+1) − a = 1`: one contractible
component, independent of length. -/
theorem eulerChar1D_filledBox (a : ℤ) : (a + 1) - a = 1 := by ring

/-- **THEOREM (valuation / inclusion-exclusion).** The cubical Euler characteristic is a
valuation: `χ(A ∪ B) + χ(A ∩ B) = χ(A) + χ(B)`. This is the combinatorial core that makes
`χ` well-defined and additive; it is the reason the numeric readout may sum `χ` over the
locked domains the law assembles. -/
theorem eulerChar_union_add_inter {α : Type*} [DecidableEq α] (dim : α → ℕ)
    (A B : Finset α) :
    eulerChar dim (A ∪ B) + eulerChar dim (A ∩ B)
      = eulerChar dim A + eulerChar dim B := by
  classical
  unfold eulerChar
  exact Finset.sum_union_inter

/-- **THEOREM (2-D normalization).** A filled rectangle of `(a+1)×(b+1)` lattice points
has Euler characteristic `N₀ − N₁ + N₂ = 1`, INDEPENDENT of `a, b`. Here
`N₀ = (a+1)(b+1)` vertices, `N₁ = a(b+1) + (a+1)b` unit edges (horizontal then vertical),
and `N₂ = a·b` unit squares. A solid rectangle, however large, is topologically a
point. -/
theorem eulerChar2D_filledBox (a b : ℤ) :
    (a + 1) * (b + 1) - (a * (b + 1) + (a + 1) * b) + a * b = 1 := by ring

/-- **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

What this page does not claim

This does not claim that any particular cosmic-web foam has Euler characteristic 1. This does not claim that the Euler characteristic alone determines the full topology of a region. This does not claim that the framework's numerical simulations are machine-checked theorems.

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: