spacing_eq
plain-language theorem explainer
Consecutive terms in the RS Schumann sequence differ by exactly 4φ. Researchers verifying zero-parameter geophysical resonance fits cite this identity to confirm the observed spacing of roughly 6.47 Hz. The proof reduces directly to the sequence definition via simplification and ring normalization.
Claim. For every natural number $n$, if $f(n) = (4n-1)φ + 3$ denotes the RS-predicted Schumann frequency, then $f(n+1) - f(n) = 4φ$, where $φ$ is the golden ratio and the formula incorporates the forced spatial dimension $D=3$.
background
The module constructs Schumann resonance frequencies from Recognition Science using only forced constants. The definition schumannRS(n) sets the n-th harmonic to (4n − 1)φ + 3 for n ≥ 1. D is the abbrev for the spatial dimension fixed at 3 by the eight-tick octave. The local setting matches five measured harmonics (7.83, 14.3, 20.8, 27.3, 33.8 Hz) to the formula with errors below 0.4 percent, interpreting 3 as D, φ² as self-similarity, and 4 as D+1.
proof idea
This is a one-line wrapper that applies simp on the definition of schumannRS together with Nat.cast_add and Nat.cast_one, followed by ring normalization to obtain the constant difference 4φ.
why it matters
The result supplies the harmonic_spacing field of the master theorem earthBrainResonance_forced, which asserts the full Earth-brain resonance pattern follows from the Recognition Composition Law, the self-similar fixed point φ (T6), and the forced dimension D=3 (T8). It closes the structural decomposition by confirming Δf = 4φ matches observation within the zero-parameter claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.