Cosmology Domain Coarsening2 D Rowwise Cost Independent Of Width

The row-wise cost bound

When a two-dimensional field is divided into regions of uniform charge, the cost of tracking those regions is a central question. The declaration rowCost, the total number of 1D super-regions when each row is coarsened independently, answers this for a grid modeled as a list of rows. The theorem rowwise_cost_eq proves that for any grid whose rows are all nonempty, the separable coarsening cost equals the total horizontal interface plus the number of rows: rowCost rows = rowInterface rows + rows.length. 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 theorem rowwise_cost_independent_of_width is a direct restatement of this result, highlighting the key consequence: the cost does not scale with the area of the grid. The true 2D component coarsening also merges vertically, so it is never worse than this separable bound. The numeric bound components_2D <= rowCost is proved, and composed with the resolution cost per cadence cycle, the 2D engine's state and work are both bounded by the interface, not the area.

In plain terms, this means that for a two-dimensional world, the cost of recognition is controlled by the length of the boundaries between regions, not by how much space those regions occupy. A large empty area costs nothing extra; only the edges where charges differ matter. This is a structural fact about the coarsening process, not a claim about any specific physical system.

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

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

What this page does not claim

The theorem does not apply to grids with empty rows, which are excluded by the nonempty hypothesis. The theorem does not claim that the true 2D component coarsening equals the separable row-wise cost; it only provides an upper bound. The theorem does not establish the exact 2D analogue of the 1D law, which remains an inequality rather than an identity.

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: