Flags
The Flags structure supplies a typed collection of boolean switches for vNext behaviors in the Recognition Science codebase. Modules that control certificate emission or optional schedulers reference it to read or override defaults. The definition consists of a direct structure declaration that lists five fields with literal defaults and attaches the Repr and DecidableEq instances.
claimA record type whose fields are five booleans: enable-v2-certificate reporting (default true), macrocore ISA expansion (default false), phi-IR codec packing (default false), consent-derivative gate (default false), and J-greedy scheduler (default false).
background
This structure sits in the configuration module and serves as the single source of truth for optional execution paths. Its doc-comment states the flags are default-safe, with v2 certificates on and all other behaviors off. The module imports Mathlib and depends on mirrors in VM.State plus scattered definitions from Chemistry, Derivations, and NumberTheory; none of those supply the flag values themselves.
proof idea
The declaration is a plain structure definition that enumerates the five fields with their default values and attaches deriving Repr, DecidableEq. No lemmas or tactics are applied.
why it matters in Recognition Science
The structure is read by the default instance in the same module and by VM.State.flags, which supplies the private configuration object used throughout the virtual machine. It therefore gates experimental features while preserving the core recognition-forcing chain (T0-T8) and the Recognition Composition Law. No open questions are attached to this definition.
scope and limits
- Does not enforce any invariants on combinations of the five flags.
- Does not supply runtime validation or error handling for flag values.
- Does not define the semantic effect of each flag on downstream code.
- Does not record version numbers or compatibility constraints.
Lean usage
def customFlags : Flags := { enableV2Certs := false, enableMacrocore := true }formal statement (Lean)
7structure Flags where
8 /-- Enable v2 certificate bundle (report emission). -/
9 enableV2Certs : Bool := true
proof body
Definition body.
10 /-- Enable Macrocore ISA and macro-expansion path. -/
11 enableMacrocore : Bool := false
12 /-- Enable φ‑IR codec and neutral window packer. -/
13 enablePhiIR : Bool := false
14 /-- Enable ConsentDerivative static gate. -/
15 enableConsentGate : Bool := false
16 /-- Enable J‑greedy scheduler (optional). -/
17 enableJScheduler : Bool := false
18deriving Repr, DecidableEq
19
20/-- Global default flags. Projects may override via their own module. -/