Encyclopedia Cosmology Cosmology Interface Component Bound Card Le Succ Of Merge

ARTICLE 3 claims 3 theorems

Cosmology Interface Component Bound Card Le Succ Of Merge

A machine-checked theorem shows that merging cells one at a time can never reduce the number of regions by more than one per merge, a fact that underpins how recognition systems count their own structure.

Verify this page

The merge bound

A grid of cells, each carrying a color. Cells of the same color that touch form a region; cells of different colors that touch form a boundary. The question is simple: how many regions can there be? A machine-checked theorem in the Recognition Science framework answers this with a clean inequality: the number of regions is at most the number of boundary edges plus one. This holds for any connected grid in any dimension, from a line to a cube.

The proof rests on a basic observation about merging. If you take two regions and weld them together, the total count drops by exactly one. So if you start with a world of separate cells and add back the boundary edges one at a time, each edge can merge at most two regions. The theorem card_le_succ_of_merge (a formal statement in the framework's machine-checked library) captures this: if a function maps a set A onto a set B, and the only way two distinct elements of A can map to the same element of B is if one of them is a special element, then the size of A is at most the size of B plus one. That special element is the one region that a new edge can collapse into.

This abstract bound becomes concrete on the lattices the framework actually uses. In two dimensions, the diamond-shaped grid of points where |x| + |y| ≤ t, and in three dimensions, the octahedral grid where |x| + |y| + |z| ≤ t, the theorem applies directly. The framework proves that on these exact grids, for any radius t, the number of locked domains (the regions the recognition process settles on) is at most the number of interface edges plus one. This was previously only checked numerically on live simulations; now it is a proved theorem, valid for every size of grid at once.

The theorem does not claim that the bound is always an equality. In one dimension, the number of regions is exactly the number of boundaries plus one. In two and three dimensions, a boundary can loop around and touch itself, so the count can be less than the bound. The theorem also assumes the world is connected; a world split into separate islands would need a different bound. And the theorem says nothing about what the colors mean, only about how many regions a given coloring can produce.

What the bound changes is the practical question of how much structure a recognition process can carry. If the interface is small, the number of distinct regions is small, no matter how the colors are arranged. That is a constraint on the world itself, not on any particular simulation, and it is now a permanent fact in the framework's library.

THEOREM mono_components_le_bichromatic_succ · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
mono_components_le_bichromatic_succ · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean:254 
/-- **Locked domains are at most the interface plus one.** For a connected finite world with edge
list `E` and charge `c`, the number of monochromatic connected components (the locked domains the
engine carries) is at most the number of bichromatic edges (the recognition-active interface) plus
one. This is the dimension-free form of the 1D identity `runs = boundaries + 1`. -/
theorem mono_components_le_bichromatic_succ {β : Type*} [Finite V] [Nonempty V] [DecidableEq β]
    (E : List (V × V)) (c : V → β)
    (hconn : ∀ u v : V, clos E u v) :
    comp (E.filter (fun p => decide (c p.1 = c p.2)))
      ≤ (E.filter (fun p => decide (c p.1 ≠ c p.2))).length + 1 := by
  set mono := E.filter (fun p => decide (c p.1 = c p.2)) with hmono
  set bi := E.filter (fun p => decide (c p.1 ≠ c p.2)) with hbi
  have hsplit : ∀ p, p ∈ mono ++ bi ↔ p ∈ E := by
    intro p
    simp only [hmono, hbi, List.mem_append, List.mem_filter, decide_eq_true_eq]
    constructor
    · rintro (⟨hp, _⟩ | ⟨hp, _⟩) <;> exact hp
    · intro hp
      by_cases hc : c p.1 = c p.2
      · exact Or.inl ⟨hp, hc⟩
      · exact Or.inr ⟨hp, hc⟩
  have h1 : comp mono ≤ comp (mono ++ bi) + bi.length := comp_le_comp_append mono bi
  have h2 : comp (mono ++ bi) = comp E := comp_congr hsplit
  have h3 : comp E = 1 := comp_eq_one_of_connected E hconn
  rw [h2, h3] at h1
  omega
THEOREM card_le_succ_of_merge · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
card_le_succ_of_merge · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean:151 
/-- A surjection that collapses at most one pair (everything maps injectively except possibly into a
single class) loses at most one element of cardinality. -/
theorem card_le_succ_of_merge {A B : Type*} [Finite B]
    (f : A → B) (β : A) (hmerge : ∀ x y, f x = f y → x = y ∨ x = β ∨ y = β) :
    Nat.card A ≤ Nat.card B + 1 := by
  classical
  have hinj : Function.Injective
      (fun x : A => if x = β then (none : Option B) else some (f x)) := by
    intro x y hxy
    dsimp only at hxy
    by_cases hx : x = β <;> by_cases hy : y = β
    · exact hx.trans hy.symm
    · rw [if_pos hx, if_neg hy] at hxy; exact absurd hxy (by simp)
    · rw [if_neg hx, if_pos hy] at hxy; exact absurd hxy (by simp)
    · rw [if_neg hx, if_neg hy] at hxy
      have hf : f x = f y := Option.some.inj hxy
      rcases hmerge x y hf with h | h | h
      · exact h
      · exact absurd h hx
      · exact absurd h hy
  have hcard := Nat.card_le_card_of_injective _ hinj
  haveI := Fintype.ofFinite B
  have hoption : Nat.card (Option B) = Nat.card B + 1 := by
    rw [← Fintype.card_eq_nat_card, ← Fintype.card_eq_nat_card, Fintype.card_option]
  omega
THEOREM descent · descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean:430 
/-- From any off-centre diamond vertex there is a 4-neighbour edge to a strictly-lower cell: step the
larger-magnitude coordinate one unit toward the origin. -/
theorem descent (t : ℕ) :
    ∀ v : Vtx t, height t v ≠ 0 →
      ∃ u, ((v, u) ∈ edges t ∨ (u, v) ∈ edges t) ∧ height t u < height t v := by
  rintro ⟨⟨x, y⟩, hmem⟩ hv
  simp only [height] at hv
  rw [mem_ball_iff] at hmem
  rcases lt_trichotomy x 0 with hx | hx | hx
  · refine ⟨⟨(x + 1, y), ?_⟩, Or.inl ?_, ?_⟩
    · rw [mem_ball_iff]; omega
    · rw [mem_edges]; unfold adj; dsimp only; omega
    · simp only [height]; omega
  · subst hx
    rcases lt_trichotomy y 0 with hy | hy | hy
    · refine ⟨⟨(0, y + 1), ?_⟩, Or.inl ?_, ?_⟩
      · rw [mem_ball_iff]; omega
      · rw [mem_edges]; unfold adj; dsimp only; omega
      · simp only [height]; omega
    · exfalso; omega
    · refine ⟨⟨(0, y - 1), ?_⟩, Or.inl ?_, ?_⟩
      · rw [mem_ball_iff]; omega
      · rw [mem_edges]; unfold adj; dsimp only; omega
      · simp only [height]; omega
  · refine ⟨⟨(x - 1, y), ?_⟩, Or.inl ?_, ?_⟩
    · rw [mem_ball_iff]; omega
    · rw [mem_edges]; unfold adj; dsimp only; omega
    · simp only [height]; omega

What this page does not claim

The bound is not an equality in every dimension; in 2D and 3D it can be strictly less than the interface plus one. The theorem does not apply to disconnected worlds. The theorem says nothing about what the colors or regions represent physically.

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/InterfaceComponentBound.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND