pith. machine review for the scientific record. sign in
def definition def or abbrev high

default

show as:
view Lean formalization →

The baseline vNext feature flag configuration enables the certificate bundle by default and leaves optional paths disabled. Modules throughout the monolith cite this definition to establish standard behavior before project overrides. The definition is a direct record instantiation using the structure's built-in defaults.

claimThe default flag configuration enables the v2 certificate bundle while disabling the macrocore ISA, the phi-IR codec, and the consent gate.

background

The Flags structure defines vNext feature flags that are default-safe, with certificates enabled by default and behavior changes off. Its fields include enableV2Certs for the v2 certificate bundle report emission, enableMacrocore for the Macrocore ISA and macro-expansion path, enablePhiIR for the phi-IR codec and neutral window packer, and enableConsentGate for the ConsentDerivative static gate. This module sets the local theoretical setting for safe defaults in the recognition science configuration layer. Upstream results include default block offsets from the PeriodicTable and configuration structures from Gravity.ILG and Modal.Possibility.

proof idea

The definition is a one-line wrapper that instantiates the Flags structure with its default field values.

why it matters in Recognition Science

This default anchors the configuration used by twenty downstream results, including the phi cubed in theta band theorem in Applied.PhotobiomodulationDevice and the EmpiricalAnchors in Constants.ExternalAnchors. It fills the role of providing the standard safe configuration in the vNext feature flags system, ensuring consistent behavior across the framework unless overridden.

scope and limits

formal statement (Lean)

  21def default : Flags := {}

proof body

Definition body.

  22
  23end Config
  24end IndisputableMonolith

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.