IndisputableMonolith.Cosmology.FoamTopology

   1import Mathlib
   2
   3/-!
   4# Cosmology: the Euler characteristic of the assembled recognition foam (Phase 18)
   5
   6## Status: THEOREM (0 sorry, 0 RS-internal axiom).
   7
   8Phase 15 assembles a genuine many-domain foam from the forced birth law; Phase 17
   9freezes its super-horizon part. This module gives the parameter-free TOPOLOGICAL readout
  10that `scripts/cosmogenesis/foam_topology.py` computes on the assembled structure: the
  11cubical Euler characteristic of a digital region, the recognition analogue of the
  12cosmic-web genus statistic.
  13
  14The Euler characteristic of a finite cubical complex is the alternating sum of its cell
  15counts, `χ = N₀ − N₁ + N₂ − N₃` (occupied vertices, minus unit edges, plus unit squares,
  16minus unit cubes). Two facts make the numeric readout meaningful with no fitted scale,
  17and both are proved here.
  18
  19## §1. Contractible normalization: a filled box reads `χ = 1`
  20
  21A filled `d`-box has `χ = 1`, INDEPENDENT of its side lengths
  22(`eulerChar{1,2,3}D_filledBox`). That size-independence is the signature of a topological
  23invariant: a solid region, however large, has the Euler characteristic of a point. So in
  24the numeric readout any deviation of `χ` from `1` measures genuine topology, extra
  25connected components, tunnels (`b₁`), or enclosed voids (`b₂`), and never mere size. The
  262-D identity is `N₀ − N₁ + N₂ = (a+1)(b+1) − [a(b+1) + (a+1)b] + ab = 1`; the 3-D identity
  27is the analogous alternating sum over the six face families and the cube interior.
  28
  29## §2. Inclusion-exclusion (valuation): `χ` is additive over domains
  30
  31`χ(A ∪ B) + χ(A ∩ B) = χ(A) + χ(B)` for any two finite cell sets
  32(`eulerChar_union_add_inter`), so `χ` is additive over disjoint unions
  33(`eulerChar_disjoint_union`). This is the combinatorial core that makes `χ` well-defined
  34and is the reason the readout may sum the Euler characteristic over the separated locked
  35domains the law assembles: `k` disjoint solid domains read `χ = k`, recovering the
  36component count, while a single contractible domain reads `χ = 1`.
  37
  38## What the numeric module shows on top of this (classical, not Lean)
  39
  40The polar law assembles a single contractible domain (`χ = 1`), while the Thue-Morse foam
  41fragments into a simply-connected dust whose `χ` equals its component count `b₀` (so
  42`b₁ = b₂ = 0`: no tunnels, no enclosed voids). The Euler curve `χ(R)` as the world grows
  43is a topological signature that separates the laws, and the Phase-17 freeze-out lowers
  44`χ` by erasing the inner ball's topology to the vacuum while the frozen outer foam keeps
  45its dust topology. Hole/void detection is checked numerically against hand-built shapes
  46(a 2-D annulus reads `χ = 0`, a hollow 3-D shell reads `χ = 2`).
  47
  48## §4. The closed forced relaxation erases topology (Phase 20)
  49
  50The Phase-7 forced dynamics (`RecognitionEquilibrium`) relaxes any coupled world to
  51consensus, conserving the level sum and dropping the level variance monotonically. A
  52connected `σ = 0` world therefore relaxes to the all-zero field, whose positive excursion
  53set is empty (`χ = 0`, the vacuum); a positive consensus fills the region (`χ = χ(K)`, one
  54blob). Either way every handle and enclosed void is gone (`eulerChar_excursion_empty`,
  55`eulerChar_excursion_all`). So a sponge fed to the closed dynamics has its topology erased,
  56the law-level fact behind `scripts/cosmogenesis/foam_relaxation_topology.py`: sustained
  57cosmic-web structure needs the OPEN driven law (Phase 11), not the closed relaxation.
  58-/
  59
  60namespace IndisputableMonolith
  61namespace Cosmology
  62namespace FoamTopology
  63
  64open Finset
  65
  66/-! ## §1. The Euler characteristic as an alternating cell-count sum, and its valuation. -/
  67
  68/-- The Euler characteristic of a finite set of cells, each weighted by `(-1)` raised to
  69its dimension: `χ(K) = ∑_{c ∈ K} (-1)^{dim c}`. For a cubical complex this is the
  70alternating sum of cell counts by dimension, `N₀ − N₁ + N₂ − …`, the quantity computed
  71in `scripts/cosmogenesis/foam_topology.py`. -/
  72def eulerChar {α : Type*} (dim : α → ℕ) (K : Finset α) : ℤ :=
  73  ∑ c ∈ K, (-1 : ℤ) ^ (dim c)
  74
  75/-- The empty complex has Euler characteristic zero. -/
  76@[simp] theorem eulerChar_empty {α : Type*} (dim : α → ℕ) :
  77    eulerChar dim (∅ : Finset α) = 0 := by
  78  simp [eulerChar]
  79
  80/-- **THEOREM (valuation / inclusion-exclusion).** The cubical Euler characteristic is a
  81valuation: `χ(A ∪ B) + χ(A ∩ B) = χ(A) + χ(B)`. This is the combinatorial core that makes
  82`χ` well-defined and additive; it is the reason the numeric readout may sum `χ` over the
  83locked domains the law assembles. -/
  84theorem eulerChar_union_add_inter {α : Type*} [DecidableEq α] (dim : α → ℕ)
  85    (A B : Finset α) :
  86    eulerChar dim (A ∪ B) + eulerChar dim (A ∩ B)
  87      = eulerChar dim A + eulerChar dim B := by
  88  classical
  89  unfold eulerChar
  90  exact Finset.sum_union_inter
  91
  92/-- **THEOREM.** Over disjoint cell sets the Euler characteristic is additive:
  93`χ(A ∪ B) = χ(A) + χ(B)`. So `k` separated locked domains contribute `k` times their
  94Euler characteristic; with the box normalization of §2, `k` disjoint solid domains read
  95`χ = k`, recovering the connected-component count. -/
  96theorem eulerChar_disjoint_union {α : Type*} [DecidableEq α] (dim : α → ℕ)
  97    {A B : Finset α} (h : Disjoint A B) :
  98    eulerChar dim (A ∪ B) = eulerChar dim A + eulerChar dim B := by
  99  classical
 100  have hbase := eulerChar_union_add_inter dim A B
 101  have hinter : A ∩ B = (∅ : Finset α) := Finset.disjoint_iff_inter_eq_empty.mp h
 102  rw [hinter, eulerChar_empty, add_zero] at hbase
 103  exact hbase
 104
 105/-! ## §2. The contractible normalization: a filled box reads `χ = 1`, size-independent. -/
 106
 107/-- **THEOREM (1-D normalization).** A filled segment of `a + 1` lattice points (so `a`
 108unit edges) has Euler characteristic `N₀ − N₁ = (a+1) − a = 1`: one contractible
 109component, independent of length. -/
 110theorem eulerChar1D_filledBox (a : ℤ) : (a + 1) - a = 1 := by ring
 111
 112/-- **THEOREM (2-D normalization).** A filled rectangle of `(a+1)×(b+1)` lattice points
 113has Euler characteristic `N₀ − N₁ + N₂ = 1`, INDEPENDENT of `a, b`. Here
 114`N₀ = (a+1)(b+1)` vertices, `N₁ = a(b+1) + (a+1)b` unit edges (horizontal then vertical),
 115and `N₂ = a·b` unit squares. A solid rectangle, however large, is topologically a
 116point. -/
 117theorem eulerChar2D_filledBox (a b : ℤ) :
 118    (a + 1) * (b + 1) - (a * (b + 1) + (a + 1) * b) + a * b = 1 := by ring
 119
 120/-- **THEOREM (3-D normalization).** A filled box of `(a+1)×(b+1)×(c+1)` lattice points
 121has Euler characteristic `N₀ − N₁ + N₂ − N₃ = 1`, INDEPENDENT of `a, b, c`. The cell
 122counts 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
 123along the three axes); `N₂ = ab(c+1) + a(b+1)c + (a+1)bc` (squares in the three coordinate
 124planes); `N₃ = abc` (unit cubes). A solid box, however large, is topologically a point,
 125so in the numeric readout any deviation of `χ` from `1` measures genuine topology, never
 126size. -/
 127theorem eulerChar3D_filledBox (a b c : ℤ) :
 128    (a + 1) * (b + 1) * (c + 1)
 129      - (a * (b + 1) * (c + 1) + (a + 1) * b * (c + 1) + (a + 1) * (b + 1) * c)
 130      + (a * b * (c + 1) + a * (b + 1) * c + (a + 1) * b * c)
 131      - a * b * c = 1 := by ring
 132
 133/-! ## §2b. The Betti detectors: one removed interior vertex is one hole (2-D) or one void (3-D).
 134
 135These normalize the separated Betti readout in `scripts/cosmogenesis/foam_betti.py`. Removing a
 136single strictly-interior vertex from a filled box (with all its incident cells present, so the box
 137side is at least three per axis) deletes the vertex and its incident higher cells. In 2-D the
 138removed contributions are `1` vertex, `4` edges, `4` squares, so `χ` falls from `1` to
 139`1 + (-1 + 4 - 4) = 0`: the solid becomes an annulus with one tunnel (`b₁ = 1`). In 3-D they are
 140`1` vertex, `6` edges, `12` squares, `8` cubes, so `χ` rises from `1` to
 141`1 + (-1 + 6 - 12 + 8) = 2`: the solid becomes a hollow shell with one enclosed void (`b₂ = 1`).
 142With `eulerChar{2,3}D_filledBox` (the blob, `χ = 1`) these pin all three primitive topologies the
 143readout reports: blob (`χ = 1`), hole (`χ = 0`), void (`χ = 2`). -/
 144
 145/-- **THEOREM (2-D hole detector).** A filled rectangle with one strictly-interior vertex removed
 146has `χ = 0`: deleting the vertex (`N₀ −= 1`), its `4` incident edges, and its `4` incident squares
 147drops `χ` from `1` to `0`, the invariant of an annulus with one tunnel (`b₁ = 1`). Meaningful for
 148`a, b ≥ 2` (so a strictly-interior vertex exists); the identity itself holds for all `a, b`. -/
 149theorem eulerChar2D_oneHole (a b : ℤ) :
 150    ((a + 1) * (b + 1) - 1)
 151      - ((a * (b + 1) + (a + 1) * b) - 4)
 152      + (a * b - 4) = 0 := by ring
 153
 154/-- **THEOREM (3-D void detector).** A filled box with one strictly-interior vertex removed has
 155`χ = 2`: deleting the vertex (`N₀ −= 1`), its `6` incident edges, `12` incident squares, and `8`
 156incident cubes raises `χ` from `1` to `2`, the invariant of a hollow shell with one enclosed void
 157(`b₂ = 1`). Meaningful for `a, b, c ≥ 2` (so a strictly-interior vertex exists); the identity
 158itself holds for all `a, b, c`. -/
 159theorem eulerChar3D_oneVoid (a b c : ℤ) :
 160    ((a + 1) * (b + 1) * (c + 1) - 1)
 161      - ((a * (b + 1) * (c + 1) + (a + 1) * b * (c + 1) + (a + 1) * (b + 1) * c) - 6)
 162      + ((a * b * (c + 1) + a * (b + 1) * c + (a + 1) * b * c) - 12)
 163      - (a * b * c - 8) = 2 := by ring
 164
 165/-! ## §3. The freeze-out lowers `χ`: erasing a contractible inner ball drops it by one. -/
 166
 167/-- **THEOREM (freeze-out simplification, abstract form).** If the assembled positive
 168region splits as a disjoint union of an inner ball `I` and an outer frozen foam `O`, and
 169the inner ball is contractible (`χ(I) = 1`, the §2 normalization), then erasing the inner
 170ball (the Phase-17 homogenization to the vacuum) lowers the total Euler characteristic by
 171exactly one: `χ(I ∪ O) = χ(O) + 1`. This is the law-level statement behind the numeric
 172drop in `χ` across the recognition front. -/
 173theorem eulerChar_freezeOut_drop {α : Type*} [DecidableEq α] (dim : α → ℕ)
 174    {I O : Finset α} (hdisj : Disjoint I O) (hI : eulerChar dim I = 1) :
 175    eulerChar dim (I ∪ O) = eulerChar dim O + 1 := by
 176  rw [eulerChar_disjoint_union dim hdisj, hI]
 177  ring
 178
 179/-! ## §4. The closed forced relaxation erases topology: the `σ = 0` consensus endpoint is trivial.
 180
 181The Phase-7 forced recognition dynamics (`Cosmology.RecognitionEquilibrium`) drives any coupled
 182world to consensus. The level sum is conserved by every forced resolution
 183(`RecognitionEquilibrium.pairResolve_levelSum`) and the level variance is a Lyapunov function that
 184drops by exactly `(xᵢ − xⱼ)² / 2` per resolution (`RecognitionEquilibrium.variance_pairResolve`,
 185hence `variance_nonincreasing`), with the zero-cost fixed point being consensus
 186(`RecognitionEquilibrium.totalCost_eq_zero_iff`). So a connected `σ = 0` world relaxes to the
 187all-zero field: the unique consensus level is `σ / n = 0`.
 188
 189Read on the positive excursion set `{c ∈ K : p c}` with `p c := 0 < f c` (the over-dense cells),
 190that endpoint is topologically TRIVIAL. The two lemmas below pin the two possible consensus
 191excursion sets, and both kill every handle (`b₁`) and enclosed void (`b₂`):
 192
 193* a `σ = 0` connected consensus is the all-zero field, so no cell is over-dense, the excursion set
 194  is empty, and `χ = 0` (the vacuum, `eulerChar_excursion_empty`);
 195* a strictly positive consensus (`σ > 0`) makes every cell over-dense, so the excursion set is the
 196  whole region and `χ = χ(K)` (a single contractible blob, `= 1` for a box by §2,
 197  `eulerChar_excursion_all`).
 198
 199This is the law-level content of the `scripts/cosmogenesis/foam_relaxation_topology.py` history: a
 200sponge fed to the closed dynamics has its handles and voids erased and decays to the vacuum. The
 201closed forced law cannot sustain assembled structure; the cosmic web requires the OPEN driven law
 202(Phase 11), and that necessity is exactly the gap between this trivial endpoint and a sponge. -/
 203
 204/-- **THEOREM (vacuum endpoint).** If no cell of `K` is over-dense (`¬ p c` for every `c ∈ K`, the
 205`σ = 0` consensus `f ≡ 0` under `p c := 0 < f c`), the positive excursion set `K.filter p` is empty
 206and its Euler characteristic is `0`. The closed forced relaxation erases the structure to the
 207vacuum. -/
 208theorem eulerChar_excursion_empty {α : Type*} (dim : α → ℕ) (p : α → Prop) [DecidablePred p]
 209    (K : Finset α) (h : ∀ c ∈ K, ¬ p c) :
 210    eulerChar dim (K.filter p) = 0 := by
 211  rw [Finset.filter_false_of_mem h, eulerChar_empty]
 212
 213/-- **THEOREM (blob endpoint).** If every cell of `K` is over-dense (`p c` for every `c ∈ K`, a
 214strictly positive consensus `σ > 0`), the positive excursion set `K.filter p` is all of `K`, so its
 215Euler characteristic is `χ(K)`, a single contractible blob (`= 1` for a filled box by §2). Either
 216consensus endpoint is topologically trivial: no handles (`b₁`), no enclosed voids (`b₂`). -/
 217theorem eulerChar_excursion_all {α : Type*} (dim : α → ℕ) (p : α → Prop) [DecidablePred p]
 218    (K : Finset α) (h : ∀ c ∈ K, p c) :
 219    eulerChar dim (K.filter p) = eulerChar dim K := by
 220  rw [Finset.filter_true_of_mem h]
 221
 222end FoamTopology
 223end Cosmology
 224end IndisputableMonolith
 225