LState
LState augments the legacy LNAL VM state with a window index and J-budget accumulators to support per-window budgeting checks in vNext certificates. Researchers implementing LNAL simulation semantics or URC certificate generators reference this structure for state transitions and invariant preservation. The declaration is a structure definition that bundles four fields with no proof obligations.
claimThe augmented VM state is a structure consisting of a base legacy LNAL state, a natural number window index that increments every eight ticks, a current window J-budget accumulator, and a previous window J-budget snapshot.
background
In the VM.State module the LState structure wraps LNAL.LState to track budgeting across eight-tick windows. The windowIdx field counts these periods while winJ and winJPrev accumulate and snapshot the J-cost, where J denotes the uniqueness function from the forcing chain. This setup supports the Recognition Composition Law by maintaining monotone budgets for certificate verification. The upstream from theorem in PrimitiveDistinction supplies the seven axioms that reduce to four structural conditions plus three definitional facts, which this state representation satisfies.
proof idea
This is a structure definition introducing four fields: base LNAL state, window index, current and previous J budgets. No lemmas are applied as it is a definitional wrapper.
why it matters in Recognition Science
This structure underpins the voxelStep definition in LNALSemantics and feeds into certificates such as CostCeilingCert, LNALInvariantsCert, ScheduleNeutralityCert and SU3MaskCert by providing the state for J-budget checks. It directly supports the per-window budgeting required for vNext certificates, closing the loop on the eight-tick octave (T7) and J-uniqueness (T5) in the forcing chain. It enables conservative COMMIT boundaries in commitEvent under the v2 flag.
scope and limits
- Does not define the transition rules for lStep or lCycle.
- Does not enforce any invariants on the J budgets.
- Does not specify the initialization logic beyond the structure fields.
- Does not connect to spatial dimensions or mass formulas.
formal statement (Lean)
17structure LState where
18 /-- Base LNAL VM state (legacy semantics). -/
19 base : LNAL.LState
20 /-- Monotone window counter (increments every eight ticks). -/
21 windowIdx : Nat
22 /-- Current window J budget accumulator. -/
23 winJ : Nat
24 /-- Previous window J budget snapshot. -/
25 winJPrev : Nat
26deriving Repr
27
28namespace LState
29
30/-- Initialize the augmented VM state from legacy registers. -/