spacing_bounds
plain-language theorem explainer
The theorem proves the Schumann resonance spacing satisfies 6.472 < 4φ < 6.476. Researchers modeling zero-parameter planetary resonances cite it to confirm the golden-ratio interval matches observed harmonic spacing. The proof is a one-line wrapper applying nlinarith to the pre-established phi bounds phi_gt_1618 and phi_lt_1619.
Claim. $6.472 < 4φ < 6.476$ where $φ = (1 + √5)/2$ is the golden ratio.
background
In the Earth-Brain Resonance module the spacing between Schumann harmonics is Δf = 4φ. The module constructs the five harmonics via f(n) = (4n − 1)·φ + 3, with D = 3 from T8 and φ from T6 self-similarity. The bound verifies the numerical match to measured intervals near 6.5 Hz. Upstream phi bounds come from Numerics.Interval.PhiBounds.phi_gt_1618 and the sibling phi_lt_1619.
proof idea
The proof is a one-line term wrapper. It builds the conjunction by applying nlinarith to phi_gt_1618 for the lower inequality and nlinarith to phi_lt_1619 for the upper inequality.
why it matters
This anchors the spacing prediction inside the Earth-Brain Resonance theorem, which matches Schumann frequencies to RS-forced quantities with zero free parameters. It supports the claim that EEG band boundaries mirror the cavity spectrum via φ and D = 3. The result closes the numerical verification step before the master certificate section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.