recognition_work_localizes
plain-language theorem explainer
In a T-tick cadence cycle with at most one resolved edge per tick, total recognition work is at most 2PT and region-activations at most 2T, both independent of the region population. Cosmologists and RS engine auditors cite this as the Phase-11 cost-localization headline: the numerator stays cadence-capped while volume grows. The proof is a one-line pairing of the cycle work and activation bounds.
Claim. For any tick count $T$, resolution schedule $r : \{0,\ldots,T-1\} \to \mathrm{Option}(\iota \times \iota)$, per-region cost ceiling $P$, and cost function $c : \iota \to \mathbb{N}$ with $c(i) \le P$ for all $i$: $\sum_t W(r(t),c) \le 2PT$ and $\sum_t A(r(t)) \le 2T$, where $W$ is the tick recognition work (sum of endpoint costs, or $0$ if unresolved) and $A$ is the tick activation count ($0$ or $2$).
background
The module formalizes Phase-11 of the cosmogenesis engine: open-system dynamics drive a scale-adaptive cell engine over a growing world, and recognition cost per cadence cycle must stay bounded while the world grows. The forced law posts at most one recognition event per tick (T7 eight-tick octave; cosmogenesis cadence $8$). A cycle is modeled as $T$ ticks with resolution map $r$ over an arbitrary region-index type $\iota$.
Tick work $W(e,c)$ is $0$ if the tick resolves nothing and $c(a)+c(b)$ if it resolves edge $(a,b)$ (double-entry posting of both endpoints). Tick activations $A(e)$ are the same with unit cost, hence $0$ or $2$. Upstream, cycle_work_le shows the sum of tick work over the cycle is $\le 2PT$ whenever every region costs at most $P$ to expand; cycle_activations_le specializes to unit cost and gets $\le 2T$ activations. Neither bound mentions $|\iota|$.
proof idea
One-line term proof: the conjunction is exactly the pair of upstream lemmas. The first conjunct is cycle_work_le T res P cost hcost (sum of per-tick work bounds via tickWork_le, then constant-sum simplification to $2PT$). The second is cycle_activations_le T res, itself a specialization of cycle_work_le at $P=1$ and unit cost, rewritten through the definition of tick activations.
why it matters
This is the Phase-11 cost-localization headline for Recognition Science cosmology. When the world grows by a fixed number of regions per cycle (conjugate births), the recognition-cost numerator is capped by cadence $T$ and per-region ceiling $P$ while the volume denominator grows, so the recognition-active fraction falls toward zero and cost localizes to a sub-extensive interface: the engine never expands the locked interior.
It sits with two siblings from the module doc: schedule-independence of the literal engine run, and conjugate-birth charge conservation ($\sigma=0$ through every birth). Together they say the driven engine is literal, conserves $\sigma$ through growth, and pays a per-cycle recognition cost bounded by the cadence regardless of how large reality grows. The cadence link is T7 (eight-tick octave). No downstream Lean dependents are wired yet; the declaration is the public packaging of the two cycle bounds for cosmogenesis scripts and paper citation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.