matchesPhiPeak
matchesPhiPeak returns true exactly when a measured frequency f lies inside a supplied tolerance of one of the six phi-ladder values phi^{-2} through phi^3. Experimental physicists running EEG protocols derived from Recognition Science would call it to score individual spectral peaks against the predicted meditation frequencies. The definition is a direct disjunction of six absolute-value comparisons with no auxiliary lemmas.
claimThe predicate matchesPhiPeak(f, tolerance) holds if and only if |f - phi^{-2}| < tolerance or |f - phi^{-1}| < tolerance or |f - 1| < tolerance or |f - phi| < tolerance or |f - phi^2| < tolerance or |f - phi^3| < tolerance, where phi is the golden-ratio fixed point of the Recognition Composition Law.
background
The Experiments.Protocols module encodes testable predictions from voxel theory, with the first core claim being EEG spectral peaks at phi^n Hz during meditation. The phi values are taken from the self-similar fixed point (T6) forced by the J-uniqueness relation in the upstream forcing chain. The module explicitly labels every prediction a hypothesis equipped with falsification criteria rather than a derived theorem.
proof idea
The definition is a noncomputable boolean expression formed by the disjunction of six strict inequalities, each comparing the absolute deviation of f from one phi power against the tolerance argument. No upstream lemmas are invoked; the body directly encodes the six-point phi-ladder match condition.
why it matters in Recognition Science
matchesPhiPeak supplies the concrete matching test consumed by isEEGFalsified, which decides whether a dataset falsifies the EEG phi-frequency hypothesis. It thereby translates the abstract phi-ladder (T5-T6) into an operational criterion for the experimental protocol. The module treats the entire construction as a hypothesis whose empirical status remains open.
scope and limits
- Does not prove that phi peaks appear in any EEG recording.
- Does not specify how tolerance or minimum-match thresholds are chosen.
- Does not extend the check to powers outside the interval from -2 to 3.
- Does not incorporate signal phase, amplitude, or coherence measures.
formal statement (Lean)
80noncomputable def matchesPhiPeak (f : ℝ) (tolerance : ℝ) : Bool :=
proof body
Definition body.
81 (|f - φ^(-2 : ℤ)| < tolerance) ||
82 (|f - φ^(-1 : ℤ)| < tolerance) ||
83 (|f - 1| < tolerance) ||
84 (|f - φ| < tolerance) ||
85 (|f - φ^(2 : ℤ)| < tolerance) ||
86 (|f - φ^(3 : ℤ)| < tolerance)
87
88/-- The EEG prediction is falsified if too few peaks match -/