runs_eq
plain-language theorem explainer
For any nonempty charge field, the number of maximal equal-charge runs equals the number of adjacent unequal pairs plus one. Cosmologists and RS auditors cite this as the 1D domain-coarsening cost law: carried super-regions track forced distinctions, not volume. Proof is induction on the tail with a case split on whether the head equals the next element.
Claim. For every charge type $\alpha$ with decidable equality, every $a \in \alpha$, and every list $\ell$ of charges, the number of maximal equal-charge runs in $a{::}\ell$ equals the number of adjacent unequal pairs in $a{::}\ell$ plus one: $\mathrm{runs}(a{::}\ell) = \mathrm{boundaries}(a{::}\ell) + 1$.
background
The module models a recognition charge field along the ladder as a finite list of values in a type $\alpha$ with decidable equality (the threshold-0 same-charge test). Two adjacent entries form a forced distinction exactly when they differ; a maximal contiguous block of equal charges is a locked domain and coarsens losslessly into one super-region.
boundaries counts forced distinctions: it is $0$ on empty and singleton lists, and on $a{::}b{::}\ell$ adds $1$ if $a \neq b$ (else $0$) and recurses. runs counts maximal equal-charge runs (the coarse super-regions the engine carries): $0$ on empty, $1$ on a singleton, and the same recursive step as boundaries but with base $1$ on length one. The module status is a pure theorem (no sorry, no extra axioms beyond Mathlib).
This is the formal core of Phase-12 domain coarsening: carry each locked domain at the coarsest rung its recognition allows, in one $O(1)$ step, independent of run length.
proof idea
Induction on the tail $\ell$, generalizing over the head $a$.
Base case $\ell = []$: both sides simplify to $1 = 0 + 1$.
Inductive step $\ell = b{::}t$: unfold both runs and boundaries on $a{::}b{::}t$ to expose the shared indicator $(a = b \mapsto 0,, a \neq b \mapsto 1)$. Rewrite the inductive hypothesis at head $b$, then case-split on $a = b$. In each branch the indicators match and omega closes the arithmetic identity $(0\text{ or }1) + (\mathrm{boundaries}(b{::}t) + 1) = ((0\text{ or }1) + \mathrm{boundaries}(b{::}t)) + 1$.
why it matters
This is the headline identity of DomainCoarsening: carried cost is set by the interface, never by volume. A field of length $N$ made of two constant blocks ($\mathrm{boundaries} = 1$) is carried as exactly two super-regions no matter how large $N$ is. Downstream, carried_cost_tracks_distinctions packages it with the volume bound as the sub-extensivity statement the engine needs; runs_le_length is the companion inequality; the 2D module lifts it row-wise as runs_eq_of_ne_nil.
Composed with the cadence bound (at most one resolution per tick) and open-system dynamics (bulk blocks grow linearly while the active interface grows diffusively), it is the formal core of "engine cost is sub-extensive in the volume." Minimality is immediate: each distinction forces a new block, so runs is also the least number of constant contiguous blocks any lossless cover can use. Landmark contact is the phi-rung coarsening story (T-1 RungCoarsen internal cost zero on equal members; T-2 IdleFastForward one-step carry), not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.