winJZero
plain-language theorem explainer
winJZero returns true precisely when the current window J-budget accumulator of an LState equals zero. VM implementers and vNext certificate verifiers cite the predicate to detect exhaustion of the per-window allocation. The definition is a direct field projection and equality test on the winJ component of the supplied state structure.
Claim. Let $s$ be an element of the VM state space LState. Then winJZero$(s)$ holds if and only if the current-window J-budget accumulator of $s$ equals zero.
background
LState is the VM state wrapper that augments the base LNAL virtual-machine state with windowed budgeting fields. It records a monotone window index that increments every eight ticks, the running J accumulator winJ for the current window, and the snapshot winJPrev of the preceding window. This structure supplies the per-window J accounting required for vNext certificates.
proof idea
The definition is a one-line field projection that extracts the winJ component of the input LState and tests equality with zero.
why it matters
The predicate supplies the depletion test inside the windowed J-budgeting layer that aligns with the eight-tick octave. It is referenced by sibling transition functions such as jBudgetUpdate and lStep to enforce budget boundaries. In the Recognition framework it closes the interface between the LNAL base semantics and the certificate budgeting mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.