Cosmology Foam Topology Euler Char Union Add Inter

The Euler characteristic as a ledger

The Euler characteristic is a number that describes the shape of an object by counting its basic pieces. For a digital region built from cells, it is the alternating sum of the cell counts: vertices minus edges plus squares minus cubes, written χ = N₀ − N₁ + N₂ − N₃. This single number is a topological invariant, meaning a solid box, no matter how large, always has χ = 1, the same as a point. What changes the number is not size but genuine structure: separate pieces, tunnels, or enclosed voids each leave their own mark.

The key property for adding shapes together is called inclusion-exclusion. For any two finite collections of cells A and B, the Euler characteristic of their union plus the Euler characteristic of their intersection equals the sum of their individual Euler characteristics: χ(A ∪ B) + χ(A ∩ B) = χ(A) + χ(B). This identity, proved in the framework's machine-checked library of formal theorems, is what makes the Euler characteristic well-defined and additive. It means you can count the topology of a large assembled structure by summing the topology of its separate parts, provided you account for what they share. For disjoint pieces, the intersection is empty with χ = 0, so the formula simplifies to plain addition: the total is just the sum of the parts.

In Recognition Science, this theorem is the combinatorial core of a cosmological readout. The framework models the universe's large-scale structure as a foam of locked domains, and the Euler characteristic is a topological signature that separates different assembly laws. A single contractible domain reads χ = 1, while k separated solid domains read χ = k, recovering the component count. The theorem guarantees this summation is legitimate: the readout may add the Euler characteristic over the separated domains the law assembles without double-counting their shared boundaries. A filled box with a single interior vertex removed reads χ = 0 in two dimensions, the signature of an annulus with one tunnel, and χ = 2 in three dimensions, the signature of a hollow shell with one enclosed void.

The theorem does not claim that any particular physical foam actually forms, nor does it identify which assembly law governs the real cosmos. It is a purely combinatorial identity about finite cell sets, true for any collection of cells regardless of their origin. The framework's own simulations show different laws produce different Euler curves as the world grows, but matching those curves to the observed universe remains an empirical check, not a proved consequence. What the theorem establishes is a precise accounting rule: when you combine regions, the Euler characteristic of the whole is determined by the parts and their overlap, and nothing else.

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

What this page does not claim

The theorem does not claim that any particular physical foam actually forms in the universe. The theorem does not identify which assembly law governs the real cosmos. The theorem does not assert that matching simulated Euler curves to observed cosmic structure has been achieved.

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: