Encyclopedia Cosmology Cosmology Interface Component Bound Comp Eq One Of Connected

ARTICLE 3 claims 3 theorems

Cosmology Interface Component Bound Comp Eq One Of Connected

In a connected world, the number of distinct regions the recognition engine can lock onto is at most the number of boundary crossings plus one, a bound now proved for any dimension.

Verify this page

The interface bound

In graph theory, a simple fact governs how many pieces a network can break into: deleting an edge can increase the number of connected components by at most one. The Recognition Science declaration comp_eq_one_of_connected applies that classical fact to the framework's recognition process, where a discrete record of events assigns each cell a charge value. Cells sharing a charge form locked domains, and the boundaries between different charges form the interface. The theorem states that in any connected world, the number of locked domains is at most the number of interface edges plus one.

The result is dimension-free. It holds for any finite graph, whether the cells line up in one dimension, form a 2D grid, or fill a 3D lattice. The proof works by starting with only the monochromatic edges, those connecting cells of equal charge, which generate the locked domains. Adding back the bichromatic edges, those crossing the interface, reconstructs the full connected world. Each added edge can merge at most two domains, so the count grows by at most one per interface edge, yielding the inequality: locked domains ≤ interface edges + 1.

For the specific lattices the engine runs on, the theorem also supplies the connectivity hypothesis. A finite world is connected if it has a height function with a unique zero and a descent edge from every other cell, a criterion the framework's pull toward coarser descriptions satisfies. The 2D diamond, the L1 ball |x| + |y| ≤ t with 4-neighbor adjacency, and the 3D octahedron, |x| + |y| + |z| ≤ t with 6-neighbor adjacency, both instantiate this criterion. This gives locked domains ≤ interface + 1 on those exact lattices for every radius, closing a gap that previously relied only on numeric checks.

What the theorem does not claim is that the bound is tight, that the locked domains are unique, or that the interface itself is connected. A multiply connected interface, such as a ring of one charge surrounding an island of another, still satisfies the inequality but does not reduce to the simple 1D identity where runs equal boundaries plus one. The theorem also assumes the world is connected; a disconnected world can have more domains than the bound allows. The result is a structural guarantee about counting, not a statement about which specific regions the engine will choose.

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 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 tight for all connected worlds; a cycle graph with alternating charges achieves equality, but a star graph does not. The interface edges themselves form a connected subgraph; the theorem only bounds the count of domains they separate. The theorem identifies which locked domains the engine will choose; it only constrains how many can exist.

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