IndisputableMonolith.Cosmology.DomainCoarsening
Defines the 1D locked-domain coarsening cost on a charge sequence: the number of forced distinctions where adjacent sites carry unequal charge. Inside a locked domain (a maximal run of equal charge) the cost is zero. Cosmology and RS-engine work cite it as the atomic interface cost before lifting to 2D. The module is definitional, with elementary list lemmas on runs, boundaries, and cost-tracking.
claimFor a finite charge sequence $c=(c_0,\ldots,c_{n-1})$, the distinction count is $\#\{i:c_i\neq c_{i+1}\}$. The run decomposition partitions $c$ into maximal constant blocks; the carried coarsening cost equals the number of runs minus one (zero on the empty field), and is at most the length of $c$.
background
In Recognition Science cosmology, discrete charge fields encode local recognition state. A locked domain is a maximal connected region of equal charge; inside it no distinction is forced, so the recognition engine pays nothing. Cost arises only at interfaces between domains.
This module works on the line. It introduces the boundary count (adjacent unequal pairs) and the run decomposition (maximal constant blocks). Base facts cover empty and singleton sequences; further lemmas bound the run count by length and identify carried cost with the distinction count.
The setting is preparatory for higher-dimensional coarsening: once the 1D interface cost is exact, a 2D world can treat locked domains as 4-connected components whose recognition-active boundary is a curve.
proof idea
Definition module with supporting list lemmas, not a single deep theorem. Boundaries and runs are defined by recursion on finite sequences. Nil and singleton cases are immediate. Remaining facts (run decomposition identity, runs at most length, carried cost equals distinction count) proceed by induction on list structure, comparing adjacent heads and tails.
why it matters in Recognition Science
Feeds DomainCoarsening2D, which lifts locked-domain coarsening off the line into a 2D world. Downstream, a locked domain is a maximal 4-connected component of equal charge, carried as one coarse super-region, and the recognition-active interface is a 1D curve, so engine cost localizes to a perimeter (sub-extensive in area). That module backs the cosmogenesis domain_coarsen_2d script. The 1D distinction count supplied here is the atomic cost that makes perimeter localization rigorous.
scope and limits
- Does not treat 2D or higher connectivity; that lives in DomainCoarsening2D.
- Does not derive physical constants, mass formulae, or forcing-chain steps T0–T8.
- Does not claim continuum limits or measure-theoretic perimeter formulae.
- Does not address time evolution or dynamical coarsening of domains.