lStep
plain-language theorem explainer
The lStep definition wraps the core LNAL stepper to advance a wrapped VM state while incrementing a monotone window counter on every eight-tick boundary and conditionally refreshing the J-budget accumulator. Fluid-simulation and certificate authors cite it when they need legacy LNAL evolution plus per-window cost tracking. The body performs a direct boundary test on the base winIdx8 field, updates the window index, then branches on the enableV2Certs flag to either call jBudgetUpdate or copy the prior J values.
Claim. Let $LState$ be the structure $(base : LNAL.LState, windowIdx : Nat, winJ : Nat, winJPrev : Nat)$. For program $P$ and state $s$, $lStep(P,s)$ returns the state whose base is obtained by one LNAL step on $s.base$, whose window index is incremented precisely when the new base satisfies $winIdx8=0$, and whose J-budget fields are either refreshed by the budget-update rule or left unchanged according to the v2-certificate flag.
background
LState augments the legacy LNAL.LState with a monotone window counter (incremented every eight ticks) and two J-budget accumulators that record the current and previous window's J-cost. The module sits inside the VM layer that bridges LNAL registers to classical fluid semantics. Upstream, tick supplies the fundamental RS time quantum with the explicit remark that one octave equals eight ticks; the PrimitiveDistinction.from theorem supplies the seven-axiom foundation that justifies treating the base stepper as a primitive distinction operation.
proof idea
The definition is a direct construction: apply LNAL.lStep to the base field, test the resulting winIdx8 for boundary, compute the new window index by conditional increment, then branch on enableV2Certs to invoke jBudgetUpdate or to copy the existing winJ and winJPrev fields verbatim.
why it matters
lStep supplies the single-step primitive used by voxelStep in LNALSemantics and by the fold lemmas in Simulation2D; those in turn feed the CostCeilingCert, LNALInvariantsCert and ScheduleNeutralityCert structures. It therefore closes the eight-tick octave (T7) inside the VM while preserving the legacy LNAL semantics required by the Recognition Composition Law. No open scaffolding remains; the definition is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.