Encyclopedia Cosmology Cosmology Interface Component Bound Connected Of Descent

ARTICLE 4 claims 4 theorems

Cosmology Interface Component Bound Connected Of Descent

A finite world is one connected piece if every cell can step downhill to a single lowest cell, a fact the Recognition Science framework proves and then uses to bound its own domain counts.

Verify this page

The descent criterion

In graph theory, a finite set of cells with adjacency links is connected when you can travel from any cell to any other along the links. The declaration connected_of_descent gives a simple sufficient condition: if every cell has a whole-number height, exactly one cell has height zero, and every other cell has a link to some cell of strictly smaller height, then the whole set is one component. The proof is a descent argument: from any cell, repeatedly follow the smaller-height link; the heights are natural numbers, so the process must end, and it can only end at the unique zero cell. That cell is reachable from everywhere, so the graph is connected.

The condition is not necessary. A connected graph can fail it: a simple cycle of three cells, each linked to the other two, is connected, but no assignment of distinct heights makes every non-minimal cell adjacent to a strictly lower one. The criterion is a tool for proving connectivity in worlds that have a natural height, not a characterization of all connected graphs.

In Recognition Science, the framework models a finite world as a set of cells with a charge value on each cell. Cells with equal charge form locked domains; cells with different charge form the interface between domains. The framework's library, a machine-checked collection of formal theorems, proves that on any connected world, the number of locked domains is at most the number of interface edges plus one. That bound needs the world to be connected, and connected_of_descent supplies that hypothesis for the specific lattices the engine runs on: the 2D diamond (points whose x and y absolute values sum to at most t, with 4-neighbor adjacency) and the 3D octahedron (same with z, 6-neighbor adjacency). In both, the height is the L1 norm, the unique zero is the origin, and the descent theorem is proved for every radius t.

The consequence is a dimension-free bound on domain count, instantiated on the exact lattices the engine evolves. For the diamond and octahedron of any size, locked domains never exceed interface edges plus one. This turns a previously numeric check into a formal theorem, valid for all radii, not just the ones tested.

The criterion does not claim that every connected world has such a height, nor that the descent condition is necessary. It also does not claim anything about the number of locked domains on a disconnected world; the bound explicitly assumes connectivity. The framework's own physical claim, that recognition drives the pull toward coarser descriptions, is read here only as graph connectivity, not as a statement about actual cosmology.

THEOREM comp · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean
comp · IndisputableMonolith/Cosmology/InterfaceComponentBound.lean:68 
/-- The number of connected components (locked domains) of the graph with edge list `E`. Uses
`Nat.card`, so it is well-defined for any `Finite V` with no decidability hypothesis on the closure. -/
noncomputable def comp (E : List (V × V)) : ℕ := Nat.card (Quotient (cs E))
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
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 descent criterion is not necessary for connectivity; a cycle of three cells is connected but has no such height. The bound does not apply to disconnected worlds. The framework's physical claim about recognition pulling toward coarser descriptions is not established by this theorem; only the graph connectivity is.

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