lCycle
plain-language theorem explainer
The eight-tick cycle helper applies the wrapped single-step transition exactly eight times to advance a virtual machine state through one full window. VM tooling and commit modules cite it to simulate periodic budgeting updates. The definition is a direct wrapper around the iterate combinator applied to the single-step function.
Claim. Define the eight-tick cycle operator that maps a program $P$ and initial VM state wrapper $s$ to the state obtained by applying the wrapped transition function eight times: $C(P,s) := iterate(wrapped-step_P, 8, s)$, where the state wrapper tracks window indices and J-budgets.
background
The VM state wrapper is a structure containing a base legacy LNAL state, a monotone window counter incremented every eight ticks, and accumulators for the current and previous window J-budgets. This wrapper supports per-window budgeting for vNext certificates while preserving legacy semantics. The single-step wrapper applies the legacy small-step transition, detects window boundaries via the winIdx8 flag, and updates counters when the v2 certificate flag is active. The iterate combinator from the compatibility layer delegates directly to Nat.iterate. This definition sits in the VM.State module that imports LNAL registers and the virtual machine to connect legacy execution with Recognition Science windowing.
proof idea
The definition is a one-line wrapper that invokes the iterate combinator on the wrapped single-step transition for exactly eight steps.
why it matters
This supplies the periodic eight-tick advancement required by the T7 octave landmark in the forcing chain. It feeds the cycleReport definition in the Commit module, which produces smoke-test output showing window advancement and commit events. The construction aligns with the eight-tick period used for phi-ladder J-cost accounting in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.