harmonic1_bounds
RS-predicted Schumann fundamental satisfies 7.854 < f(1) < 7.857 Hz. Researchers modeling ionosphere resonances or EEG band boundaries cite the bound. Proof substitutes the closed-form expression then invokes nlinarith on the golden-ratio interval lemmas.
claim$7.854 < 3φ + 3 < 7.857$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The Earth-Brain Resonance module defines the zero-parameter RS prediction for Schumann harmonics as f(n) = (4n − 1)·φ + 3, with φ the golden ratio and the constant 3 equal to spatial dimension D. The definition schumannRS implements this formula for n ≥ 1. The upstream equality harmonic1_eq specializes the formula at n = 1 to obtain schumannRS 1 = 3φ + 3.
proof idea
The proof rewrites the goal via harmonic1_eq, reducing it to bounds on 3φ + 3. It then applies nlinarith once with phi_gt_1618 to obtain the lower bound and once with phi_lt_1619 to obtain the upper bound.
why it matters in Recognition Science
The bound is invoked by fundamental_near_theta_alpha_boundary and harmonic1_in_theta to place f(1) inside the theta band and within 0.15 Hz of the 8 Hz theta/alpha boundary. It substantiates the module claim that f(1) matches the measured 7.83 Hz datum within 0.03 Hz using only RS-forced quantities (D = 3 from T8, φ from T6 self-similarity).
scope and limits
- Does not derive the general harmonic formula from the Recognition Composition Law.
- Does not bound the remaining four harmonics.
- Does not incorporate measurement error on the 7.83 Hz datum.
- Does not address higher-order corrections to the cavity model.
Lean usage
theorem harmonic1_near_8 : 8 - schumannRS 1 < 0.15 := by linarith [harmonic1_bounds.1]formal statement (Lean)
170theorem harmonic1_bounds : 7.854 < schumannRS 1 ∧ schumannRS 1 < 7.857 := by
proof body
Term-mode proof.
171 rw [harmonic1_eq]
172 exact ⟨by nlinarith [phi_gt_1618], by nlinarith [phi_lt_1619]⟩
173