cycle_work_le
plain-language theorem explainer
Over a T-tick cadence cycle with at most one resolved edge per tick and per-region expansion cost at most P, total recognition work is at most 2PT, with no dependence on the region population. Cosmologists citing Phase-11 cost localization use this to show the engine cost stays cadence-bounded while the world grows. The proof sums the per-tick bound and collapses the constant sum to 2PT.
Claim. Let $T\in\mathbb{N}$ and let $\mathrm{res}:\{0,\ldots,T-1\}\to\mathrm{Option}(\iota\times\iota)$ record at most one resolved edge per tick. If every region $i$ has expansion cost $\mathrm{cost}(i)\le P$, then $\sum_{t}\mathrm{tickWork}(\mathrm{res}(t),\mathrm{cost})\le 2PT$. The bound depends only on the cadence $T$ and the per-region ceiling $P$, not on the size of the index type $\iota$.
background
This module formalizes the Phase-11 claim behind the driven cosmogenesis engine: when open-system dynamics run a scale-adaptive cell engine over a growing world, recognition cost per cadence cycle stays bounded while volume grows, so cost localizes to a sub-extensive interface.
The forced cadence law (T7 eight-tick octave; cosmogenesis cadence 8) posts at most one recognition event per tick. A cycle is modeled as $T$ ticks with resolution map $\mathrm{res}$ over an arbitrary region index type $\iota$. Each resolved edge activates both endpoints (double-entry posting). The single-tick work is zero on an unresolved tick and $\mathrm{cost}(a)+\mathrm{cost}(b)$ on a resolved edge $(a,b)$.
The upstream lemma states that any single tick costs at most $2P$ whenever every endpoint costs at most $P$. The present result lifts that tick bound to a full cycle by summing over $\mathrm{Fin},T$.
proof idea
Apply the per-tick bound pointwise: for each $t$, $\mathrm{tickWork}(\mathrm{res},t,\mathrm{cost})\le 2P$ by the upstream tick lemma under the uniform ceiling hypothesis. Summing over $\mathrm{Fin},T$ via $\mathrm{Finset.sum_le_sum}$ yields a sum bounded by $\sum_{t} 2P$. The constant sum equals $2P\cdot T$ by $\mathrm{Finset.sum_const}$, cardinality of $\mathrm{Fin},T$, and rearranging the scalar multiplication. Transitivity of $\le$ finishes the proof.
why it matters
This is the work half of the Phase-11 cost-localization headline. Downstream, the unit-cost specialization gives at most $2T$ region-activations per cycle, and the conjunction theorem packages both bounds: work $\le 2PT$ and activations $\le 2T$, both independent of population size. With a world that grows by a fixed number of regions per cycle (conjugate births), the recognition numerator is capped while volume grows, so the recognition-active fraction falls toward zero and the engine never expands the locked interior.
Together with schedule-independence of the engine run and charge conservation through many births ($\sigma=0$), this completes the triad: the driven engine is literal, conserves $\sigma$ through growth, and pays a per-cycle recognition cost bounded only by the cadence. The bound is the formal core of sub-extensive localization under T7 cadence forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.