harmonic5_matches
plain-language theorem explainer
The Recognition Science prediction for the fifth Schumann harmonic matches the measured 33.8 Hz within a 0.06 Hz tolerance. Researchers in zero-parameter physics and Earth-brain coupling would cite this verification. The proof substitutes the explicit formula for the fifth term and bounds the deviation using linear arithmetic on the golden ratio interval.
Claim. $|(19φ + 3) - 33.8| < 0.06$, where $φ$ is the golden ratio.
background
In the EarthBrainResonance module, Schumann frequencies are predicted by the zero-parameter formula schumannRS(n) := (4n − 1)φ + 3, with φ the golden ratio and the coefficient 4 arising from D + 1 where D = 3 is the spatial dimension. Upstream lemmas establish the bounds 1.618 < φ < 1.619 together with the identity schumannRS(5) = 19φ + 3. The module context links these frequencies to EEG band boundaries via the Recognition Science forcing chain.
proof idea
This is a term-mode proof that first rewrites the goal using the equality theorem harmonic5_eq to obtain |19 phi + 3 - 33.8| < 0.06. It then applies abs_lt to split into two inequalities and discharges both sides with nlinarith using the golden ratio bounds phi_gt_1618 and phi_lt_1619.
why it matters
The result is invoked by all_harmonics_match to complete the conjunction over all five harmonics and by earthBrainResonance_forced to certify the full resonance structure. It supplies the empirical closure for the highest term in the sequence derived from the Recognition Composition Law, T6 (phi self-similarity), and T8 (D=3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.