harmonic3_matches
plain-language theorem explainer
The RS-predicted third Schumann harmonic equals 11φ + 3 and satisfies |11φ + 3 − 20.8| < 0.01. Researchers modeling ionosphere cavity modes or EEG correlations with geophysical frequencies would cite it. The proof rewrites via the closed-form identity for schumannRS at n = 3 and discharges the resulting bounds on φ by linear arithmetic.
Claim. $|(11φ + 3) - 20.8| < 0.01$, where φ is the golden ratio.
background
The EarthBrainResonance module defines schumannRS(n) := (4n − 1)φ + 3 to encode the RS-predicted Schumann harmonics using D = 3 and the self-similar fixed point φ. The third harmonic is therefore 11φ + 3. Upstream lemmas supply the algebraic identity schumannRS 3 = 11φ + 3 together with the tight bounds 1.618 < φ < 1.619. The module context is the zero-parameter matching of the five measured Schumann frequencies to this formula, with alignment to EEG band boundaries.
proof idea
The term-mode proof rewrites the goal using harmonic3_eq to obtain 11φ + 3, applies abs_lt to split into one-sided inequalities, and closes both sides by nlinarith instantiated with the phi bounds phi_gt_1618 and phi_lt_1619.
why it matters
This lemma is invoked by all_harmonics_match to verify the full set of five harmonics within 0.06 Hz and by earthBrainResonance_forced, the master claim that the resonance spectrum follows from the Recognition Composition Law with no free parameters. It supplies the concrete numerical check for n = 3, instantiating T6 (φ) and T8 (D = 3) at the observed frequency 20.8 Hz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.