enableV2Certs
plain-language theorem explainer
The declaration supplies a Boolean flag that gates v2 certificate bundle emission inside VM state transitions. CommitEvent and lStep cite the flag to decide whether to enforce certificate boundaries or update window counters. The definition is realized as a direct alias to the enableV2Certs field of the default configuration record.
Claim. $enableV2Certs : Bool$ is the flag value taken from the default configuration record, i.e. $enableV2Certs := flags.enableV2Certs$ where $flags$ is the default $Config.Flags$ structure with $enableV2Certs$ preset to true.
background
The VM.State module wraps LNAL virtual-machine execution to maintain per-window J-budget counters and eight-tick window indices for vNext certificates. The sibling flags definition supplies the default-safe configuration record imported from Config, exposing the three Boolean toggles that control certificate reporting, macrocore expansion, and phi-IR packing. Upstream, UniversalForcingSelfReference.for records the structural properties required of any meta-realization instance, while PhiLadderLattice.that supplies the hypothesis structure for phi-ladder Poisson summation that downstream analytic results may assume.
proof idea
The definition is a one-line alias that directly references the enableV2Certs field of the default flags structure.
why it matters
commitEvent uses the flag to witness conservative COMMIT boundaries, and lStep uses it to wrap legacy small-step semantics while conditionally advancing window counters. The declaration realizes the vNext feature-flag interface defined in Config.Flags, allowing the VM layer to track J-cost budgeting across the eight-tick octave without altering core LNAL behavior. It supplies the concrete toggle that later theorems can condition upon when the analytic infrastructure for phi-ladder sums becomes available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.