harmonic1_bounds
plain-language theorem explainer
The theorem establishes that the Recognition Science formula for the fundamental Schumann resonance yields a frequency strictly between 7.854 Hz and 7.857 Hz. Researchers modeling zero-parameter geophysical resonances or EEG band alignments would cite the interval to quantify the 0.03 Hz match with the observed 7.83 Hz peak. The proof reduces the claim via algebraic substitution of the explicit formula and discharges the resulting bounds with interval arithmetic on the golden-ratio sandwich.
Claim. Let $f(1) = 3φ + 3$ where $φ = (1 + √5)/2$ is the golden ratio. Then $7.854 < 3φ + 3 < 7.857$.
background
The module constructs a zero-parameter model for Schumann resonances inside the Recognition Science framework. The function schumannRS sends each positive integer n to the frequency (4n − 1)φ + 3, where φ is the self-similar fixed point forced at T6 and the coefficient 3 encodes the spatial dimension D forced at T8. The module documentation states that this yields the structural decomposition f(1) = D · φ² with spacing Δf = 4φ.
proof idea
The term proof first rewrites the target by the lemma harmonic1_eq, which states schumannRS 1 = 3φ + 3. It then applies nlinarith to the two imported lemmas that establish 1.618 < φ and φ < 1.619, producing the strict numerical bounds on the linear expression 3φ + 3.
why it matters
The bound is invoked directly by fundamental_near_theta_alpha_boundary and harmonic1_in_theta to place the fundamental just below the theta/alpha EEG boundary. It supplies the concrete numerical verification for the first harmonic of the formula f(n) = (4n − 1)·φ + 3 that the module documentation claims matches measured values within 0.03 Hz. The result thereby anchors the Earth-brain resonance interpretation at the T6 and T8 landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.