Cosmology Interface Component Bound Clos Root Of Descent

The descent lemma

A graph is connected when a path links every pair of its vertices. The lemma clos_root_of_descent gives a cheap way to prove that a finite graph is connected: assign a whole number height to each vertex, pick one vertex as the root with height zero, and require that every other vertex has an edge leading to a strictly lower vertex. Under those conditions, every vertex is connected to the root, so the graph is one component.

The proof is a descent argument. From any vertex, follow the required edge to a lower vertex, then again, until the height reaches zero. The unique zero-height vertex is the root, so the path ends there. The formal statement in the machine-checked library of formal theorems says that the equivalence closure of the edge relation connects every vertex to the root, which is exactly the definition of being in the same component.

The lemma is dimension-free: it works on any finite vertex type with any edge list. The framework uses it to show that its standard 2D diamond lattice and 3D octahedron lattice are connected, using the L1 norm as the height and the origin as the root. This is the recognition law's own pull toward the coarsest description, read as graph connectivity: the descent edge is the forced move toward a single summary.

The lemma does not claim that the descent edge is unique, that the height function is part of the graph structure, or that the graph is connected without the descent hypothesis. It also does not establish anything about the number of locked domains; that is the job of the separate inequality theorem that this lemma feeds into.

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

What this page does not claim

The descent lemma does not prove that the graph is connected without the descent hypothesis. It does not establish the number of locked domains, only connectivity. It does not claim the descent edge is unique or that the height function is canonical.

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: