harmonic1_matches
plain-language theorem explainer
The theorem shows that the Recognition Science formula for the fundamental Schumann resonance frequency lies within 0.03 Hz of the observed 7.83 Hz value. Geophysicists examining zero-parameter models of cavity resonances would cite the bound when comparing RS predictions to ionosphere data. The proof substitutes the explicit expression for the predicted frequency and discharges the resulting inequalities via linear arithmetic on the golden-ratio interval bounds.
Claim. $|(4n-1)φ + 3 - 7.83| < 0.03$ at $n=1$, where $φ$ denotes the golden ratio and the left-hand side is the absolute deviation of the RS-predicted first harmonic from the measured value.
background
The EarthBrainResonance module matches measured Schumann harmonics (7.83, 14.3, 20.8, 27.3, 33.8 Hz) to the zero-parameter expression $f(n) = (4n-1)φ + 3$, with $φ$ the golden ratio from T6 and the coefficient 4 arising from $D+1$ where $D=3$ is forced by T8. The definition schumannRS(n) implements this formula directly. Upstream, harmonic1_eq records the specialization schumannRS 1 = 3φ + 3. The supporting bounds phi_gt_1618 and phi_lt_1619 establish the concrete interval 1.618 < φ < 1.619 used for numerical verification.
proof idea
Term-mode proof. The rewrite harmonic1_eq replaces schumannRS 1 by its closed form 3φ + 3. The tactic abs_lt splits the absolute-value goal into a pair of strict inequalities. Each side is discharged by nlinarith instantiated with the local phi_gt_1618 and phi_lt_1619 lemmas.
why it matters
harmonic1_matches supplies the base case for all_harmonics_match, which lifts the bound to all five harmonics inside 0.06 Hz. It is invoked inside the master theorem earthBrainResonance_forced, whose doc-comment states that the formula follows from the Recognition Composition Law alone once T6 forces φ and T8 forces D = 3. The module doc records that the fundamental equals 3φ² = φ⁴ + 1 ≈ 7.854 Hz and lands at the theta/alpha EEG boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.