inFreqBand
plain-language theorem explainer
The definition supplies a predicate asserting that a real frequency f belongs to the half-open interval from low to high. It is cited by the placement theorems that map each Schumann resonance harmonic into an EEG band. Realization consists of the direct conjunction of the two real inequalities.
Claim. The predicate holds if and only if $low ≤ f < high$.
background
The Earth-Brain Resonance module establishes a zero-parameter match between the Schumann resonance spectrum and the boundaries of EEG frequency bands using the RS-forced formula f(n) = (4n-1)φ + 3. Frequencies are classified using half-open intervals to reflect the conventional division of brain-wave regimes. The module imports the fine-structure constant from Constants.Alpha, the stable-state band operation from PreLogicalCost, and the BRF Cayley transform theta from the Riemann Hypothesis plumbing.
proof idea
The definition is a direct abbreviation of the conjunction low ≤ f ∧ f < high. No external lemmas are invoked; the body is the literal translation of interval membership into a Prop.
why it matters
This predicate is the common interface for the five harmonic placement theorems and the overall EarthBrainResonanceCert structure. It thereby links the RS-forced quantities (D = 3 from T8, φ from T6) to the observed alignment between terrestrial resonances and brain rhythms. The construction closes one link in the chain from the unified forcing chain to empirical frequency architecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.