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

EEGProtocol

show as:
view Lean formalization →

EEGProtocol records default parameters for EEG recordings aimed at detecting phi-frequency peaks during meditation. Experimental physicists validating Recognition Science predictions would instantiate this record to fix sample size, duration, sampling rate, resolution, and electrode placement for reproducibility. The definition is a direct record with hardcoded defaults and no lemmas or computation.

claimAn EEG protocol is a record with sample size $n=30$, recording duration $T=600$ s, sampling rate $f_s=256$ Hz, frequency resolution $0.1$ Hz, and electrode list from the 10-20 system.

background

The Experiments.Protocols module formalizes testable predictions from voxel theory. Core items include EEG peaks at phi^n Hz during meditation, mode ratios classifying consciousness states, and explicit falsification criteria for each claim. Frequency is defined as the real numbers in RSNativeUnits. The upstream for structure from UniversalForcingSelfReference records structural properties required by the self-reference axioms.

proof idea

The structure is defined directly by enumerating each field with its type and default value. No lemmas are applied and no tactics are used.

why it matters in Recognition Science

This protocol supplies the concrete parameters checked inside theoryConfirmed, which returns true only when the EEG prediction is not falsified. It operationalizes the first core prediction listed in the module documentation and connects to the phi-ladder and T5 J-uniqueness by providing a measurable test for self-similar frequency patterns. The module treats the entire prediction set as hypotheses rather than theorems.

scope and limits

formal statement (Lean)

  36structure EEGProtocol where
  37  /-- Sample size for each group -/
  38  n_subjects : ℕ := 30

proof body

Definition body.

  39  /-- Recording duration in seconds -/
  40  duration_sec : ℕ := 600  -- 10 minutes
  41  /-- Sampling rate in Hz -/
  42  sampling_rate : ℕ := 256
  43  /-- Frequency resolution in Hz -/
  44  freq_resolution : ℝ := 0.1
  45  /-- Electrode positions (10-20 system) -/
  46  electrodes : List String := ["Fz", "Cz", "Pz", "O1", "O2"]
  47
  48/-- Predicted EEG peaks with confidence intervals -/

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.