boundaries_nil

In the domain-coarsening model, a charge field along the ladder is a list of values of type $\alpha$ (with decidable equality). Two adjacent entries form a forced distinction exactly when their charges differ; a maximal equal-charge run is a locked domain with no internal distinction and coarsens losslessly to one super-region.

The function that counts those distinctions is defined by recursion on the list: the empty list and any singleton contribute $0$, and a cons cell $a::b::\ell$ adds $1$ if $a\neq b$ (else $0$) and continues on $b::\ell$. The companion count of maximal equal-charge runs is the number of coarse super-regions the scale-adaptive engine actually carries.

The module's headline identity is that, on every nonempty field, the run count equals the distinction count plus one. That makes carried cost track the interface, not the volume.

One-line definitional proof: unfold the empty-list clause of the recursive distinction count and close by reflexivity. Marked @[simp] so the base case fires automatically in later rewrites.

This is the empty-list base case for the distinction count that underpins Phase-12 domain coarsening. Together with the singleton base case and the recursive step, it supplies the simp infrastructure for the headline identity that the number of coarse super-regions equals the number of forced distinctions plus one on every nonempty field.

That identity is the formal core of sub-extensive engine cost: a field of length $N$ made of two constant blocks is carried as two super-regions no matter how large $N$ is. Composed with the cadence bound (at most one resolution per tick) and open-system growth of bulk versus interface, it is why carried cost tracks distinctions rather than volume. The empty case is trivial but mandatory for the inductive and simp closure of those arguments.