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

ModeRatioProtocol

show as:
view Lean formalization →

ModeRatioProtocol defines a record that standardizes EEG coherence measurements of M2/M4 ratios across four consciousness states. Physicists running voxel-theory tests would instantiate this structure to collect comparable data on state classification. The definition is a direct record with three defaulted fields and no computation.

claimA record consisting of a list of consciousness states (defaulting to baseline, flow, analytical, meditation), an integer trials-per-state (default 20), and a modality string (default ``EEG_coherence'').

background

The declaration lives in Experiments.Protocols, whose module document states that all entries are hypotheses with explicit falsification criteria derived from the voxel/meaning framework. One listed core prediction is that M2/M4 ratios classify consciousness states, alongside EEG φ-frequency peaks and coherence-transfer healing. ConsciousnessState is the sibling inductive type whose five constructors (baseline, flow, analytical, meditation, sleep) label the states to be measured. Upstream structures such as Measurement supply the pattern for recording numeric values with error bars, while PhiForcingDerived and SpectralEmergence supply the J-cost and emergence background that motivate the ratio observable.

proof idea

The declaration is a plain structure definition whose three fields each carry a default value. No lemmas or tactics are invoked; the body simply lists the field names and their initializers.

why it matters in Recognition Science

The structure encodes the module's second core prediction that M2/M4 ratios distinguish consciousness states. It supplies the concrete parameter record that downstream siblings such as ModeRatioPrediction and ratioInRange are expected to consume. In the Recognition framework it operationalizes the link between phi-ladder dynamics and measurable EEG coherence, while the module document reminds the reader that the claim remains a testable hypothesis rather than a derived theorem.

scope and limits

formal statement (Lean)

 104structure ModeRatioProtocol where
 105  /-- States to measure -/
 106  states : List ConsciousnessState := [.baseline, .flow, .analytical, .meditation]

proof body

Definition body.

 107  /-- Number of trials per state -/
 108  trials_per_state : ℕ := 20
 109  /-- Measurement modality -/
 110  modality : String := "EEG_coherence"
 111
 112/-- Predictions for mode ratios by state -/

depends on (10)

Lean names referenced from this declaration's body.