Cosmology Interface Component Bound Mono Components Le Bichromatic Succ

The interface bound

A finite world made of cells, each painted one of several colors. Neighboring cells of the same color clump together into regions; neighboring cells of different colors form the boundaries between them. A simple question: how many regions can there be? The answer, proved as a theorem in the framework's machine-checked library of formal theorems, is that on any connected world the number of same-colored regions is at most the number of boundary edges plus one. In symbols, components(monochromatic graph) ≤ (bichromatic edges) + 1. This is the declaration mono_components_le_bichromatic_succ, a theorem that holds in any dimension for any finite connected graph.

The proof is a classical graph fact wearing a formal coat. Deleting an edge from a connected graph can increase the number of components by at most one; adding edges back merges at most one pair of regions at a time. The theorem formalizes this intuition: it starts with the monochromatic graph, whose components are the locked domains, and adds back the bichromatic edges one by one. Each addition merges at most two regions, so after adding all k boundary edges the component count can have grown by no more than k. Since the ambient world is connected, the final count is 1, and the initial count is therefore at most k + 1. The formal proof uses an injection argument to bound the merge at each step.

Connectivity is a hypothesis, not a free gift. The theorem requires that the whole world is one piece. The library also proves that the specific lattices the engine runs on satisfy this: the 2D diamond (points with |x| + |y| ≤ t, 4-neighbor adjacency) and the 3D octahedron (|x| + |y| + |z| ≤ t, 6-neighbor adjacency) are connected for every radius t. The proof uses a height function, the L1 norm, with a unique zero at the origin and a descent edge from every other cell. This is the recognition law's own pull toward the coarsest description, read as graph connectivity.

In one dimension the bound is an equality: runs = boundaries + 1. In two and three dimensions the interface can be multiply connected, so the equality relaxes to an inequality. The theorem closes a gap that was previously only checked numerically on live fields; it is now a formal theorem with no unproved assumptions beyond the standard three axioms of the ambient type theory.

What the theorem does not claim is just as important. It does not say that the bound is tight, only that it is an upper limit. It does not say that the locked domains are physically meaningful; that is a modeling choice. It does not derive any cosmological constant or particle mass. It is a combinatorial fact about colored graphs, and its role in the framework is to guarantee that the engine's internal representation never carries more regions than the interface can justify.

/-- **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

/-- 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

/-- **Iterated merge bound.** Adding a list `F` of edges lowers the component count by at most
`F.length`. -/
theorem comp_le_comp_append [Finite V] (X F : List (V × V)) :
    comp X ≤ comp (X ++ F) + F.length := by
  induction F with
  | nil => simp
  | cons f F' ih =>
    obtain ⟨a, b⟩ := f
    have hset : ∀ p, p ∈ (a, b) :: (X ++ F') ↔ p ∈ X ++ (a, b) :: F' := by
      intro p
      simp only [List.mem_cons, List.mem_append]
      tauto
    have hstep : comp (X ++ F') ≤ comp (X ++ (a, b) :: F') + 1 := by
      have := comp_le_comp_cons a b (X ++ F')
      rwa [comp_congr hset] at this
    calc comp X ≤ comp (X ++ F') + F'.length := ih
      _ ≤ (comp (X ++ (a, b) :: F') + 1) + F'.length := by omega
      _ = comp (X ++ (a, b) :: F') + (F'.length + 1) := by ring
      _ = comp (X ++ (a, b) :: F') + ((a, b) :: F').length := by simp [List.length_cons]

What this page does not claim

The bound is not claimed to be tight; it is an upper limit. The theorem does not assign physical meaning to the locked domains. The theorem does not derive any cosmological constant or particle mass.

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: