harmonic3_in_beta
plain-language theorem explainer
The RS-predicted third Schumann harmonic lies inside the beta EEG band. Researchers modeling Earth-brain frequency coupling would cite this placement. The proof is a term-mode wrapper that unfolds the band-membership predicate and feeds the two-sided bounds from harmonic3_bounds into linear arithmetic.
Claim. $13 ≤ f(3) < 30$, where $f(n) = (4n-1)φ + 3$ and $φ = (1 + √5)/2$.
background
The module constructs Schumann resonance frequencies from Recognition Science using only forced constants: spatial dimension D = 3 and the golden ratio φ fixed by self-similarity. The explicit formula is schumannRS n := (4 * n - 1) * φ + 3. This places the harmonics at measured values within 0.4 % and aligns them with EEG band boundaries.
proof idea
The term proof first unfolds the definition of inFreqBand to obtain the conjunction low ≤ f ∧ f < high. It then supplies each conjunct by linarith applied directly to the left and right inequalities of harmonic3_bounds.
why it matters
This theorem is invoked by schumann_spans_eeg_bands to show that the five RS harmonics occupy theta, beta, and gamma bands. It completes the beta-band assignment for the third harmonic inside the zero-parameter model that links planetary cavity modes to neural architecture via T8 (D = 3) and T6 (φ).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.