mockState
plain-language theorem explainer
mockState supplies a baseline augmented VM state with all registers and window counters zeroed for smoke-test examples. VM tooling authors cite it when initializing cycle demonstrations under the v2 COMMIT boundary. The definition is a direct one-line application of the LState.init constructor to zero arguments.
Claim. Let $LState$ be the structure consisting of a legacy base state together with window index and $J$-budget accumulators. Define $mockState := init(Reg6.zero, Aux5.zero)$, where $init$ constructs the augmented state by setting the base to the legacy initialization and zeroing the window fields.
background
The VM.Commit module concerns predicates for conservative COMMIT boundaries under the v2 flag. LState wraps the legacy LNAL.LState and augments it with a monotone window counter (incremented every eight ticks), a current-window $J$ accumulator, and its predecessor. The init function from VM.State constructs this wrapper by calling LNAL.LState.init on the supplied Reg6 and Aux5 values and then zeroing the window fields. The upstream 'for' structure from UniversalForcingSelfReference records the structural properties required for meta-realization certificates that guarantee orbit and step coherence.
proof idea
This is a one-line definition that applies the LState.init constructor to Reg6.zero and Aux5.zero.
why it matters
mockState supplies the initial state consumed by cycleReport, which performs a smoke-test cycle demonstration and reports the resulting window index, winJ value, and commit event. It therefore anchors tooling verification of conservative COMMIT boundaries. In the Recognition framework the construction sits inside the eight-tick octave (T7) and the window budgeting that supports vNext certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.