boundaries
plain-language theorem explainer
Counts forced distinctions along a charge field: the number of adjacent pairs with unequal charges. Empty and singleton lists contribute zero; each unequal neighbor pair adds one. Cosmology and domain-coarsening arguments cite it as the active interface size. The body is a plain structural recursion on lists with decidable equality.
Claim. For a list $\ell$ of charges (with decidable equality), $\mathrm{boundaries}(\ell)$ is the number of adjacent unequal pairs. Formally: $\mathrm{boundaries}([])=0$, $\mathrm{boundaries}([a])=0$, and $\mathrm{boundaries}(a::b::\ell)=\mathbf{1}_{a\neq b}+\mathrm{boundaries}(b::\ell)$. Within a maximal equal-charge run there is no distinction.
background
The DomainCoarsening module formalizes Phase-12 cosmogenesis: a scale-adaptive engine carries each locked domain (a maximal run of equal recognition charge) as one coarse super-region. Charge fields are modeled as lists with decidable equality; two adjacent sites form a forced distinction exactly when their charges differ.
The companion count runs tallies maximal equal-value runs (the super-regions the engine carries). This definition tallies the complementary quantity: adjacent unequal pairs, i.e. the recognition-active interface. Module headline: for every nonempty field, the number of runs equals the number of boundaries plus one, so carried cost tracks distinctions, not volume.
Locked domains of any length contribute zero internal distinctions and coarsen losslessly (internal cost zero under rung coarsening; idle fast-forward in one step).
proof idea
Definition by structural recursion on the list, not a proved theorem. Base cases: empty and singleton return 0 (no adjacent pair). Inductive step on $a::b::\ell$: add 1 if $a\neq b$, else 0, then recurse on $b::\ell$. Decidable equality on the charge type supplies the branch. No lemmas are invoked; the recursion is the content.
why it matters
This is the interface half of the module identity that the coarsest lossless representation has size equal to forced distinctions plus one. Downstream, runs_eq proves runs equal boundaries plus one on every nonempty field; carried_cost_tracks_distinctions packages that with the length bound so engine cost is sub-extensive when distinctions grow only diffusively while volume grows linearly.
Simp lemmas boundaries_nil and boundaries_singleton discharge the base cases. The 2D coarsening layer reuses the same interface count on rows. In the broader RS picture this makes precise "carry each region at the coarsest phi-rung its recognition allows": cost is set by the active interface, not by domain volume, and composes with the cadence bound (at most one resolution per tick) toward sub-extensive cosmogenesis cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.