harmonic1_eq
plain-language theorem explainer
The RS-predicted first Schumann harmonic equals 3φ + 3. Researchers modeling zero-parameter geophysical resonances would cite this base reduction. The proof is a one-line wrapper that unfolds the frequency definition and reduces by ring normalization.
Claim. The RS-predicted first Schumann resonance frequency satisfies $f(1) = 3φ + 3$, where $f(n) = (4n-1)φ + 3$ for $n ≥ 1$.
background
schumannRS(n) denotes the RS-predicted n-th Schumann harmonic frequency, defined by the zero-parameter expression (4n − 1)·φ + 3. The module sets D = 3 from the eight-tick octave (T8) and φ from the self-similar fixed point (T6). The local setting matches the five measured cavity frequencies (7.83 Hz to 33.8 Hz) to this formula, with the fundamental rewritten as D·φ².
proof idea
One-line wrapper that unfolds schumannRS, casts the natural number argument, and applies ring simplification.
why it matters
This supplies the base case for the coefficient reduction section. It is invoked directly by fundamental_eq_D_phi_sq to equate the fundamental with D·φ² and by harmonic1_bounds to bound the numerical match to measured 7.83 Hz. The identity closes the first step linking T6 self-similarity and T8 dimension to the observed Schumann spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.