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

EEGPrediction

show as:
view Lean formalization →

EEGPrediction supplies the record type for expected EEG spectral peaks at integer powers of the golden ratio. Experimental physicists testing Recognition Science would reference this structure when logging meditation-induced bands and their detection thresholds. The declaration is a direct structure definition that enumerates five fields with two defaults supplied inline.

claimA record consisting of an integer mode index $n$, real center frequency $f = φ^n$ in Hz, bandwidth $Δf$ in Hz (default 0.2), minimum amplitude in μV²/Hz, and detection confidence (default 0.95).

background

Recognition Science places physical frequencies on the phi-ladder generated by the self-similar fixed point T6. The module Experiments.Protocols turns the voxel framework into concrete laboratory claims, beginning with EEG peaks at φ^n Hz during meditation. Upstream, SpectralEmergence.of shows how the same lattice forces SU(3)×SU(2)×U(1) and three generations, while PhiForcingDerived.of encodes the J-cost that selects discrete modes; NucleosynthesisTiers.of and LedgerFactorization.of supply the tier and calibration language reused here.

proof idea

The declaration is a plain structure definition that introduces the five fields without any computational content or proof obligations.

why it matters in Recognition Science

This structure supplies the data format consumed by eegPredictions, which populates the list checked inside theoryConfirmed. It directly encodes the first core prediction in the module documentation. The construction therefore links the phi-forcing axioms (T6) and the eight-tick octave (T7) to an observable channel that can falsify the entire framework if the predicted bands are absent.

scope and limits

formal statement (Lean)

  49structure EEGPrediction where
  50  /-- The mode index n in φ^n -/
  51  mode_index : ℤ
  52  /-- Central frequency (φ^n Hz) -/
  53  center_freq : ℝ
  54  /-- Expected peak width (Hz) -/
  55  bandwidth : ℝ := 0.2

proof body

Definition body.

  56  /-- Minimum peak amplitude (μV²/Hz) -/
  57  min_amplitude : ℝ
  58  /-- Confidence level for detection -/
  59  confidence : ℝ := 0.95
  60
  61/-- The set of predicted EEG frequencies -/

used by (2)

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

depends on (11)

Lean names referenced from this declaration's body.