harmonic4_bounds
plain-language theorem explainer
The theorem proves that the Recognition Science formula for the fourth Schumann harmonic satisfies 27.270 Hz < f(4) < 27.285 Hz. Researchers modeling zero-parameter geophysical resonances or EEG band alignments would cite this interval to confirm agreement with the observed 27.3 Hz peak within 0.03 Hz. The proof rewrites the target using the closed-form equality for n=4 and applies nonlinear arithmetic on the golden-ratio bounds.
Claim. Let $f(n) = (4n-1)φ + 3$ with $φ$ the golden ratio. Then $27.270 < f(4) ∧ f(4) < 27.285$.
background
The module constructs Schumann resonance frequencies from Recognition Science using only the golden ratio forced at T6 and spatial dimension D=3 forced at T8. The definition schumannRS(n) := (4n − 1)·φ + 3 encodes the general form f(n) = D·φ² + (n−1)·(D+1)·φ. The fourth harmonic is isolated by the sibling result that states schumannRS(4) = 15·φ + 3. Interval bounds on φ are supplied by the lemmas establishing 1.618 < φ and φ < 1.619.
proof idea
The proof rewrites the inequality via the equality that expands schumannRS(4) to 15·φ + 3. It then splits the conjunction and applies nlinarith to each side, citing the lower bound on φ for the left inequality and the upper bound for the right inequality.
why it matters
This bound is invoked by the downstream theorem that places the fourth harmonic inside the beta band [13,30) Hz. It supports the module claim that all five harmonics match measured values within 0.06 Hz using only RS-forced constants. The result fills the structural decomposition linking harmonics to the eight-tick octave and self-similarity of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.