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

ConsciousnessState

show as:
view Lean formalization →

ConsciousnessState enumerates five discrete labels that parameterize mode-ratio measurements in EEG protocols. Experimentalists testing voxel-theory predictions would cite the type when defining trial conditions for baseline through sleep states. The declaration is a direct inductive enumeration equipped with decidable equality and representation instances.

claimLet $C$ be the inductive type whose constructors are the five states baseline, flow, analytical, meditation, and sleep.

background

The module Experiments.Protocols supplies testable hypotheses drawn from voxel theory, among them the claim that M2/M4 ratios distinguish consciousness states. ConsciousnessState supplies the discrete labels required by the subsequent protocol and prediction structures. The module document states that every such prediction remains a hypothesis equipped with explicit falsification criteria.

proof idea

The declaration is the inductive definition itself together with the two derived instances DecidableEq and Repr.

why it matters in Recognition Science

It supplies the state domain for both ModeRatioPrediction and ModeRatioProtocol, thereby enabling the core experimental claim that mode ratios classify consciousness states. This step connects the Recognition framework's phi-ladder and coherence predictions to concrete EEG observables. It leaves open the empirical question of whether the predicted ratio bands are observed.

scope and limits

formal statement (Lean)

  95inductive ConsciousnessState
  96  | baseline
  97  | flow
  98  | analytical
  99  | meditation
 100  | sleep
 101  deriving DecidableEq, Repr
 102
 103/-- M2/M4 ratio measurement protocol -/

used by (2)

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