mockState
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not execute any VM instructions or opcode transitions.
- Does not compute J-cost, defect distances, or forcing-chain steps.
- Does not depend on specific values of phi or the alpha band.
- Does not witness any theorem; it is only an example initializer.
Lean usage
let final := lCycle mockProgram mockStateformal statement (Lean)
19@[simp] def mockState : LState := LState.init Reg6.zero Aux5.zero
proof body
Definition body.
20
21/-- Smoke-test cycle demonstration for tooling. -/