runs_singleton
plain-language theorem explainer
A singleton charge field has exactly one maximal equal-charge run. Formalizers of domain coarsening cite this when reducing the super-region count on unit-length locked domains. The proof is pure definitional reflexivity from the base clause of the run counter.
Claim. For every charge value $a$, the number of maximal equal-charge runs on the singleton list equals one: $\mathrm{runs}([a]) = 1$.
background
In the domain-coarsening model, a charge field along the ladder is a list of values of type $\alpha$ (with decidable equality). A locked domain is a maximal contiguous run of equal charge; the engine carries each such run as one coarse super-region, independent of run length.
The counter $\mathrm{runs}$ returns the number of those maximal runs: empty list gives $0$, a singleton gives $1$, and on $a::b::\ell$ it adds $1$ exactly when $a \neq b$ and recurses. The companion $\mathrm{boundaries}$ counts adjacent unequal pairs (forced distinctions) and is $0$ on empty and singleton lists.
The module headline is that for every nonempty field, $\mathrm{runs} = \mathrm{boundaries} + 1$, so carried cost tracks the interface, not volume. This singleton fact is the unit-length base of that picture.
proof idea
One-line term proof by rfl. The recursive definition of the run counter has the clause that a one-element list contributes exactly $1$, so the equality is definitional and needs no lemmas.
why it matters
This is a @[simp] base case in the Phase-12 domain-coarsening development: the coarsest lossless representation has size equal to forced distinctions plus one. It sits beside the nil case and feeds the inductive skeleton of the headline identity $\mathrm{runs}(a::\ell) = \mathrm{boundaries}(a::\ell) + 1$, and the length bound on runs.
In the Recognition framework that identity is the formal core of sub-extensive engine cost: locked domains of any size cost one super-region (internal cost zero by equal charge), while only distinctions force new blocks. Composed with cadence bounds and open-system growth of constant blocks, carried cost tracks the interface, not the linearly growing world. No downstream dependents are recorded yet; the lemma is infrastructure for those equalities and for simp-driven reductions on unit domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.