mockState
plain-language theorem explainer
mockState supplies a zero-initialized LState for baseline examples in VM commit tooling. Cycle demonstration authors cite it to run lCycle without custom register setup. The definition is a direct one-line application of the LState.init constructor.
Claim. The baseline augmented VM state is the structure obtained by initializing the legacy LNAL state with zeroed Reg6 and Aux5 registers, then setting window index and J accumulators to zero.
background
LState is the VM state wrapper that augments the legacy LNAL.LState with a monotone window counter (incrementing every eight ticks) and per-window J-budget fields. The init function constructs such an LState from supplied Reg6 and Aux5 values while zeroing the window fields. The surrounding VM.Commit module addresses predicates for conservative COMMIT boundaries under the v2 flag and imports the meta-realization structure from UniversalForcingSelfReference.
proof idea
One-line definition that applies the LState.init constructor to Reg6.zero and Aux5.zero.
why it matters
This definition supplies the concrete state argument required by cycleReport, the smoke-test demonstration that applies lCycle and reports windowIdx, winJ, and commitEvent. It closes a tooling gap in the VM layer while remaining independent of the full self-reference axioms recorded in UniversalForcingSelfReference.for.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.