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

modeRatioPredictions

show as:
view Lean formalization →

modeRatioPredictions supplies the concrete list of expected M2/M4 ratio intervals for four consciousness states drawn from the voxel framework. Experimental physicists running EEG protocols to classify flow, analytical, meditation, and baseline modes would cite these bounds when defining acceptance regions. The definition is a direct enumeration of four ModeRatioPrediction records, each carrying a state, ratio interval, and numeric .

claimThe predicted mode ratios are the list of four records: flow state with interval $[1.5, 3.0]$ at , analytical state with $[0.3, 0.8]$ at , meditation state with $[0.9, 1.1]$ at , and baseline state with $[0.8, 1.2]$ at .

background

The module formalizes testable predictions derived from the voxel/meaning framework. Its core claims include EEG peaks at powers of phi during meditation and the use of M2/M4 ratios to classify consciousness states; every prediction is explicitly labeled a hypothesis carrying falsification criteria. ModeRatioPrediction is the record type that pairs a ConsciousnessState with an expected ratio interval (ratio_low to ratio_high) and a value. The upstream structure definition supplies exactly this record layout, which the present definition populates with four concrete instances.

proof idea

The definition is a direct list literal containing four ModeRatioPrediction records. No lemmas or tactics are invoked; the body simply enumerates the four states together with their chosen ratio bounds and values.

why it matters in Recognition Science

This definition operationalizes one of the four core experimental predictions listed in the module header: that M2/M4 ratios classify consciousness states. It therefore supplies the numerical targets against which EEG data can be compared, closing the loop from the Recognition Science phi-ladder and J-cost formalism to concrete, falsifiable measurements. Because the module treats all such lists as hypotheses, the definition also marks the boundary between derived theory and pending experimental test.

scope and limits

formal statement (Lean)

 123def modeRatioPredictions : List ModeRatioPrediction :=

proof body

Definition body.

 124  [⟨.flow, 1.5, 3.0, 0.95⟩,        -- High M2/M4 in flow
 125   ⟨.analytical, 0.3, 0.8, 0.95⟩,  -- Low M2/M4 in analytical
 126   ⟨.meditation, 0.9, 1.1, 0.95⟩,  -- Balanced in meditation
 127   ⟨.baseline, 0.8, 1.2, 0.90⟩]    -- Variable at baseline
 128
 129/-- Check if measured ratio falls in predicted range -/

depends on (1)

Lean names referenced from this declaration's body.