schumannRS
RS supplies the n-th Schumann harmonic frequency via the zero-parameter expression f(n) = (4n - 1) φ + 3. Geophysicists and neuroscientists comparing ionospheric resonances to EEG bands cite this formula. The declaration is a direct definition that encodes the structural decomposition using D = 3 and the golden ratio φ forced by the Recognition chain.
claimThe frequency of the n-th Schumann resonance harmonic is given by $f(n) = (4n - 1)φ + 3$, where $φ = (1 + √5)/2$ is the golden ratio and $n$ is a positive integer.
background
The Earth-Brain Resonance module models Schumann cavity modes with Recognition Science constants. Here φ denotes the golden ratio from T6 self-similarity as the fixed point of the J-function, and D = 3 is the spatial dimension forced by T8. The formula decomposes as f(n) = D φ² + (n-1)(D+1)φ, which simplifies to the given expression since φ² = φ + 1 and D + 1 = 4.
proof idea
The declaration is a direct definition that substitutes the RS constants into the linear frequency expression. No lemmas or tactics are invoked; it functions as the base case for downstream numerical verifications.
why it matters in Recognition Science
This definition anchors the EarthBrainResonanceCert structure and feeds the all_harmonics_match theorem that verifies agreement with measurements. It implements the zero-parameter claim from the module, linking T6 (φ) and T8 (D=3) to observed Earth cavity spectra and their alignment with brainwave bands.
scope and limits
- Does not derive the formula from electromagnetic boundary conditions.
- Does not include damping or quality factors.
- Does not apply to non-terrestrial cavities.
- Does not predict phase or polarization.
Lean usage
example : schumannRS 1 = 3 * phi + 3 := by rw [schumannRS]; ring
formal statement (Lean)
96def schumannRS (n : ℕ) : ℝ := (4 * (n : ℝ) - 1) * phi + 3
proof body
Definition body.
97
98/-- Measured Schumann resonance harmonics (Hz). -/
used by (29)
-
all_harmonics_match -
EarthBrainResonanceCert -
fundamental_eq_D_phi_sq -
fundamental_eq_phi4_plus_1 -
fundamental_near_theta_alpha_boundary -
harmonic1_bounds -
harmonic1_eq -
harmonic1_in_theta -
harmonic1_matches -
harmonic2_bounds -
harmonic2_eq -
harmonic2_in_beta -
harmonic2_matches -
harmonic3_bounds -
harmonic3_eq -
harmonic3_in_beta -
harmonic3_matches -
harmonic4_bounds -
harmonic4_eq -
harmonic4_in_beta -
harmonic4_matches -
harmonic5_bounds -
harmonic5_eq -
harmonic5_in_gamma -
harmonic5_matches -
schumannMeasured -
schumannRS_strictMono -
schumann_spans_eeg_bands -
spacing_eq