spacing_eq
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive absolute frequencies without the full RS forcing chain.
- Does not model damping or cavity losses in the Earth-ionosphere waveguide.
- Does not claim uniqueness outside the phi-ladder construction.
- Does not extend to non-integer indices or continuous spectra.
formal statement (Lean)
146theorem spacing_eq (n : ℕ) :
147 schumannRS (n + 1) - schumannRS n = 4 * phi := by
proof body
Term-mode proof.
148 simp only [schumannRS, Nat.cast_add, Nat.cast_one]; ring
149
150/-- The spacing 4φ is positive. -/