manyBirths_chargeSum
plain-language theorem explainer
Any finite batch of conjugate births (+u at the fine frontier, -u at the coarse frontier) leaves the total level sum unchanged. Cosmology proofs that track sigma through driven ladder expansion cite this to keep sigma = 0 after k cadence cycles. The argument is a short list-sum algebra: append and replicate cancel by ring.
Claim. For every $k \in \mathbb{N}$, $u \in \mathbb{R}$, and finite list $xs$ of reals, $\mathrm{sum}(\underbrace{u,\ldots,u}_{k} \mathbin{++} xs \mathbin{++} \underbrace{-u,\ldots,-u}_{k}) = \mathrm{sum}(xs)$.
background
The module formalizes Phase-7 forward dynamics on a field of recognition levels: each tick resolves a coupled pair by sending both endpoints to their mean (the sigma = 0, J-minimal move). Closed-system facts already show that a single resolution conserves the level sum and strictly lowers variance, so the dynamics descends to consensus (vanishing total J-cost on edges).
The driven open-system extension grows the ladder each cadence cycle by a conjugate birth: a charge $+u$ at the fine frontier and $-u$ at the coarse frontier. The sibling fact for one birth, and this fact for $k$ births, ensure the charge sum is still the initial total. Together with resolution conservation, sigma = 0 therefore survives the whole driven run; births inject structure without breaking the conserved charge that closed descent relies on.
Levels live as real lists; sum is ordinary list summation. Replication builds the $k$ frontier charges. No new cost or coupling axioms enter here: only list algebra over $\mathbb{R}$.
proof idea
Tactic proof in two steps. First simp rewrites with List.sum_append, List.sum_replicate, and nsmul_eq_mul, turning the concatenated sum into $k \cdot u + \mathrm{sum}(xs) + k \cdot (-u)$. Then ring cancels the opposite multiples and leaves $\mathrm{sum}(xs)$. No induction and no cosmology-specific lemmas: pure list and ring arithmetic.
why it matters
Module doc pairs this with conjugateBirth_chargeSum as the open-input half of sigma conservation: resolutions conserve charge by pairResolve_levelSum; births conserve it by these two theorems. That split is what lets the driven expanding dynamics keep non-homogenizing structure alive while still sitting on the same conserved-sigma ground that closed descent relaxes toward consensus.
In the broader Recognition picture this is bookkeeping for the forced open drive on the phi-ladder (cadence births at the horizons), not a new forcing step. It does not itself force $D = 3$, the eight-tick octave, or J-uniqueness; it only guarantees that whatever those landmarks fix about the ladder, multi-cycle conjugate injection does not spoil the global charge that the J-cost Lyapunov story needs. With zero sorry it closes the multi-birth case of the expanding-dynamics charge ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.