tickWork_le
plain-language theorem explainer
A single cadence tick contributes at most twice the per-region expansion ceiling in recognition work: if every region costs at most P forced postings, a resolved edge costs at most 2P and an idle tick costs 0. Cosmologists bounding open-system engine cost cite this as the per-tick step toward cycle-level localization. The proof is a two-case match on the optional edge plus Nat addition of the endpoint ceilings.
Claim. Fix a region index type and a cost map $c$ from regions to naturals. Suppose $c(i)\le P$ for every region $i$. For any optional undirected edge $e$ (either empty or a pair of endpoints), the recognition work of that tick is at most $2P$: idle ticks contribute $0$, and a resolved edge $(a,b)$ contributes $c(a)+c(b)\le 2P$.
background
The module formalizes a Phase-11 cosmogenesis bound: when expanding open-system dynamics drive a scale-adaptive cell engine over a growing world, recognition cost per cadence cycle stays bounded while volume grows, so engine cost localizes to a sub-extensive interface.
The forced cadence law (T7 eight-tick octave) posts at most one recognition event per tick. A cycle is modeled as $T$ ticks with resolution map sending each tick to an optional edge on an arbitrary region type. Recognition work of a tick is defined by matching that option: none costs $0$; some $(a,b)$ costs $c(a)+c(b)$ (double-entry expansion of both endpoints). The fundamental tick is the RS time quantum $\tau_0=1$.
The standing hypothesis is a uniform ceiling $P$ on per-region forced-posting cost. The bound deliberately never mentions the cardinality of the region type, only $P$ and the tick structure.
proof idea
Case-split on the optional edge. If none, simp on the definition of tick work yields $0\le 2P$. If some pair $(a,b)$, unfold to $c(a)+c(b)$, apply Nat.add_le_add to the two endpoint inequalities $c(a)\le P$ and $c(b)\le P$, then rewrite $P+P$ as $2P$ via symmetry of two_mul. No external lemmas beyond basic Nat arithmetic.
why it matters
This is the per-tick atom of the module's main claim that recognition work per cycle is bounded by the cadence, independent of population. Downstream, cycle_work_le sums the inequality over Fin T to obtain total work $\le 2PT$, with $\iota$ absent from the bound. The same lemma specializes (take $P=1$ and constant cost $1$) to tickActivations_le_two: a tick activates at most two regions.
In the framework this is the formal core of "the recognition-active fraction falls toward zero": numerator (work) is capped by cadence $T$ and ceiling $P$ while the world grows by conjugate births. It sits with schedule-independence of the literal engine and sigma-conserving many-births equilibrium. Landmark link: T7 eight-tick octave forces at most one resolved edge per tick, which is what makes the $2P$ ceiling meaningful.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.