tickActivations
plain-language theorem explainer
Counts how many region-activations one cadence tick contributes: zero if the tick resolves nothing, two if it resolves an edge (both endpoints). Cosmology and cost-localization arguments cite it as the unit-cost specialization of per-tick recognition work. The definition is a one-line wrapper applying the general tick-work functional at constant cost one.
Claim. For a resolved-edge option $e \in \mathrm{Option}(\iota \times \iota)$, the number of region-activations contributed by that tick is $0$ if $e = \mathrm{none}$, and $2$ if $e = \mathrm{some}(a,b)$ (the two endpoints). Equivalently, it is the recognition work of $e$ under the constant unit cost function $i \mapsto 1$.
background
The module formalizes Phase-11 cost localization: under open-system expanding dynamics, recognition cost per cadence cycle stays bounded while the world grows, so engine cost localizes to a sub-extensive interface. The forced law (T7 eight-tick octave) posts at most one recognition event per tick. A cycle is modeled as $T$ ticks with resolution map $\mathrm{res} : \mathrm{Fin}, T \to \mathrm{Option}(\iota \times \iota)$ over an arbitrary region index type $\iota$.
Per-tick recognition work is defined by matching on the optional edge: nothing costs $0$; an edge $(a,b)$ costs $\mathrm{cost}(a)+\mathrm{cost}(b)$. The present definition specializes that functional to unit cost, so it literally counts activated endpoints rather than weighted postings. Upstream, the RS tick is the fundamental time quantum $\tau_0 = 1$, and active edges per tick are normalized to $A = 1$.
proof idea
Pure definitional wrapper: apply the general per-tick work functional to the constant cost function sending every region to $1$. No tactics or lemmas; the match on $\mathrm{none}$ versus $\mathrm{some}(a,b)$ is inherited, yielding $0$ or $1+1=2$.
why it matters
This is the activation counter used by the Phase-11 localization chain. Downstream, tickActivations_le_two shows a single tick contributes at most two activations; cycle_activations_le lifts that to a $T$-tick cycle bound of $2T$, independent of population size; and recognition_work_localizes packages both the work bound $2PT$ and the activation bound $2T$ as the cost-localization headline.
In framework terms it sits under T7 (eight-tick cadence, at most one forced resolution per tick) and supports the claim that recognition-active fraction falls toward zero as volume grows by conjugate births: the numerator is capped by cadence alone while the denominator grows. Together with schedule-independence and charge conservation through births, it closes the "engine never expands the locked interior" story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.