schumann_spans_eeg_bands
plain-language theorem explainer
The theorem places the five phi-derived Schumann harmonics into EEG bands: the fundamental in theta (4-8 Hz), harmonics 2-4 in beta (13-30 Hz), and the fifth in gamma (30-100 Hz). Researchers studying electromagnetic coupling between planetary cavities and neural oscillations cite it to connect the Recognition Science spectrum to observed brain rhythms. The proof is a direct term that assembles five pre-established band-membership facts for each harmonic.
Claim. Let $f(n) = (4n-1)φ + 3$ with $φ = (1 + √5)/2$. Then $f(1)$ lies in the interval [4, 8] Hz, $f(2)$, $f(3)$, and $f(4)$ lie in [13, 30] Hz, and $f(5)$ lies in [30, 100] Hz.
background
The EarthBrainResonance module defines the Schumann resonances from the Recognition Science formula $f(n) = (4n-1)φ + 3$, where $φ$ is the self-similar fixed point forced by T6 and $D = 3$ is the spatial dimension forced by T8. The predicate inFreqBand checks whether a frequency falls inside a closed interval. Upstream, PhiForcingDerived.of supplies the structure of J-cost and the phi-ladder, while DAlembert.LedgerFactorization.of calibrates the underlying ledger arithmetic. The module doc states that all five harmonics match measured values within 0.06 Hz using only these RS-forced quantities.
proof idea
The proof is a term-mode wrapper that constructs the conjunction directly from five sibling lemmas: harmonic1_in_theta for the fundamental, harmonic2_in_beta, harmonic3_in_beta, and harmonic4_in_beta for the middle harmonics, and harmonic5_in_gamma for the highest. Each component lemma is an algebraic verification that the explicit phi expression lies inside the target interval.
why it matters
This theorem supplies the band-placement facts required by the master theorem earthBrainResonance_forced, which certifies that the full Earth-Brain resonance follows from the Recognition Composition Law with zero free parameters. It realizes the module claim that the Schumann spacing 4φ ≈ 6.47 Hz and the EEG boundary ratio 13/8 ≈ φ establish a structural link, consistent with T6 self-similarity and T8 dimension forcing. The module doc notes the connection to the eight-tick octave via the factor 4 = D + 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.