runs_nil
plain-language theorem explainer
The empty charge list has zero maximal equal-charge runs, so the domain-coarsening engine carries no super-regions. Base-case infrastructure for anyone counting forced distinctions along a recognition ladder. Proof is definitional reflexivity from the first clause of runs.
Claim. For any charge type $\alpha$, the number of maximal equal-charge runs on the empty list is zero: $\mathrm{runs}([]) = 0$.
background
In DomainCoarsening, a charge field along the ladder is a List α with decidable equality. Adjacent unequal charges are forced distinctions; a maximal run of equal charges is a locked domain that coarsens losslessly to one super-region.
The function runs counts those maximal equal-value runs: the number of coarse super-regions the engine carries. By definition it sends the empty list to 0, a singleton to 1, and otherwise adds 1 at each adjacent inequality while recursing on the tail.
The module headline is that for nonempty fields, runs equals boundaries plus one, so carried cost tracks the interface of distinctions, not volume.
proof idea
One-line definitional proof: rfl matches the first equation of runs, which is runs [] = 0. Marked @[simp] so the empty base case reduces automatically.
why it matters
Closes the empty-list base case of the run counter that underpins Phase-12 domain coarsening: locked domains of any size count once, and the engine cost is sub-extensive in volume. Together with the singleton and inductive clauses it supports the identity that nonempty run count equals forced distinctions plus one, and the optimality claim that runs is the minimum number of constant contiguous blocks in any lossless cover. No direct downstream edges are recorded; the simp attribute makes it available wherever empty fields appear in the coarsening algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.