isEEGFalsified
plain-language theorem explainer
The definition states that EEG data falsifies the phi-peak prediction precisely when the count of measured frequencies matching any phi^n value within tolerance falls below the required minimum. Experimental physicists testing consciousness-state predictions from voxel theory would cite this predicate to set rejection thresholds on meditation EEG recordings. It is realized as a direct filter-and-length comparison on the input record.
Claim. Let $D$ be a record holding a list of measured peak frequencies, tolerance $0 < t$, and integer threshold $m$. Then $D$ falsifies the prediction if the number of entries $f$ in the list satisfying $|f - phi^k| < t$ for some integer $k$ is strictly less than $m$.
background
The module supplies explicit falsification criteria for five testable predictions derived from voxel theory, among them EEG peaks at phi^n Hz during meditation. The EEGFalsification record packages a list of measured frequencies, a tolerance (default 0.2 Hz), and a minimum-match count (default 3). The upstream matchesPhiPeak predicate returns true exactly when a frequency lies within tolerance of one of the listed phi powers: phi^{-2}, phi^{-1}, 1, phi, phi^2, and so on.
proof idea
One-line wrapper that applies the matchesPhiPeak predicate to each element of measured_peaks via filter, then compares the resulting list length against the min_matches field.
why it matters
The definition supplies the concrete falsification test for the EEG phi-frequency hypothesis listed in the module's core predictions. It thereby closes the experimental interface for the phi-ladder emergence that originates in the J-uniqueness step of the unified forcing chain. No downstream declarations yet depend on it, leaving open its later linkage to statistical power calculations or integration with the mode-ratio protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.