IndisputableMonolith.Cosmology.InterfaceComponentBound

   1import Mathlib
   2
   3/-!
   4# Locked domains are at most the interface plus one (any dimension)
   5
   6## Status: THEOREM (0 sorry, 0 axiom beyond Mathlib's standard three).
   7
   8This module closes the connected-graph fact left OPEN in
   9`scripts/cosmogenesis/domain_coarsen_2d.py`, `domain_coarsen_3d.py`, and their Lean bridges
  10`IndisputableMonolith.Cosmology.DomainCoarsening2D` / `DomainCoarsening3D`: the locked-domain
  11("super-region") count the engine carries is at most the number of forced distinctions
  12(the recognition-active interface) plus one,
  13
  14  `components(monochromatic graph) <= (bichromatic edges) + 1`,
  15
  16on any connected world in any dimension. In 1D this is the exact identity
  17`DomainCoarsening.runs_eq` (`runs = boundaries + 1`); in 2D and 3D a domain interface can be
  18multiply connected, so the equality becomes this inequality. It was previously only
  19numeric-discharged ("verified on the live field every cycle") because it needs
  20component-counting-under-edge-deletion, which is not in Mathlib. Here it is a Lean theorem.
  21
  22The proof is dimension-free. A finite world is a finite vertex type `V`. A charge field
  23`c : V -> β` colours the vertices; an edge list `E : List (V × V)` is the adjacency the world
  24actually has (the 6-neighbour graph in 3D, 4-neighbour in 2D, the line in 1D). The monochromatic
  25edges (`c` equal on both ends) generate the locked domains; the bichromatic edges (`c` unequal)
  26are the interface. Component count is `Nat.card` of the quotient by the equivalence closure of the
  27edge relation, which needs only `Finite V` (no decidability of the closure, the usual obstruction).
  28
  29The mechanism is the classical "deleting an edge raises the component count by at most one": adding
  30the bichromatic edges back to the monochromatic graph reconstructs the (connected) ambient world,
  31and each added edge merges at most two locked domains. Formally, `comp_le_comp_cons` is the atomic
  32merge bound (proved by an `Option`-valued injection that is injective away from the single class the
  33new edge can collapse into), `comp_le_comp_append` iterates it over the interface, and
  34`comp_eq_one_of_connected` supplies the connected ambient endpoint. The headline is
  35`mono_components_le_bichromatic_succ`.
  36
  37The headline takes connectivity as a hypothesis. For the lattices the engine actually runs on, that
  38hypothesis is discharged here too, by a reusable criterion: `connected_of_descent` says a finite world
  39with a height `h : V → ℕ` that has a unique zero and a descent edge from every other cell is one
  40component. That is the recognition law's own pull toward the coarsest description, read as graph
  41connectivity. The 2D diamond (`Diamond`, the L1 ball `|x| + |y| ≤ t`, 4-neighbour) and the 3D
  42octahedron (`Octahedron`, `|x| + |y| + |z| ≤ t`, 6-neighbour) instantiate it with the L1 norm as
  43height and the origin as the unique zero, so `Diamond.mono_le_interface_succ` and
  44`Octahedron.mono_le_interface_succ` give `locked domains ≤ interface + 1` on the exact lattices the
  45engine evolves, for every radius (no fixed size, no `decide`). This closes the "wire the specific
  46lattice graph" step left routine in the Phase 13/14/15 docstrings.
  47-/
  48
  49namespace IndisputableMonolith
  50namespace Cosmology
  51namespace InterfaceComponentBound
  52
  53variable {V : Type*}
  54
  55/-- Base adjacency from an edge list, as ordered pairs. The equivalence closure symmetrizes, so the
  56orientation of each pair is irrelevant. -/
  57def gen (E : List (V × V)) (a b : V) : Prop := (a, b) ∈ E
  58
  59/-- Connectivity closure of the edge relation: the least equivalence relation containing `gen E`.
  60Two vertices are related iff a path of edges joins them. -/
  61def clos (E : List (V × V)) : V → V → Prop := Relation.EqvGen (gen E)
  62
  63theorem clos_equiv (E : List (V × V)) : Equivalence (clos E) := Relation.EqvGen.is_equivalence _
  64
  65/-- The connectivity closure as a `Setoid`; its quotient is the set of locked domains. -/
  66def cs (E : List (V × V)) : Setoid V := ⟨clos E, clos_equiv E⟩
  67
  68/-- The number of connected components (locked domains) of the graph with edge list `E`. Uses
  69`Nat.card`, so it is well-defined for any `Finite V` with no decidability hypothesis on the closure. -/
  70noncomputable def comp (E : List (V × V)) : ℕ := Nat.card (Quotient (cs E))
  71
  72/-- Universal property of the equivalence closure: it is below any equivalence relation containing
  73the generating relation. -/
  74theorem eqvGen_le {r s : V → V → Prop} (hs : Equivalence s) (h : ∀ a b, r a b → s a b) :
  75    ∀ a b, Relation.EqvGen r a b → s a b := by
  76  intro a b hab
  77  induction hab with
  78  | rel x y hxy => exact h x y hxy
  79  | refl x => exact hs.refl x
  80  | symm x y _ ih => exact hs.symm ih
  81  | trans x y z _ _ ih1 ih2 => exact hs.trans ih1 ih2
  82
  83/-- Monotonicity in the edge list: more edges can only merge domains, so the closure grows. Here,
  84prepending an edge keeps every prior connection. -/
  85theorem clos_mono_cons (a b : V) (X : List (V × V)) {u v : V} (h : clos X u v) :
  86    clos ((a, b) :: X) u v := by
  87  refine eqvGen_le (clos_equiv ((a, b) :: X)) ?_ u v h
  88  intro x y hxy
  89  exact Relation.EqvGen.rel x y (List.mem_cons_of_mem _ hxy)
  90
  91/-- The merged relation: the closure of `X` with the classes of `a` and `b` lumped together. This is
  92exactly the closure after adding the single edge `(a, b)`. -/
  93def merged (a b : V) (X : List (V × V)) (u v : V) : Prop :=
  94  clos X u v ∨ (clos X u a ∧ clos X v b) ∨ (clos X u b ∧ clos X v a)
  95
  96theorem merged_equiv (a b : V) (X : List (V × V)) : Equivalence (merged a b X) := by
  97  have e := clos_equiv X
  98  refine ⟨?_, ?_, ?_⟩
  99  · intro u; exact Or.inl (e.refl u)
 100  · intro u v h
 101    rcases h with h | ⟨h1, h2⟩ | ⟨h1, h2⟩
 102    · exact Or.inl (e.symm h)
 103    · exact Or.inr (Or.inr ⟨h2, h1⟩)
 104    · exact Or.inr (Or.inl ⟨h2, h1⟩)
 105  · intro u v w huv hvw
 106    rcases huv with huv | ⟨ua, vb⟩ | ⟨ub, va⟩
 107    · rcases hvw with hvw | ⟨va', wb'⟩ | ⟨vb', wa'⟩
 108      · exact Or.inl (e.trans huv hvw)
 109      · exact Or.inr (Or.inl ⟨e.trans huv va', wb'⟩)
 110      · exact Or.inr (Or.inr ⟨e.trans huv vb', wa'⟩)
 111    · rcases hvw with hvw | ⟨va', wb'⟩ | ⟨vb', wa'⟩
 112      · exact Or.inr (Or.inl ⟨ua, e.trans (e.symm hvw) vb⟩)
 113      · exact Or.inr (Or.inl ⟨ua, wb'⟩)
 114      · exact Or.inl (e.trans ua (e.symm wa'))
 115    · rcases hvw with hvw | ⟨va', wb'⟩ | ⟨vb', wa'⟩
 116      · exact Or.inr (Or.inr ⟨ub, e.trans (e.symm hvw) va⟩)
 117      · exact Or.inl (e.trans ub (e.symm wb'))
 118      · exact Or.inr (Or.inr ⟨ub, wa'⟩)
 119
 120theorem gen_cons_le_merged (a b : V) (X : List (V × V)) :
 121    ∀ u v, gen ((a, b) :: X) u v → merged a b X u v := by
 122  intro u v h
 123  have e := clos_equiv X
 124  rcases List.mem_cons.1 h with hpair | hmem
 125  · rw [Prod.mk.injEq] at hpair
 126    obtain ⟨rfl, rfl⟩ := hpair
 127    exact Or.inr (Or.inl ⟨e.refl _, e.refl _⟩)
 128  · exact Or.inl (Relation.EqvGen.rel u v hmem)
 129
 130/-- The closure after adding edge `(a, b)` is exactly the merge of the `a`-class and the `b`-class. -/
 131theorem clos_cons_iff (a b : V) (X : List (V × V)) (u v : V) :
 132    clos ((a, b) :: X) u v ↔ merged a b X u v := by
 133  constructor
 134  · exact eqvGen_le (merged_equiv a b X) (gen_cons_le_merged a b X) u v
 135  · intro h
 136    have hab : clos ((a, b) :: X) a b := Relation.EqvGen.rel a b List.mem_cons_self
 137    rcases h with h | ⟨ua, vb⟩ | ⟨ub, va⟩
 138    · exact clos_mono_cons a b X h
 139    · exact (clos_equiv ((a, b) :: X)).trans (clos_mono_cons a b X ua)
 140        ((clos_equiv ((a, b) :: X)).trans hab
 141          ((clos_equiv ((a, b) :: X)).symm (clos_mono_cons a b X vb)))
 142    · exact (clos_equiv ((a, b) :: X)).trans (clos_mono_cons a b X ub)
 143        ((clos_equiv ((a, b) :: X)).trans ((clos_equiv ((a, b) :: X)).symm hab)
 144          ((clos_equiv ((a, b) :: X)).symm (clos_mono_cons a b X va)))
 145
 146/-- The surjection from the finer (fewer edges) to the coarser (one more edge) quotient. -/
 147def proj (a b : V) (X : List (V × V)) : Quotient (cs X) → Quotient (cs ((a, b) :: X)) :=
 148  Quotient.lift (fun v => Quotient.mk (cs ((a, b) :: X)) v)
 149    (fun _ _ h => Quotient.sound (clos_mono_cons a b X h))
 150
 151/-- A surjection that collapses at most one pair (everything maps injectively except possibly into a
 152single class) loses at most one element of cardinality. -/
 153theorem card_le_succ_of_merge {A B : Type*} [Finite B]
 154    (f : A → B) (β : A) (hmerge : ∀ x y, f x = f y → x = y ∨ x = β ∨ y = β) :
 155    Nat.card A ≤ Nat.card B + 1 := by
 156  classical
 157  have hinj : Function.Injective
 158      (fun x : A => if x = β then (none : Option B) else some (f x)) := by
 159    intro x y hxy
 160    dsimp only at hxy
 161    by_cases hx : x = β <;> by_cases hy : y = β
 162    · exact hx.trans hy.symm
 163    · rw [if_pos hx, if_neg hy] at hxy; exact absurd hxy (by simp)
 164    · rw [if_neg hx, if_pos hy] at hxy; exact absurd hxy (by simp)
 165    · rw [if_neg hx, if_neg hy] at hxy
 166      have hf : f x = f y := Option.some.inj hxy
 167      rcases hmerge x y hf with h | h | h
 168      · exact h
 169      · exact absurd h hx
 170      · exact absurd h hy
 171  have hcard := Nat.card_le_card_of_injective _ hinj
 172  haveI := Fintype.ofFinite B
 173  have hoption : Nat.card (Option B) = Nat.card B + 1 := by
 174    rw [← Fintype.card_eq_nat_card, ← Fintype.card_eq_nat_card, Fintype.card_option]
 175  omega
 176
 177/-- **Atomic merge bound.** Adding one edge lowers the component count by at most one: equivalently,
 178the component count without the edge is at most the count with it, plus one. -/
 179theorem comp_le_comp_cons [Finite V] (a b : V) (X : List (V × V)) :
 180    comp X ≤ comp ((a, b) :: X) + 1 := by
 181  have hmerge : ∀ x y : Quotient (cs X),
 182      proj a b X x = proj a b X y → x = y ∨ x = Quotient.mk (cs X) b ∨ y = Quotient.mk (cs X) b := by
 183    refine Quotient.ind₂ ?_
 184    intro u v huv
 185    have hcl : clos ((a, b) :: X) u v := Quotient.exact huv
 186    rcases (clos_cons_iff a b X u v).1 hcl with h | ⟨ua, vb⟩ | ⟨ub, va⟩
 187    · exact Or.inl (Quotient.sound h)
 188    · exact Or.inr (Or.inr (Quotient.sound vb))
 189    · exact Or.inr (Or.inl (Quotient.sound ub))
 190  exact card_le_succ_of_merge (proj a b X) (Quotient.mk (cs X) b) hmerge
 191
 192/-- The component count depends only on the edge set, not the order or multiplicity of the list. -/
 193theorem comp_congr {X Y : List (V × V)} (h : ∀ p, p ∈ X ↔ p ∈ Y) : comp X = comp Y := by
 194  have hgen : gen X = gen Y := by
 195    funext a b
 196    exact propext (h (a, b))
 197  have hclos : clos X = clos Y := by unfold clos; rw [hgen]
 198  have hcs : cs X = cs Y := by
 199    apply Setoid.ext
 200    intro a b
 201    change clos X a b ↔ clos Y a b
 202    rw [hclos]
 203  unfold comp; rw [hcs]
 204
 205/-- **Iterated merge bound.** Adding a list `F` of edges lowers the component count by at most
 206`F.length`. -/
 207theorem comp_le_comp_append [Finite V] (X F : List (V × V)) :
 208    comp X ≤ comp (X ++ F) + F.length := by
 209  induction F with
 210  | nil => simp
 211  | cons f F' ih =>
 212    obtain ⟨a, b⟩ := f
 213    have hset : ∀ p, p ∈ (a, b) :: (X ++ F') ↔ p ∈ X ++ (a, b) :: F' := by
 214      intro p
 215      simp only [List.mem_cons, List.mem_append]
 216      tauto
 217    have hstep : comp (X ++ F') ≤ comp (X ++ (a, b) :: F') + 1 := by
 218      have := comp_le_comp_cons a b (X ++ F')
 219      rwa [comp_congr hset] at this
 220    calc comp X ≤ comp (X ++ F') + F'.length := ih
 221      _ ≤ (comp (X ++ (a, b) :: F') + 1) + F'.length := by omega
 222      _ = comp (X ++ (a, b) :: F') + (F'.length + 1) := by ring
 223      _ = comp (X ++ (a, b) :: F') + ((a, b) :: F').length := by simp [List.length_cons]
 224
 225/-- On the empty edge list every vertex is its own component, so the count is the number of cells. -/
 226theorem clos_nil (u v : V) : clos ([] : List (V × V)) u v ↔ u = v := by
 227  constructor
 228  · intro h
 229    induction h with
 230    | rel x y hxy => exact absurd hxy (by simp [gen])
 231    | refl x => rfl
 232    | symm x y _ ih => exact ih.symm
 233    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
 234  · intro h; subst h; exact Relation.EqvGen.refl u
 235
 236theorem comp_nil [Finite V] : comp ([] : List (V × V)) = Nat.card V := by
 237  have hbij : Function.Bijective (Quotient.mk (cs ([] : List (V × V)))) := by
 238    refine ⟨?_, Quotient.mk_surjective⟩
 239    intro u v h
 240    exact (clos_nil u v).1 (Quotient.exact h)
 241  unfold comp
 242  exact (Nat.card_congr (Equiv.ofBijective _ hbij)).symm
 243
 244/-- A connected ambient world is a single component. -/
 245theorem comp_eq_one_of_connected [Finite V] [Nonempty V] (E : List (V × V))
 246    (hconn : ∀ u v : V, clos E u v) : comp E = 1 := by
 247  haveI : Subsingleton (Quotient (cs E)) :=
 248    ⟨Quotient.ind₂ fun u v => Quotient.sound (hconn u v)⟩
 249  haveI : Nonempty (Quotient (cs E)) := ⟨Quotient.mk (cs E) (Classical.arbitrary V)⟩
 250  unfold comp
 251  rw [Nat.card_eq_one_iff_unique]
 252  exact ⟨inferInstance, inferInstance⟩
 253
 254/-- **Locked domains are at most the interface plus one.** For a connected finite world with edge
 255list `E` and charge `c`, the number of monochromatic connected components (the locked domains the
 256engine carries) is at most the number of bichromatic edges (the recognition-active interface) plus
 257one. This is the dimension-free form of the 1D identity `runs = boundaries + 1`. -/
 258theorem mono_components_le_bichromatic_succ {β : Type*} [Finite V] [Nonempty V] [DecidableEq β]
 259    (E : List (V × V)) (c : V → β)
 260    (hconn : ∀ u v : V, clos E u v) :
 261    comp (E.filter (fun p => decide (c p.1 = c p.2)))
 262      ≤ (E.filter (fun p => decide (c p.1 ≠ c p.2))).length + 1 := by
 263  set mono := E.filter (fun p => decide (c p.1 = c p.2)) with hmono
 264  set bi := E.filter (fun p => decide (c p.1 ≠ c p.2)) with hbi
 265  have hsplit : ∀ p, p ∈ mono ++ bi ↔ p ∈ E := by
 266    intro p
 267    simp only [hmono, hbi, List.mem_append, List.mem_filter, decide_eq_true_eq]
 268    constructor
 269    · rintro (⟨hp, _⟩ | ⟨hp, _⟩) <;> exact hp
 270    · intro hp
 271      by_cases hc : c p.1 = c p.2
 272      · exact Or.inl ⟨hp, hc⟩
 273      · exact Or.inr ⟨hp, hc⟩
 274  have h1 : comp mono ≤ comp (mono ++ bi) + bi.length := comp_le_comp_append mono bi
 275  have h2 : comp (mono ++ bi) = comp E := comp_congr hsplit
 276  have h3 : comp E = 1 := comp_eq_one_of_connected E hconn
 277  rw [h2, h3] at h1
 278  omega
 279
 280/-! ### A reusable connectivity criterion: descent toward a root
 281
 282The headline needs a connected ambient world (`hconn`). For the lattices the engine actually runs on
 283(the growing 2D diamond and the 3D octahedron, both L1 balls) connectivity has one cause: from any
 284cell off the centre, a single step toward the centre is a lattice edge to a strictly-lower cell, so
 285every cell reaches the centre. This is the recognition law's own pull toward the coarsest description,
 286read as a graph statement. We package it once, dimension-free, as a potential-descent criterion, then
 287instantiate it on the concrete lattices below. -/
 288
 289/-- If a height `h : V → ℕ` has a unique zero `root`, and every cell of positive height has a lattice
 290edge to a strictly-lower cell, then every cell is connected to `root`. The proof is strong induction
 291on `h v`: a zero-height cell is the root; a positive-height cell steps down an edge to a cell the
 292induction hypothesis already connects to the root. -/
 293theorem clos_root_of_descent [Finite V] (E : List (V × V)) (h : V → ℕ) (root : V)
 294    (hzero : ∀ v, h v = 0 → v = root)
 295    (hdesc : ∀ v, h v ≠ 0 → ∃ u, ((v, u) ∈ E ∨ (u, v) ∈ E) ∧ h u < h v) :
 296    ∀ v, clos E v root := by
 297  have e := clos_equiv E
 298  have H : ∀ n, ∀ v, h v = n → clos E v root := by
 299    intro n
 300    induction n using Nat.strong_induction_on with
 301    | _ n ih =>
 302      intro v hv
 303      rcases Nat.eq_zero_or_pos (h v) with h0 | hpos
 304      · rw [hzero v h0]; exact e.refl root
 305      · have hvne : h v ≠ 0 := by omega
 306        obtain ⟨u, hedge, hlt⟩ := hdesc v hvne
 307        have hvu : clos E v u := by
 308          rcases hedge with he | he
 309          · exact Relation.EqvGen.rel v u he
 310          · exact e.symm (Relation.EqvGen.rel u v he)
 311        have hur : clos E u root := ih (h u) (by omega) u rfl
 312        exact e.trans hvu hur
 313  intro v
 314  exact H (h v) v rfl
 315
 316/-- **Descent connectivity.** Under the same hypotheses the whole world is one component: any two
 317cells are connected through the root. -/
 318theorem connected_of_descent [Finite V] (E : List (V × V)) (h : V → ℕ) (root : V)
 319    (hzero : ∀ v, h v = 0 → v = root)
 320    (hdesc : ∀ v, h v ≠ 0 → ∃ u, ((v, u) ∈ E ∨ (u, v) ∈ E) ∧ h u < h v) :
 321    ∀ u v, clos E u v := by
 322  have e := clos_equiv E
 323  intro u v
 324  exact e.trans (clos_root_of_descent E h root hzero hdesc u)
 325    (e.symm (clos_root_of_descent E h root hzero hdesc v))
 326
 327/-- **Interface bound from a descent function.** Combining the descent criterion with the headline:
 328any finite world that admits a height with a unique zero and an edge of descent from every other cell
 329satisfies `locked domains ≤ interface + 1`. This is the form instantiated on the diamond and the
 330octahedron below: the lattice supplies `E`, the L1 norm supplies `h`, the centre supplies `root`. -/
 331theorem mono_le_interface_of_descent {β : Type*} [Finite V] [Nonempty V] [DecidableEq β]
 332    (E : List (V × V)) (c : V → β) (h : V → ℕ) (root : V)
 333    (hzero : ∀ v, h v = 0 → v = root)
 334    (hdesc : ∀ v, h v ≠ 0 → ∃ u, ((v, u) ∈ E ∨ (u, v) ∈ E) ∧ h u < h v) :
 335    comp (E.filter (fun p => decide (c p.1 = c p.2)))
 336      ≤ (E.filter (fun p => decide (c p.1 ≠ c p.2))).length + 1 :=
 337  mono_components_le_bichromatic_succ E c (connected_of_descent E h root hzero hdesc)
 338
 339/-! ### Concrete certificate
 340
 341Two cells of opposite charge joined by one edge: two locked domains, exactly one interface edge plus
 342one. This pins the bound tight and confirms the theorem is not vacuous. -/
 343
 344theorem twoCell_connected : ∀ u v : Fin 2, clos [((0 : Fin 2), (1 : Fin 2))] u v := by
 345  have e := clos_equiv [((0 : Fin 2), (1 : Fin 2))]
 346  have h01 : clos [((0 : Fin 2), (1 : Fin 2))] 0 1 := Relation.EqvGen.rel 0 1 (by simp [gen])
 347  have h : ∀ u : Fin 2, clos [((0 : Fin 2), (1 : Fin 2))] u 0 := by
 348    intro u
 349    fin_cases u
 350    · exact e.refl 0
 351    · exact e.symm h01
 352  intro u v
 353  fin_cases v
 354  · exact h u
 355  · exact e.trans (h u) h01
 356
 357/-- The two-cell world has exactly two locked domains (its empty monochromatic graph), pinned by
 358`comp_nil`. -/
 359theorem twoCell_comp_nil : comp ([] : List (Fin 2 × Fin 2)) = 2 := by
 360  rw [comp_nil]; simp [Nat.card_eq_fintype_card]
 361
 362/-- The interface bound applied to the two opposite-charge cells: two locked domains, one interface
 363edge. The bound is tight (`2 ≤ 1 + 1`). -/
 364theorem twoCell_interface_bound :
 365    comp (([((0 : Fin 2), (1 : Fin 2))]).filter (fun p => decide ((id p.1) = (id p.2))))
 366      ≤ (([((0 : Fin 2), (1 : Fin 2))]).filter (fun p => decide ((id p.1) ≠ (id p.2)))).length + 1 :=
 367  mono_components_le_bichromatic_succ [((0 : Fin 2), (1 : Fin 2))] id twoCell_connected
 368
 369/-! ### The engine's actual lattices: the 2D diamond and the 3D octahedron
 370
 371The coarsening engine runs on a growing 2D diamond (`scripts/cosmogenesis/domain_coarsen_2d.py`: the
 372L1 ball `|x| + |y| ≤ t`, 4-neighbour adjacency) and a growing 3D octahedron
 373(`domain_coarsen_3d.py`: `|x| + |y| + |z| ≤ t`, 6-neighbour adjacency). Both are connected at every
 374radius for the same reason, supplied once by the descent criterion: the L1 norm is a height with a
 375unique zero at the origin, and from any other cell a single step toward the origin is a lattice edge
 376to a strictly-lower cell. So the interface bound holds on the actual structures the simulation
 377evolves, for every radius, as a THEOREM (no fixed size, no `decide`). This closes the "wire the
 378specific lattice graph" step left routine-but-open in Phases 13/14/15. -/
 379
 380namespace Diamond
 381
 382/-- The 2D diamond of radius `t`: the L1 ball `|x| + |y| ≤ t` as a finite set of lattice points.
 383The bounding box makes it a `Finset`; the L1 filter carves out the diamond. -/
 384def ball (t : ℕ) : Finset (ℤ × ℤ) :=
 385  (Finset.Icc (-(t : ℤ), -(t : ℤ)) ((t : ℤ), (t : ℤ))).filter
 386    (fun p => p.1.natAbs + p.2.natAbs ≤ t)
 387
 388theorem mem_ball_iff (t : ℕ) (x y : ℤ) : (x, y) ∈ ball t ↔ x.natAbs + y.natAbs ≤ t := by
 389  unfold ball
 390  simp only [Finset.mem_filter, Finset.mem_Icc, Prod.mk_le_mk]
 391  constructor
 392  · rintro ⟨_, h⟩; exact h
 393  · intro h; exact ⟨⟨⟨by omega, by omega⟩, by omega, by omega⟩, h⟩
 394
 395/-- Vertices of the diamond: lattice points in the ball. The `Finset` coercion provides `Fintype`
 396and `DecidableEq` automatically. -/
 397abbrev Vtx (t : ℕ) := {p : ℤ × ℤ // p ∈ ball t}
 398
 399/-- L1 height of a diamond vertex (its graph-distance potential toward the centre). -/
 400def height (t : ℕ) (v : Vtx t) : ℕ := v.val.1.natAbs + v.val.2.natAbs
 401
 402/-- The centre of the diamond is a vertex (the origin lies in every ball). -/
 403def center (t : ℕ) : Vtx t := ⟨(0, 0), by rw [mem_ball_iff]; omega⟩
 404
 405instance (t : ℕ) : Nonempty (Vtx t) := ⟨center t⟩
 406
 407/-- 4-neighbour adjacency: L1 distance exactly one. -/
 408def adj (p q : ℤ × ℤ) : Prop := (p.1 - q.1).natAbs + (p.2 - q.2).natAbs = 1
 409
 410instance : DecidableRel adj := fun p q => by unfold adj; infer_instance
 411
 412/-- The 4-neighbour edge list of the diamond: every adjacent ordered pair of vertices. -/
 413noncomputable def edges (t : ℕ) : List (Vtx t × Vtx t) :=
 414  (Finset.univ.filter (fun pr : Vtx t × Vtx t => adj pr.1.val pr.2.val)).toList
 415
 416theorem mem_edges (t : ℕ) (a b : Vtx t) : (a, b) ∈ edges t ↔ adj a.val b.val := by
 417  unfold edges
 418  rw [Finset.mem_toList, Finset.mem_filter]
 419  simp [Finset.mem_univ]
 420
 421/-- A zero-height diamond vertex is the centre. -/
 422theorem hzero (t : ℕ) : ∀ v : Vtx t, height t v = 0 → v = center t := by
 423  rintro ⟨⟨x, y⟩, hmem⟩ h0
 424  simp only [height] at h0
 425  apply Subtype.ext
 426  have hx : x = 0 := by omega
 427  have hy : y = 0 := by omega
 428  subst hx; subst hy; rfl
 429
 430/-- From any off-centre diamond vertex there is a 4-neighbour edge to a strictly-lower cell: step the
 431larger-magnitude coordinate one unit toward the origin. -/
 432theorem descent (t : ℕ) :
 433    ∀ v : Vtx t, height t v ≠ 0 →
 434      ∃ u, ((v, u) ∈ edges t ∨ (u, v) ∈ edges t) ∧ height t u < height t v := by
 435  rintro ⟨⟨x, y⟩, hmem⟩ hv
 436  simp only [height] at hv
 437  rw [mem_ball_iff] at hmem
 438  rcases lt_trichotomy x 0 with hx | hx | hx
 439  · refine ⟨⟨(x + 1, y), ?_⟩, Or.inl ?_, ?_⟩
 440    · rw [mem_ball_iff]; omega
 441    · rw [mem_edges]; unfold adj; dsimp only; omega
 442    · simp only [height]; omega
 443  · subst hx
 444    rcases lt_trichotomy y 0 with hy | hy | hy
 445    · refine ⟨⟨(0, y + 1), ?_⟩, Or.inl ?_, ?_⟩
 446      · rw [mem_ball_iff]; omega
 447      · rw [mem_edges]; unfold adj; dsimp only; omega
 448      · simp only [height]; omega
 449    · exfalso; omega
 450    · refine ⟨⟨(0, y - 1), ?_⟩, Or.inl ?_, ?_⟩
 451      · rw [mem_ball_iff]; omega
 452      · rw [mem_edges]; unfold adj; dsimp only; omega
 453      · simp only [height]; omega
 454  · refine ⟨⟨(x - 1, y), ?_⟩, Or.inl ?_, ?_⟩
 455    · rw [mem_ball_iff]; omega
 456    · rw [mem_edges]; unfold adj; dsimp only; omega
 457    · simp only [height]; omega
 458
 459/-- **The interface bound on the 2D diamond, every radius.** For any charge field `c` on the diamond
 460of radius `t`, the number of locked (monochromatic) 4-connected domains is at most the number of
 461bichromatic interface edges plus one. THEOREM for all radii, on the exact lattice the 2D engine runs
 462on. -/
 463theorem mono_le_interface_succ {β : Type*} [DecidableEq β] (t : ℕ) (c : Vtx t → β) :
 464    comp ((edges t).filter (fun p => decide (c p.1 = c p.2)))
 465      ≤ ((edges t).filter (fun p => decide (c p.1 ≠ c p.2))).length + 1 :=
 466  mono_le_interface_of_descent (edges t) c (height t) (center t) (hzero t) (descent t)
 467
 468end Diamond
 469
 470namespace Octahedron
 471
 472/-- The 3D octahedron of radius `t`: the L1 ball `|x| + |y| + |z| ≤ t` as a finite set of points. -/
 473def ball (t : ℕ) : Finset (ℤ × ℤ × ℤ) :=
 474  (Finset.Icc (-(t : ℤ), -(t : ℤ), -(t : ℤ)) ((t : ℤ), (t : ℤ), (t : ℤ))).filter
 475    (fun p => p.1.natAbs + p.2.1.natAbs + p.2.2.natAbs ≤ t)
 476
 477theorem mem_ball_iff (t : ℕ) (x y z : ℤ) :
 478    (x, y, z) ∈ ball t ↔ x.natAbs + y.natAbs + z.natAbs ≤ t := by
 479  unfold ball
 480  simp only [Finset.mem_filter, Finset.mem_Icc, Prod.mk_le_mk]
 481  constructor
 482  · rintro ⟨_, h⟩; exact h
 483  · intro h; exact ⟨⟨⟨by omega, by omega, by omega⟩, by omega, by omega, by omega⟩, h⟩
 484
 485/-- Vertices of the octahedron: lattice points in the ball. -/
 486abbrev Vtx (t : ℕ) := {p : ℤ × ℤ × ℤ // p ∈ ball t}
 487
 488/-- L1 height of an octahedron vertex. -/
 489def height (t : ℕ) (v : Vtx t) : ℕ := v.val.1.natAbs + v.val.2.1.natAbs + v.val.2.2.natAbs
 490
 491/-- The centre of the octahedron is a vertex. -/
 492def center (t : ℕ) : Vtx t := ⟨(0, 0, 0), by rw [mem_ball_iff]; omega⟩
 493
 494instance (t : ℕ) : Nonempty (Vtx t) := ⟨center t⟩
 495
 496/-- 6-neighbour adjacency: L1 distance exactly one. -/
 497def adj (p q : ℤ × ℤ × ℤ) : Prop :=
 498  (p.1 - q.1).natAbs + (p.2.1 - q.2.1).natAbs + (p.2.2 - q.2.2).natAbs = 1
 499
 500instance : DecidableRel adj := fun p q => by unfold adj; infer_instance
 501
 502/-- The 6-neighbour edge list of the octahedron. -/
 503noncomputable def edges (t : ℕ) : List (Vtx t × Vtx t) :=
 504  (Finset.univ.filter (fun pr : Vtx t × Vtx t => adj pr.1.val pr.2.val)).toList
 505
 506theorem mem_edges (t : ℕ) (a b : Vtx t) : (a, b) ∈ edges t ↔ adj a.val b.val := by
 507  unfold edges
 508  rw [Finset.mem_toList, Finset.mem_filter]
 509  simp [Finset.mem_univ]
 510
 511/-- A zero-height octahedron vertex is the centre. -/
 512theorem hzero (t : ℕ) : ∀ v : Vtx t, height t v = 0 → v = center t := by
 513  rintro ⟨⟨x, y, z⟩, hmem⟩ h0
 514  simp only [height] at h0
 515  apply Subtype.ext
 516  have hx : x = 0 := by omega
 517  have hy : y = 0 := by omega
 518  have hz : z = 0 := by omega
 519  subst hx; subst hy; subst hz; rfl
 520
 521/-- From any off-centre octahedron vertex there is a 6-neighbour edge to a strictly-lower cell. -/
 522theorem descent (t : ℕ) :
 523    ∀ v : Vtx t, height t v ≠ 0 →
 524      ∃ u, ((v, u) ∈ edges t ∨ (u, v) ∈ edges t) ∧ height t u < height t v := by
 525  rintro ⟨⟨x, y, z⟩, hmem⟩ hv
 526  simp only [height] at hv
 527  rw [mem_ball_iff] at hmem
 528  rcases lt_trichotomy x 0 with hx | hx | hx
 529  · refine ⟨⟨(x + 1, y, z), ?_⟩, Or.inl ?_, ?_⟩
 530    · rw [mem_ball_iff]; omega
 531    · rw [mem_edges]; unfold adj; dsimp only; omega
 532    · simp only [height]; omega
 533  · subst hx
 534    rcases lt_trichotomy y 0 with hy | hy | hy
 535    · refine ⟨⟨(0, y + 1, z), ?_⟩, Or.inl ?_, ?_⟩
 536      · rw [mem_ball_iff]; omega
 537      · rw [mem_edges]; unfold adj; dsimp only; omega
 538      · simp only [height]; omega
 539    · subst hy
 540      rcases lt_trichotomy z 0 with hz | hz | hz
 541      · refine ⟨⟨(0, 0, z + 1), ?_⟩, Or.inl ?_, ?_⟩
 542        · rw [mem_ball_iff]; omega
 543        · rw [mem_edges]; unfold adj; dsimp only; omega
 544        · simp only [height]; omega
 545      · exfalso; omega
 546      · refine ⟨⟨(0, 0, z - 1), ?_⟩, Or.inl ?_, ?_⟩
 547        · rw [mem_ball_iff]; omega
 548        · rw [mem_edges]; unfold adj; dsimp only; omega
 549        · simp only [height]; omega
 550    · refine ⟨⟨(0, y - 1, z), ?_⟩, Or.inl ?_, ?_⟩
 551      · rw [mem_ball_iff]; omega
 552      · rw [mem_edges]; unfold adj; dsimp only; omega
 553      · simp only [height]; omega
 554  · refine ⟨⟨(x - 1, y, z), ?_⟩, Or.inl ?_, ?_⟩
 555    · rw [mem_ball_iff]; omega
 556    · rw [mem_edges]; unfold adj; dsimp only; omega
 557    · simp only [height]; omega
 558
 559/-- **The interface bound on the 3D octahedron, every radius.** For any charge field `c` on the
 560octahedron of radius `t`, the number of locked (monochromatic) 6-connected domains is at most the
 561number of bichromatic interface edges plus one. THEOREM for all radii, on the exact lattice the 3D
 562engine runs on (D = 3 is the dimension the forcing chain selects). -/
 563theorem mono_le_interface_succ {β : Type*} [DecidableEq β] (t : ℕ) (c : Vtx t → β) :
 564    comp ((edges t).filter (fun p => decide (c p.1 = c p.2)))
 565      ≤ ((edges t).filter (fun p => decide (c p.1 ≠ c p.2))).length + 1 :=
 566  mono_le_interface_of_descent (edges t) c (height t) (center t) (hzero t) (descent t)
 567
 568end Octahedron
 569
 570end InterfaceComponentBound
 571end Cosmology
 572end IndisputableMonolith
 573