Cosmology Domain Coarsening2 D

The two-dimensional cost law

Domain coarsening is the step where a fine-grained field, a grid of cells each carrying a charge, is compressed into larger regions of equal charge. In one dimension this compression is exact: a line of cells splits into runs, and the number of runs always equals the number of internal boundaries plus one. A boundary is a place where neighboring cells differ. The identity runs = boundaries + 1 is a proved theorem in the machine-checked library, and it holds because a one-dimensional interface between two regions is a single point.

The two-dimensional case is harder because an interface can be multiply connected: a region can wrap around another, or touch it in several separate arcs. The exact equality becomes an inequality. The library proves, as a dimension-free theorem about connected graphs, that the number of monochromatic components is at most the number of bichromatic edges plus one. This is a component-counting fact under edge deletion, and it is the hard mathematical content that the library supplies. The specific two-dimensional diamond lattice is an instance of the connected-ambient hypothesis; wiring that lattice graph into the theorem is routine and remains a stated step.

What the module proves cleanly is the separable, row-wise coarsening cost. Model the two-dimensional field as a list of rows. Let rowCost be the total number of one-dimensional super-regions when each row is coarsened independently, and let rowInterface be the total horizontal interface, the sum of boundaries over rows. The headline theorem rowwise_cost_eq states that for any grid whose rows are all nonempty,

rowCost rows = rowInterface rows + rows.length.

In words: the separable coarsening carries exactly the horizontal interface plus the number of rows super-regions. This is the per-axis generalization of the one-dimensional law, summed over rows. It depends only on the interface and the row count, never on the row widths, which means never on the area. The true two-dimensional component coarsening also merges vertically, so it is never worse: it carries at most this many super-regions. Composed with the resolution cost bound, the two-dimensional engine's state and work are both bounded by the interface, not the area.

The consequence for cosmology is direct. In a recognition-based account of the early universe, the cost of tracking a coarsening domain structure is set by its perimeter, a sub-extensive quantity. A large region costs little to carry; the expensive parts are the borders where recognition is active. The module turns that physical intuition into a proved bound, and the bound is what makes the two-dimensional coarsening tractable at all.

/-- The 1D cost law as a row lemma: a nonempty row coarsens into (its horizontal interface) + 1 super-regions. -/
theorem runs_eq_of_ne_nil (r : List α) (h : r ≠ []) : runs r = boundaries r + 1 := by
  cases r with
  | nil => exact absurd rfl h
  | cons a l => exact runs_eq a l

/-- The carried cost is bounded by the interface, not the area: the separable coarsening cost is
`rowInterface + rows.length`, with no dependence on the row widths. -/
theorem rowwise_cost_independent_of_width (rows : List (List α)) (h : ∀ r ∈ rows, r ≠ []) :
    rowCost rows = rowInterface rows + rows.length :=
  rowwise_cost_eq rows h

/-- **The separable coarsening cost = horizontal interface + number of rows.** For any 2D grid whose rows are
all nonempty, coarsening each row independently carries exactly (the total horizontal interface) plus (the
number of rows) super-regions. This is the exact per-axis generalization of the 1D law `runs = boundaries + 1`
summed over rows, and it depends only on the interface and the row count, never on the row widths (the area).
The true 2D component coarsening merges vertically as well, so it carries at most this many super-regions. -/
theorem rowwise_cost_eq (rows : List (List α)) (h : ∀ r ∈ rows, r ≠ []) :
    rowCost rows = rowInterface rows + rows.length := by
  induction rows with
  | nil => simp
  | cons r rs ih =>
    rw [rowCost_cons, rowInterface_cons, runs_eq_of_ne_nil r (h r (List.mem_cons.mpr (Or.inl rfl)))]
    rw [ih (fun row hrow => h row (List.mem_cons.mpr (Or.inr hrow)))]
    simp [List.length_cons]
    ring

/-- The carried cost is bounded by the interface, not the area: the separable coarsening cost is
`rowInterface + rows.length`, with no dependence on the row widths. -/
theorem rowwise_cost_independent_of_width (rows : List (List α)) (h : ∀ r ∈ rows, r ≠ []) :
    rowCost rows = rowInterface rows + rows.length :=
  rowwise_cost_eq rows h

What this page does not claim

The exact two-dimensional equality components = bichromatic + 1 is not proved; only the inequality holds. The diamond lattice instance is not fully wired into the theorem; that step remains routine and stated. The module does not prove that the true two-dimensional component coarsening equals the separable row-wise cost.

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/DomainCoarsening2D.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: