Encyclopedia Cosmology Cosmology Interface Component Bound

ARTICLE 4 claims 4 theorems

Cosmology Interface Component Bound

A graph-theoretic theorem with a plain meaning: in any connected world, the number of distinct regions is at most the number of boundary edges plus one.

Verify this page

The interface bound

A map of territories. The map is a connected graph: cells are vertices, and edges connect neighboring cells. Each cell has a color, and a territory is a connected region of cells sharing the same color. The interface is the set of edges where two different colors meet. The theorem states a simple counting fact: the number of territories is at most the number of interface edges plus one. This holds for any finite connected graph, in any dimension, with any number of colors.

For a line of cells (one dimension), the statement is exact: the number of runs equals the number of boundaries plus one. For a two-dimensional grid or a three-dimensional lattice, a territory can wrap around another, so the equality becomes an inequality. The proof is dimension-free. It relies on a classical graph fact: deleting an edge can increase the number of connected components by at most one. Adding the interface edges back to the monochromatic graph reconstructs the connected world, and each added edge can merge at most two territories.

The theorem was previously verified only by numerical checks on the live field each cycle. The gap was that component counting under edge deletion was not available in the standard library. This work closes that gap with a machine-checked proof. The headline result is components(monochromatic graph) ≤ (bichromatic edges) + 1, tagged as a theorem with zero unproved axioms beyond the standard three.

The proof also supplies a reusable criterion for connectivity: a finite world with a height function that has a unique zero and a descent edge from every other cell is connected. This is the recognition law's own pull toward the coarsest description, read as graph connectivity. The construction instantiates this criterion for the exact lattices the engine runs on: the two-dimensional diamond (the L1 ball |x| + |y| ≤ t with 4-neighbor adjacency) and the three-dimensional octahedron (|x| + |y| + |z| ≤ t with 6-neighbor adjacency). For every radius t, the bound holds: locked domains ≤ interface + 1.

In Recognition Science, this bound is not an isolated graph fact. It is the formal backbone of domain coarsening, the process by which the engine merges cells into larger regions. The bound guarantees that the number of regions the engine must track is always controlled by the size of the interface, not by the total number of cells. This is what makes the coarsening step computationally tractable and, more deeply, what makes the recognition of a large world possible at all.

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 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 clos_root_of_descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
clos_root_of_descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean:289 
/-- If a height `h : V → ℕ` has a unique zero `root`, and every cell of positive height has a lattice
edge to a strictly-lower cell, then every cell is connected to `root`. The proof is strong induction
on `h v`: a zero-height cell is the root; a positive-height cell steps down an edge to a cell the
induction hypothesis already connects to the root. -/
theorem clos_root_of_descent [Finite V] (E : List (V × V)) (h : V → ℕ) (root : V)
    (hzero : ∀ v, h v = 0 → v = root)
    (hdesc : ∀ v, h v ≠ 0 → ∃ u, ((v, u) ∈ E ∨ (u, v) ∈ E) ∧ h u < h v) :
    ∀ v, clos E v root := by
  have e := clos_equiv E
  have H : ∀ n, ∀ v, h v = n → clos E v root := by
    intro n
    induction n using Nat.strong_induction_on with
    | _ n ih =>
      intro v hv
      rcases Nat.eq_zero_or_pos (h v) with h0 | hpos
      · rw [hzero v h0]; exact e.refl root
      · have hvne : h v ≠ 0 := by omega
        obtain ⟨u, hedge, hlt⟩ := hdesc v hvne
        have hvu : clos E v u := by
          rcases hedge with he | he
          · exact Relation.EqvGen.rel v u he
          · exact e.symm (Relation.EqvGen.rel u v he)
        have hur : clos E u root := ih (h u) (by omega) u rfl
        exact e.trans hvu hur
  intro v
  exact H (h v) v rfl
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

What this page does not claim

The bound is not a statement about the number of colors or the size of the alphabet. The theorem does not require the graph to be planar or to have any particular embedding. The construction does not provide a constructive algorithm to find the territories, only a bound on their count.

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