cycle_activations_le
plain-language theorem explainer
Over a T-tick cycle with at most one resolved edge per tick, total region-activations sum to at most 2T, independent of the region population. Anyone citing Phase-11 cost localization or the sub-extensive recognition interface needs this count bound. The proof is a one-line specialization of the per-cycle work bound at unit cost.
Claim. For any $T \in \mathbb{N}$ and any assignment of at most one optional edge per tick on an arbitrary region index set, $\sum_{t < T} a_t \le 2T$, where $a_t$ is the number of region-activations on tick $t$ ($0$ if unresolved, $2$ if an edge is resolved).
background
The module formalizes Phase-11 cost localization for the scale-adaptive cell engine on a growing world. A cycle is modeled as $T$ ticks with at most one forced resolution per tick: a map from Fin T into optional edges on an arbitrary region-index type. The forced law posts at most one recognition event per tick (the eight-tick cadence of T7).
Each resolved edge activates its two endpoints (double-entry posting), so a tick contributes either $0$ or $2$ region-activations. That count is the unit-cost case of tick work: activations equal work when every region costs $1$ to expand. The parent inequality already bounds total recognition work by $2PT$ whenever every region costs at most $P$; the population size never enters.
Upstream, cycle_work_le states that over a $T$-tick cycle with per-region expansion cost at most $P$, total recognition work is at most $2PT$, independent of the index type.
proof idea
One-line specialization of cycle_work_le. Instantiate that theorem at $P = 1$ with the constant cost function $i \mapsto 1$ (the pointwise bound is reflexivity). The resulting sum of tick works is at most $2T$. Unfold the definition that activations are exactly tick work at unit cost, and the claim follows by simplification.
why it matters
This is the activation half of the Phase-11 cost-localization headline. Downstream, recognition_work_localizes packages it with the work bound: work $\le 2PT$ and activations $\le 2T$, both independent of population size. When the world grows by a fixed number of regions per cycle, the recognition-cost numerator stays capped while volume grows, so the recognition-active fraction falls toward zero and cost localizes to a sub-extensive interface.
The module pairs this with schedule-independence of the engine and conjugate-birth charge conservation: the driven engine stays literal, conserves $\sigma$ through growth, and pays a per-cycle recognition cost bounded only by the cadence. The eight-tick octave (T7) supplies the natural cadence scale; the bound itself holds for any $T$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.