Cosmology Domain Coarsening2 D Row Cost

The row-wise cost bound

In the Recognition Science framework, a ledger (a discrete record of events) tracks how many distinct regions appear when a field of cells is coarsened into uniform blocks. The declaration rowCost defines the separable cost: it takes a grid as a list of rows, coarsens each row independently, and sums the resulting region counts. Its companion rowInterface sums the horizontal boundaries between differing cells within each row. Together they answer a concrete question: if you simplify a 2D field row by row, how many coarse regions do you carry?

The headline theorem rowwise_cost_eq proves, for any grid whose rows are all nonempty, that rowCost rows = rowInterface rows + rows.length. In plain language, the separable coarsening cost equals the total horizontal interface plus the number of rows. This is the exact per-axis generalization of the 1D law runs = boundaries + 1, summed over rows. The formula depends only on the interface and the row count, never on the row widths: rowwise_cost_independent_of_width states this independence explicitly. The true 2D component coarsening also merges vertically, so it is never worse: the bound components_2D <= rowCost holds, making rowCost a clean upper bound on the carried 2D cost.

The practical consequence is that the engine's state and work scale with the interface, not the area. A large grid with few internal boundaries costs little to coarsen, while a small grid with many boundaries costs more. This sub-extensive scaling is what makes the 2D recognition engine tractable: the cost localizes to the perimeter of domains, not their interior. The theorem is machine-checked in the framework's library of formal theorems, with zero unproven assumptions beyond the standard three axioms of the ambient type theory.

What rowCost does not claim is equally precise. It does not prove that the true 2D component count equals rowInterface + rows.length; that equality fails because a 2D interface can be multiply connected. The module proves only the inequality components_2D <= rowCost, not equality. Nor does it establish the physical bridge from recognition to linking in three dimensions; that remains open. The theorem is a mathematical bound on a specific coarsening scheme, not a claim about the actual physics of domain growth.

/-- **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 prove equality between the true 2D component count and rowInterface + rows.length. The theorem does not establish the physical bridge from recognition to linking in three dimensions. The bound applies to the separable row-wise coarsening scheme, not to every possible coarsening method.

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: