Cosmology Foam Topology Euler Char3 D Filled Box

The solid box invariant

The Euler characteristic is a number that describes a shape's overall structure, counting its basic pieces in an alternating sum. For a three-dimensional grid of cubes, the count is vertices minus edges plus square faces minus cubes. A filled rectangular box with side lengths a, b, and c has (a+1)(b+1)(c+1) vertices, a(b+1)(c+1) + (a+1)b(c+1) + (a+1)(b+1)c edges, ab(c+1) + a(b+1)c + (a+1)bc square faces, and abc cubes. When you compute the alternating sum, all the terms cancel and the answer is always 1, no matter what a, b, and c are.

This size-independence is the signature of a topological invariant: a solid region, however large, has the Euler characteristic of a single point. The 2-D version of the same fact says a filled rectangle of any size also has Euler characteristic 1. The Recognition Science framework's machine-checked library of formal theorems proves the 3-D case in the declaration eulerChar3D_filledBox, along with the 1-D and 2-D counterparts. The proof is a direct algebraic simplification: the alternating sum collapses to 1 by cancellation of terms.

In Recognition Science, this normalization is the zero point for reading cosmic-web topology. The framework models the universe's large-scale structure as a foam of discrete regions, and its numeric readout computes the Euler characteristic of the assembled foam. Because a solid blob always reads 1, any deviation from 1 in the readout measures genuine topology: extra connected components raise the count, while tunnels or enclosed voids change it in specific ways. A hollow shell with one enclosed void, for instance, reads 2. The framework proves that the Euler characteristic is additive over disjoint regions, so k separate solid domains read k, recovering the component count directly.

The declaration does not claim that any particular cosmic foam actually has Euler characteristic 1. It establishes only the normalization for a filled box. The framework's separate numerical experiments, which are classical computations rather than formal theorems, show that one assembly law produces a single blob (reading 1) while another fragments into a dust whose characteristic equals its component count. The declaration also does not claim that the Euler characteristic detects all topological features; it distinguishes blobs, holes, and voids, but finer structure requires other invariants.

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

What this page does not claim

No claim that any particular cosmic foam assembly has Euler characteristic 1. No claim that the Euler characteristic detects all topological features of a shape. No claim that the numerical foam experiments are formally verified 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: