harmonic3_bounds
plain-language theorem explainer
Recognition Science predicts the third Schumann harmonic at 11φ + 3 Hz, and this theorem certifies the strict bounds 20.798 < 11φ + 3 < 20.809. Researchers modeling Earth-ionosphere resonances or EEG band alignments would cite it to confirm the zero-parameter match to the observed 20.8 Hz peak within 0.01 Hz. The proof is a one-line wrapper that rewrites via the closed-form equation and applies nlinarith on the golden-ratio interval bounds.
Claim. $20.798 < 11φ + 3 ∧ 11φ + 3 < 20.809$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The EarthBrainResonance module constructs Schumann frequencies from RS-forced quantities: the golden ratio φ (self-similar fixed point, T6) and D = 3 (spatial dimensions, T8). The definition schumannRS(n) := (4 * n - 1) * φ + 3 implements the general expression f(n) = (4n − 1)·φ + 3, which reproduces the five measured harmonics within 0.06 Hz. Upstream results include harmonic3_eq proving schumannRS(3) = 11φ + 3, together with the interval lemmas phi_gt_1618 : 1.618 < φ and phi_lt_1619 : φ < 1.619.
proof idea
The proof rewrites the statement using harmonic3_eq to replace schumannRS 3 with the explicit linear form 11φ + 3. It then splits the conjunction and discharges each side with nlinarith, feeding the lower bound phi_gt_1618 into the left inequality and the upper bound phi_lt_1619 into the right inequality.
why it matters
This result is used by the downstream theorem harmonic3_in_beta to show that the third harmonic lies in the beta EEG band. It provides the concrete numerical anchor for the n = 3 case of the zero-parameter Schumann formula, verifying agreement with the measured 20.8 Hz peak to within 0.01 Hz. The bound thereby links the forced constants from the UnifiedForcingChain (T6 for φ, T8 for D = 3) to observable resonances in the Earth-ionosphere cavity and brain frequency architecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.