init
plain-language theorem explainer
The definition constructs the initial augmented VM state by wrapping the legacy LNAL initializer and zeroing the three window-budget fields. Researchers building voxel simulations or SAT completeness arguments cite it as the canonical starting point for state evolution under per-window J accounting. Construction is a direct record literal that invokes the base initializer and assigns zero to window index, current J accumulator, and previous J snapshot.
Claim. Let the initial augmented VM state be the record whose base component equals the legacy LNAL initialization on registers $r_6$ and $a_5$, while the window index, current-window J-budget, and previous-window J-budget are each set to zero.
background
LState augments the legacy LNAL VM state with per-window budgeting fields required for vNext certificate tracking. Its structure contains the base legacy state, a monotone window counter that advances every eight ticks, the running J-budget accumulator for the current window, and the snapshot of the prior window's budget. The VM.State module supplies this wrapper so that LNAL execution can be instrumented with Recognition Science windowing rules.
proof idea
The definition is a direct record construction. It first binds the base field to the result of the legacy LNAL initializer applied to the two input registers, then populates the three window fields with the constant zero.
why it matters
This entry point is invoked by voxelStep to launch single-voxel LNAL execution and supplies the initial state for AllReachable, IsolationInvariant, and related SAT completeness lemmas. It anchors the eight-tick window mechanism that aligns with the octave period in the forcing chain and supplies the zero-budget starting condition used throughout the VM semantics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.