harmonic2_matches
plain-language theorem explainer
Recognition Science predicts the second Schumann resonance as 7φ + 3 Hz. This lies inside a 0.04 Hz window around the measured 14.3 Hz. Geophysicists or EEG researchers would cite the zero-parameter match. The proof substitutes the closed-form definition then applies linear arithmetic on the interval 1.618 < φ < 1.619.
Claim. $|7φ + 3 - 14.3| < 0.04$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module defines schumannRS(n) := (4n − 1)φ + 3. This expression uses D = 3 (T8) and the self-similar fixed point φ satisfying φ² = φ + 1 (T6). The upstream lemma harmonic2_eq states schumannRS(2) = 7φ + 3 exactly. Separate lemmas establish the tight bounds 1.618 < φ < 1.619. The module setting matches the five measured Schumann frequencies (7.83, 14.3, 20.8, 27.3, 33.8 Hz) to the RS formula with no free parameters.
proof idea
The term proof first rewrites via harmonic2_eq, then applies abs_lt to split the absolute-value inequality. Both resulting bounds are discharged by nlinarith using the phi interval lemmas phi_gt_1618 and phi_lt_1619.
why it matters
The result feeds all_harmonics_match, which verifies the full set of five harmonics within 0.06 Hz. It also supports the master definition earthBrainResonance_forced, which traces the formula to the Recognition Composition Law via T6 (φ forced) and T8 (D = 3 forced). The second harmonic lands at the theta/alpha to beta transition in EEG spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.