harmonic4_in_beta
plain-language theorem explainer
The RS-predicted fourth Schumann harmonic lies inside the beta EEG band [13, 30) Hz. Researchers correlating Earth cavity resonances with brain rhythms would cite the placement. The proof is a one-line wrapper that unfolds the band predicate and applies linear arithmetic to the precomputed numerical bounds on the frequency.
Claim. Let $f(n) = (4n-1)φ + 3$ be the Recognition Science formula for the $n$-th Schumann harmonic, with $φ = (1+√5)/2$. Then $13 ≤ f(4) < 30$.
background
The module matches measured Schumann resonances to a zero-parameter formula built from RS constants. schumannRS(n) returns $(4n-1)φ + 3$, where φ is the golden-ratio fixed point forced by T6 self-similarity and the leading 3 is the spatial dimension D forced by T8. inFreqBand(f, low, high) is the predicate low ≤ f < high; here low=13 and high=30 mark the conventional beta band. Upstream harmonic4_bounds supplies the tight interval (27.270, 27.285) for f(4) by rewriting via harmonic4_eq and applying the supplied inequalities on φ.
proof idea
Unfold inFreqBand to obtain the conjunction 13 ≤ schumannRS 4 ∧ schumannRS 4 < 30. Apply linarith to the left inequality using harmonic4_bounds.1 and to the right inequality using harmonic4_bounds.2.
why it matters
The result is invoked by schumann_spans_eeg_bands to show the five harmonics occupy theta (fundamental), beta (harmonics 2–4), and gamma (harmonic 5). It completes the beta-band step for n=4 inside the formula f(n)=(4n−1)φ+3 that follows from D=3 and the eight-tick octave. The placement reinforces the claim that EEG band boundaries mirror the cavity spectrum forced by Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.