Pith. sign in
module module high

IndisputableMonolith.Cosmology.DomainCoarsening2D

show as:
view Lean formalization →

Lifts the 1D locked-domain cost law to single rows of a 2D charge grid: a nonempty row coarsens into exactly its horizontal interface count plus one super-region. Cosmology formalizers cite it when stepping from 1D coarsening toward the surface-cost theorem in 3D. Argument is structural induction on list rows, with recursive cost and interface defs and a width-independence lemma.

claimFor a nonempty row $r$ of recognition charges, locked-domain coarsening yields $\mathrm{cost}(r)=I_{\parallel}(r)+1$, where $I_{\parallel}(r)$ is the number of horizontal charge transitions (interfaces) in $r$. The rowwise cost depends only on the run structure of $r$, not on ambient grid width.

background

Upstream DomainCoarsening proves the Phase-12 fact: when each LOCKED DOMAIN (a maximal run of equal recognition charge, carrying no internal distinction) is stored as one coarse super-region, the number of super-regions equals the number of forced distinctions plus one. That is the coarsest lossless representation size.

This module specializes that law to one row of a 2D grid. A row is a finite list of charges; equal adjacent entries form a run. The horizontal interface counts positions where neighboring charges differ. Cost and interface are defined by recursion on the list (empty and cons cases), so the 1D identity becomes a row lemma.

The local setting is intermediate: pure 1D coarsening below, and the 3D surface-cost theory (selected by T8, $D=3$) above.

proof idea

Not a single theorem wrapper: a small inductive package. rowCost and rowInterface are defined by structural recursion on lists, with explicit nil and cons equations. Base lemmas discharge the empty row; cons lemmas unwind one head charge against the tail run structure. The identity rowwise_cost_eq then shows nonempty rows satisfy cost = interface + 1, using the run-count fact for nonempty lists. A companion result proves the rowwise cost is independent of ambient width, so only the charge sequence matters.

why it matters in Recognition Science

Direct import parent of DomainCoarsening3D, whose doc-comment states the target: "the cost lives on a surface, not in the volume," backing the 3D cosmogenesis script in the dimension the forcing chain selects (T8: $D=3$). Once every row obeys cost = horizontal interface + 1, stacking rows and adding vertical interfaces localizes recognition cost to a 2D surface of domain boundaries. That closes the Phase-12 coarsening ladder from 1D through this 2D row step into physically selected three-space, without volume-extensive bookkeeping.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)