Encyclopedia Cosmology Cosmology Interface Component Bound Mono Le Interface Succ
ARTICLE 5 claims 5 theorems
Cosmology Interface Component Bound Mono Le Interface Succ
A machine-checked theorem sets a strict limit on how many distinct regions a discrete world can contain, based on the size of its boundary.
The interface bound
In any connected graph, the number of connected regions you get after removing some edges is at most the number of removed edges plus one. This is a classical fact about graphs, and it has a direct consequence for any discrete model of space: the number of distinct zones, or locked domains, cannot exceed the number of boundary edges separating them, plus one. The Recognition Science framework's library of formal theorems proves this bound for the specific lattices its cosmology engine actually evolves.
The framework models a finite world as a set of cells, each assigned a charge or color. Edges connect neighboring cells. Edges joining cells of the same color generate the locked domains; edges joining cells of different colors form the interface, or boundary. The theorem, named mono_le_interface_succ, states that the number of locked domains is at most the number of interface edges plus one, on any connected world in any dimension. In one dimension this is an exact equality: runs equal boundaries plus one. In two and three dimensions, where a boundary can loop around itself, the equality weakens to this inequality.
The proof is dimension-free. It relies on the simple observation that adding an interface edge back to the monochromatic graph can merge at most two locked domains into one. Starting from the monochromatic graph and adding back all interface edges reconstructs the connected world. Each added edge reduces the component count by at most one, so the original count is bounded by the number of added edges plus one. The formal proof handles the delicate case where a new edge collapses two domains into one, using an injection argument that is injective away from the single merged class.
The theorem takes connectivity as a hypothesis. The framework also proves that its standard lattices satisfy this hypothesis. A finite world with a height function that has a unique zero and a descent edge from every other cell is connected. The 2D diamond, the L1 ball in the plane with 4-neighbor adjacency, and the 3D octahedron, the L1 ball in space with 6-neighbor adjacency, both satisfy this criterion using the L1 norm as height. This gives the bound on the exact lattices the engine runs on, for every radius, with no fixed size and no brute-force checking.
What this establishes is a structural ceiling: the number of distinct regions a discrete world can maintain is strictly limited by the size of its boundary. This is a constraint on the engine's internal bookkeeping, not a claim about physical space itself. The theorem does not say that the bound is tight, nor that every world achieves it. It does not say anything about the number of dimensions being forced. It does not claim that the interface size itself is determined by the framework. The bound is a necessary condition, not a sufficient one, and it applies only to the specific lattices named, not to arbitrary graphs.
THEOREM comp_le_comp_append · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- **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]
THEOREM mono_components_le_bichromatic_succ · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- **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
/-- 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 clos_root_of_descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- 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 descent · descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- 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 theorem does not state that the bound is tight or achieved by any specific world. The theorem does not claim anything about the number of spatial dimensions being forced. The theorem does not apply to arbitrary graphs, only to the specific lattices named.
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:
- What determines the size of the interface itself in the framework's cosmology engine?
- Does the bound become tight for any of the lattices the engine evolves?
- How does the framework's notion of locked domain relate to physical regions in continuous space?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM comp_le_comp_append · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- **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]In any connected graph, the number of connected regions you get after removing some edges is at most the number of removed edges plus one. comp_le_comp_append · IndisputableMonolith/Cosmology/InterfaceComponentBound.leanTHEOREM mono_components_le_bichromatic_succ · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- **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 omegaThe number of locked domains is at most the number of interface edges plus one, on any connected world in any dimension. mono_components_le_bichromatic_succ · IndisputableMonolith/Cosmology/InterfaceComponentBound.leanTHEOREM card_le_succ_of_merge · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- 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] omegaAdding an interface edge back to the monochromatic graph can merge at most two locked domains into one. card_le_succ_of_merge · IndisputableMonolith/Cosmology/InterfaceComponentBound.leanTHEOREM clos_root_of_descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- 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 rflA finite world with a height function that has a unique zero and a descent edge from every other cell is connected. clos_root_of_descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.leanTHEOREM descent · descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
/-- 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]; omegaThe 2D diamond and the 3D octahedron both satisfy this criterion using the L1 norm as height. descent · descent · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean