flags
The declaration defines a private constant flags in VM.State as the default instance of Config.Flags. VM implementers and certificate report generators cite it to obtain the baseline vNext settings without per-module duplication. The definition is a direct one-line assignment to Config.default.
claimLet $flags : Flags$ denote the default configuration record in which $enableV2Certs = true$, $enableMacrocore = false$, and all remaining Boolean fields take the documented safe defaults.
background
The VM.State module supplies a thin wrapper around ledger and register state for the LNAL virtual machine. Its sibling definitions include LState, init, and lCycle, all of which may consult feature flags to decide whether v2 certificate bundles or macrocore expansion are active. The Flags structure itself is a record whose fields are Boolean switches with explicit defaults: certificates on, macrocore off, and phi-IR codec controlled by a third switch.
proof idea
One-line definition that directly returns the value of Config.default.
why it matters in Recognition Science
This supplies the concrete default used by enableV2Certs and by units_kgate_report_json in the URCAdapters layer. It therefore anchors certificate emission behavior for downstream cellular-automata gadgets and complexity models. In the broader Recognition framework it instantiates the default point in the modal possibility configuration space, ensuring that T5 J-uniqueness and T7 eight-tick bookkeeping remain available unless explicitly disabled.
scope and limits
- Does not prove any theorem or discharge any hypothesis.
- Does not override project-specific flag values supplied at build time.
- Does not expose the flags record outside the VM.State module.
- Does not depend on runtime ledger state or J-cost calculations.
Lean usage
def enableV2Certs : Bool := flags.enableV2Certsformal statement (Lean)
11private def flags : Config.Flags := Config.default
proof body
Definition body.
12
13/-- Feature flag mirror for the VM module. -/