cycleReport
plain-language theorem explainer
cycleReport produces a diagnostic string displaying the window index, winJ value, and commit status obtained from the cycle length function on the mock program and baseline state. Tooling and verification code would cite this definition to confirm the integration of the commit boundary predicate with cycle evaluation. The definition is a direct construction that binds the cycle result and formats it with string interpolation including the commit check.
Claim. Define the cycle report as the string ``cycle windowIdx=final.window index, winJ=final.winJ, commit=commit boundary predicate on final'' where final is the augmented state returned by the cycle length function applied to the mock program and the initial mock state.
background
The VM.Commit module defines a predicate for a conservative COMMIT boundary under the v2 flag, which returns true precisely when v2 certificates are enabled and the winJ value does not increase. The mock program is defined as a constant function that returns the BALANCE opcode for any input. The mock state initializes the registers and auxiliary data to zero values. The cycle length function, imported from VM.State, computes the final state after one full cycle of the program.
proof idea
This is a direct definition. It applies the cycle length function to the mock program and mock state to obtain the final augmented state. It then constructs the report string by interpolating the window index, winJ, and the result of the commit event predicate on that state.
why it matters
This definition serves as a smoke-test demonstration within the VM layer of the Recognition Science framework. It verifies the conservative commit boundary predicate under the v2 flag, consistent with the commit operation that models wavefunction collapse in the quantum measurement module. With no downstream theorems depending on it, the definition supports practical tooling checks for the cycle machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.