harmonic2_bounds
plain-language theorem explainer
The theorem establishes that the Recognition Science formula yields a second Schumann harmonic strictly between 14.326 Hz and 14.333 Hz. Researchers comparing zero-parameter geophysical predictions to EEG bands would cite the interval when quantifying the 0.04 Hz match to the observed 14.3 Hz peak. The proof substitutes the closed-form expression for the harmonic and applies linear arithmetic on the supplied golden-ratio bounds.
Claim. Let $f(n) := (4n-1)φ + 3$ with $φ$ the golden ratio. Then $14.326 < f(2) ∧ f(2) < 14.333$.
background
The module constructs zero-parameter predictions for Schumann resonances from Recognition Science constants. The definition schumannRS(n) expands to (4n − 1)φ + 3, where the factor 4 equals D + 1 for spatial dimension D = 3 (T8) and φ is the self-similar fixed point (T6). The upstream equality harmonic2_eq states that schumannRS(2) equals exactly 7φ + 3. Separate lemmas supply the concrete bounds 1.618 < φ and φ < 1.619.
proof idea
The proof first rewrites the goal via the equality harmonic2_eq. It then splits the conjunction and applies nlinarith to each side, using the lower bound phi_gt_1618 on the left and the upper bound phi_lt_1619 on the right.
why it matters
The bound is invoked directly by the downstream theorem harmonic2_in_beta to locate the second harmonic inside the beta EEG band [13, 30). It supplies a numerical verification for the general formula f(n) = (4n−1)φ + 3 given in the module documentation, confirming agreement with the measured 14.3 Hz Schumann resonance. The result links the eight-tick octave structure and golden-ratio self-similarity to an observable cavity frequency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.