harmonic2_in_beta
plain-language theorem explainer
Recognition Science places its second Schumann harmonic inside the beta EEG band [13, 30). Physicists modeling Earth-brain electromagnetic resonance cite this to align the predicted 14.33 Hz tone with beta rhythms. The proof reduces membership to the conjunction of bounds already established for the second harmonic and discharges them by linear arithmetic.
Claim. $13 ≤ (4·2 − 1)φ + 3 < 30$, where φ = (1 + √5)/2 is the golden ratio.
background
The EarthBrainResonance module derives Schumann resonance frequencies from Recognition Science constants. The definition schumannRS n computes the nth harmonic as (4n − 1)·φ + 3, with φ the golden ratio forced by self-similarity. The predicate inFreqBand f low high asserts that the frequency f lies in the half-open interval [low, high).
proof idea
The proof first unfolds the definition of inFreqBand, converting the goal into the conjunction 13 ≤ schumannRS 2 ∧ schumannRS 2 < 30. Each conjunct is then discharged by a separate linarith tactic that invokes the corresponding bound from the theorem harmonic2_bounds.
why it matters
This placement is invoked by the theorem schumann_spans_eeg_bands, which shows that the five harmonics occupy theta, beta, and gamma bands. It completes the beta-band assignment for harmonic 2 in the Earth-brain resonance decomposition. The argument rests on the RS-forced constants φ (T6) and D = 3 (T8) that generate the frequency formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.