runs
plain-language theorem explainer
Counts the number of maximal equal-charge runs in a finite charge field, i.e. how many coarse super-regions the domain-coarsening engine carries. Anyone citing the Phase-12 coarsening identity (super-regions = distinctions + 1) or the sub-extensive carried-cost bound depends on this counter. Defined by structural recursion on the list: empty is 0, singleton is 1, and each adjacent pair contributes 1 only when the charges differ.
Claim. For a finite list $\ell$ of charges (with decidable equality), $\mathrm{runs}(\ell)$ is the number of maximal contiguous blocks of equal charge. Explicitly: $\mathrm{runs}([])=0$, $\mathrm{runs}([a])=1$, and $\mathrm{runs}(a::b::t)=\mathbf{1}_{a\neq b}+\mathrm{runs}(b::t)$. A locked domain of any length therefore contributes exactly one.
background
The module formalizes Phase-12 domain coarsening: the scale-adaptive engine treats each locked domain (a maximal run of equal recognition charge, with no internal distinction) as one coarse super-region. The charge field along the ladder is modeled as a List of values with decidable equality; two adjacent sites form a forced distinction exactly when their charges differ.
Within a maximal equal-charge run the internal cost is zero (all members equal), so the run coarsens losslessly into one super-region and is carried in one O(1) step. The companion counter boundaries tallies adjacent unequal pairs (the active interface). The headline relation is that, on every nonempty field, the run count equals the boundary count plus one, independent of how large each constant block is.
Thus the carried representation size tracks distinctions, not volume: two constant blocks of any lengths are two super-regions.
proof idea
Pure structural definition, no proof obligations. Pattern-match on the list: nil maps to 0; a singleton maps to 1; on a :: b :: l add the indicator a ≠ b (1 if distinct, else 0) and recurse on the tail b :: l. The recursion peels one adjacent pair at a time, so each new run is opened exactly when a charge change appears.
why it matters
This is the left-hand side of the module's main identity: for every nonempty field, runs equals boundaries plus one (runs_eq), restated as the carried-cost theorem that super-region count tracks distinctions and is at most the length. Downstream lemmas (runs_nil, runs_singleton, runs_le_length) and the 2D coarsening layer (of, rowCost) all read this counter.
In the Recognition framework it makes exact the slogan "carry each region at the coarsest rung its recognition allows": locked domains of arbitrary size cost one. Composed with the cadence bound (at most one resolution per tick) and open-system growth (bulk blocks grow linearly, the active interface only diffusively), it is the formal core of sub-extensive engine cost in cosmogenesis. Minimality is immediate from the identity: each distinction forces a new block, so runs is the size of the coarsest lossless cover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.