harmonic1_in_theta
plain-language theorem explainer
The theorem places the fundamental Schumann resonance frequency, computed from the Recognition Science formula using only forced constants, inside the theta EEG band [4, 8) Hz. Researchers linking planetary electromagnetic modes to neural rhythms would cite it when mapping cavity spectra onto brain architecture. The proof is a one-line wrapper that unfolds the band predicate and invokes linear arithmetic on pre-established bounds.
Claim. Let $f(1)$ be the fundamental Schumann frequency $f(n)=(4n-1)φ+3$ with $φ=(1+√5)/2$. Then $4≤f(1)<8$.
background
The Earth-Brain Resonance module defines Schumann harmonics via the zero-parameter expression $f(n)=(4n-1)φ+3$, where $φ$ is the golden-ratio fixed point and the coefficient 4 arises from the eight-tick octave with spatial dimension $D=3$. The predicate inFreqBand tests closed-open interval membership for a real frequency. This setting rests on the phi-ladder and J-cost structures imported from PhiForcingDerived and SimplicialLedger, together with the alpha calibration that anchors the underlying constants.
proof idea
The proof unfolds inFreqBand and applies linarith directly to the two sides of the interval supplied by the sibling lemma harmonic1_bounds.
why it matters
The result is invoked by the parent theorem schumann_spans_eeg_bands, which shows the five harmonics occupy theta, beta, and gamma EEG bands. It completes the chain step that maps the RS-forced Schumann formula (D=3 from T8, φ from T6 self-similarity) onto observed brain-frequency boundaries. The module doc notes that the fundamental lands at the theta/alpha boundary with sub-percent error to measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.