cycleReport
plain-language theorem explainer
cycleReport builds a formatted string by running lCycle on the mock program and mock state then appending the commitEvent boolean. Tooling and VM layer developers reference it for quick verification of cycle output formatting. The body is a direct let-binding plus string interpolation with no lemmas applied.
Claim. Let $s$ be the state obtained by applying the cycle operator to the constant mock program (always returning the BALANCE opcode) and the zero-initialized mock state. The report is the string ``cycle windowIdx=$s$.windowIdx, winJ=$s$.winJ, commit=$b$'' where $b$ is the boolean predicate that holds precisely when v2 certificates are enabled and the current window index is at most the previous one.
background
In the VM.Commit module the commitEvent predicate is defined as enableV2Certs && s.winJ ≤ s.winJPrev and serves as the formal witness for a conservative COMMIT boundary under the v2 flag. The two mocks supply concrete inputs: mockProgram is the constant LProgram returning {op := Opcode.BALANCE} and mockState is LState.init with all registers zero. lCycle, imported from VM.State, performs one full cycle evaluation of a program on an augmented state. The module itself is placed inside the larger Recognition Science VM layer that models ledger operations and wavefunction-style commit steps.
proof idea
One-line wrapper that applies lCycle to the two mock constants, binds the resulting LState, then interpolates its window fields together with the boolean returned by commitEvent.
why it matters
The definition supplies a runnable smoke-test inside the VM.Commit module; it is not referenced by any downstream theorem. It exercises the v2 COMMIT boundary predicate and the cycle operator but does not touch the forcing chain, J-uniqueness, or the phi-ladder. No open question is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.