matchesPhiPeak
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.