boundaries_singleton
plain-language theorem explainer
A singleton charge field has zero forced distinctions: the boundary count on a one-element list is definitionally zero. Cosmology and coarsening arguments cite this as the base case when a locked domain is a single cell. The proof is pure reflexivity against the second clause of the recursive boundary definition.
Claim. For any charge value $a$, the number of forced distinctions in the one-element field $[a]$ is zero: $\mathrm{boundaries}([a]) = 0$.
background
In the DomainCoarsening module, a charge field along the recognition ladder is a list of values of type $\alpha$ (with decidable equality). Two adjacent positions form a forced distinction exactly when their charges differ. The function boundaries counts those adjacent unequal pairs: empty and singleton lists contribute zero; on $a::b::\ell$ one adds $1$ if $a\neq b$ and recurses on $b::\ell$.
A maximal equal-charge run is a locked domain with no internal distinction, so it coarsens losslessly to one super-region. The module's headline is that the number of such runs equals the boundary count plus one on every nonempty field, so carried engine cost tracks the interface, not the volume.
This lemma is the singleton base of that recursion: a one-cell field has no adjacent pair at all.
proof idea
One-line reflexivity. The definition of boundaries has an explicit clause | [_] => 0, so boundaries [a] reduces definitionally to $0$ and rfl closes the goal. Marked @[simp] so downstream rewrites discharge the singleton case automatically.
why it matters
Phase-12 domain coarsening (the formal core behind the cosmogenesis domain-coarsen engine) needs clean base cases for the boundary recursion before proving runs (a :: l) = boundaries (a :: l) + 1 and the sub-extensive cost claim. Without the singleton identity, simp and induction on list structure stall at length-one locked domains.
In the broader Recognition picture this supports "carry each region at the coarsest phi-rung its recognition allows": a single equal-charge cell is already one super-region with zero internal distinctions, matching T-1 rung coarsening (internal cost zero when members are equal) and feeding the interface-tracking story composed with the cadence bound. No downstream theorems are recorded as direct users yet; siblings runs_singleton and runs_eq are the natural consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.