jBudgetUpdate
jBudgetUpdate defines the update rule for the J budget accumulator in LState, rolling the winJ snapshot to winJPrev and resetting winJ at each window boundary when base.winIdx8 equals zero. Researchers working on the virtual machine layer of Recognition Science cite this when proving invariants on vNext certificate budgets across eight-tick windows. The definition proceeds by direct case analysis on the boundary condition followed by a record update.
claimLet $s$ be an LState with fields base, windowIdx, winJ, winJPrev. Then $jBudgetUpdate(s)$ yields the updated state where winJPrev equals $s.winJ$ if $s.base.winIdx8=0$ and $s.winJPrev$ otherwise, while winJ equals 0 if at the boundary and $s.winJ+1$ otherwise, with all other fields unchanged.
background
LState is the VM state wrapper that tracks per-window budgeting for vNext certificates. It consists of a base LNAL.LState, a monotone window counter windowIdx that increments every eight ticks, the current window J budget accumulator winJ, and the previous window snapshot winJPrev. This definition lives in the VM.State module, which wraps the legacy LNAL VM to add budgeting for certificates. It depends on the LState structure and indirectly on the cellular automaton step function and phi-ladder hypotheses for the broader framework. The upstream step definition applies a local rule to create successor tapes, providing the locality foundation for state transitions.
proof idea
The definition computes a boundary flag as whether s.base.winIdx8 equals zero. It then selects winJPrev as the current winJ on boundary or the prior snapshot otherwise, sets winJ to zero on boundary or increments it, and returns the updated record. This is a direct structural update with no external lemmas applied beyond the LState constructor.
why it matters in Recognition Science
This definition supplies the budget update logic consumed by lStep, the wrapped small-step that preserves legacy semantics while tracking vNext counters. It implements the rolling accumulator needed for the J-budget in the Recognition Science VM layer, tying into the J-uniqueness (T5) and eight-tick octave (T7) from the forcing chain. It closes part of the scaffolding for certificate tracking in the phi-ladder setting.
scope and limits
- Does not alter the base LNAL state or windowIdx.
- Does not perform any computation on the tape or apply cellular automaton rules.
- Assumes winIdx8 is defined on the base state.
- Does not handle multi-window cycles or lCycle logic.
Lean usage
let s' := jBudgetUpdate sformal statement (Lean)
41def jBudgetUpdate (s : LState) : LState :=
proof body
Definition body.
42 let boundary := s.base.winIdx8 = 0
43 let winJPrev := if boundary then s.winJ else s.winJPrev
44 let winJ := if boundary then 0 else s.winJ + 1
45 { s with winJ := winJ, winJPrev := winJPrev }
46
47/-- Wrapped small-step that preserves legacy semantics while tracking vNext counters. -/