tickWork
plain-language theorem explainer
Atomic recognition work of one tick under a per-region forced-posting cost: idle ticks cost zero; a resolved edge charges the sum of its two endpoint costs. Cosmologists bounding engine cost per cadence cycle use this as the per-tick summand. Defined by a two-branch match on the optional edge, encoding the forced law that at most one edge resolves per tick.
Claim. Given an optional edge $e$ on region indices and a per-region cost $c$, the recognition work of one tick is $0$ if $e$ is empty, and $c(a)+c(b)$ if $e=(a,b)$.
background
The module formalizes a Phase-11 cosmogenesis bound: 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. 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$. The forced cadence law (T7, eight-tick octave) posts at most one recognition event per tick.
Each resolved edge is a double-entry posting that activates its two endpoints. The per-region map $c:\iota\to\mathbb{N}$ is the forced-posting expansion cost of a region. Upstream cost notions in the foundation (J-cost of a recognition event, multiplicative-recognizer derived cost, rung-coarsened event sums) motivate treating endpoint expansion as additive work; here that idea is specialized to a discrete natural-number cost on region indices.
The fundamental RS time quantum is one tick ($\tau_0=1$). The present definition is the per-tick work atom from which cycle sums and activation counts are built.
proof idea
Pure definition by pattern match on the optional edge: the none branch returns $0$; the some(a,b) branch returns $c(a)+c(b)$. No lemmas are invoked.
why it matters
This is the atomic summand for the module's main bound. The per-tick inequality (work at most $2P$ when every region costs at most $P$) cases on this definition; summing it yields the cycle bound that total recognition work over $T$ ticks is at most $2PT$, with no dependence on the population type $\iota$. The Phase-11 headline packages that with the twin activation bound (at most $2T$ region-activations) to conclude that the recognition-active fraction falls as the world grows by a fixed number of regions per cycle.
Activation count is literally this definition at unit cost. Together with schedule-independence of the scale-adaptive engine and conjugate-birth charge conservation, the bound supports the claim that the driven engine stays literal, conserves $\sigma$ through growth, and pays a cadence-capped recognition cost independent of how large reality becomes. Framework landmark: T7 eight-tick octave as the forced cadence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.