commitEvent
plain-language theorem explainer
commitEvent defines the boolean predicate that returns true exactly when the v2 certificate flag is set and the current window J accumulator does not exceed the prior window value. Cycle evaluators and VM smoke tests cite this predicate to mark conservative commit boundaries. The definition is a direct conjunction of the enable flag and the monotonicity test on LState fields.
Claim. The predicate commitEvent($s$) holds if and only if enableV2Certs is true and the J-budget accumulator of the current window satisfies $s.winJ ≤ s.winJPrev$.
background
LState is the VM state wrapper that tracks per-window budgeting for vNext certificates; it contains a base LNAL state, a monotone window counter that increments every eight ticks, and J-budget accumulators for the current and previous windows. enableV2Certs is the feature flag mirror for the VM module. The definition sits inside the Commit submodule of the LNAL virtual machine and draws on the meta-realization structure from UniversalForcingSelfReference.
proof idea
The definition is a direct conjunction that evaluates enableV2Certs together with the inequality between the current and previous window J values stored in the LState record.
why it matters
This predicate supplies the conservative COMMIT boundary check used by cycleReport to produce smoke-test output for tooling. It closes the v2 certificate path inside the LNAL VM layer that aligns with the eight-tick windowing and J-uniqueness properties of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.