harmonic5_in_gamma
plain-language theorem explainer
The RS-predicted fifth Schumann harmonic frequency lies inside the gamma EEG band [30, 100) Hz. Neuroscientists and physicists studying brain-Earth coupling would cite this to connect cavity resonances to neural oscillations. The proof is a one-line wrapper that unfolds the band-membership predicate and applies linear arithmetic to the precomputed numerical bounds on f(5).
Claim. $30 ≤ f(5) < 100$, where $f(n) = (4n-1)φ + 3$ and $φ = (1 + √5)/2$.
background
The module derives Schumann resonance frequencies from Recognition Science using only the golden ratio φ (T6 self-similar fixed point) and spatial dimension D = 3 (T8). The general formula is f(n) = (4n − 1)·φ + 3, equivalently D·φ² + (n−1)·(D+1)·φ, with 4 = 2^(D−1) half the eight-tick octave period. schumannRS n is the definition (4*(n:ℝ) − 1)*φ + 3. inFreqBand f low high is the proposition low ≤ f ∧ f < high. harmonic5_bounds supplies the tight interval 33.742 < schumannRS 5 < 33.761 obtained by rewriting to 19φ + 3 and applying the supplied inequalities on φ.
proof idea
One-line wrapper that unfolds inFreqBand to the conjunction 30 ≤ schumannRS 5 ∧ schumannRS 5 < 100, then applies linarith separately to each conjunct using the left and right sides of harmonic5_bounds.
why it matters
This supplies the gamma-band membership for harmonic 5 inside the parent theorem schumann_spans_eeg_bands, which asserts that the five Schumann harmonics occupy exactly theta (fundamental), beta (harmonics 2–4), and gamma (harmonic 5). It completes the module claim that Earth cavity modes mirror brain frequency architecture via RS-forced quantities φ and D = 3. The placement at gamma onset aligns with the eight-tick octave through the factor 4 = 2^(D−1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.