harmonic1_eq
plain-language theorem explainer
The RS-predicted first Schumann harmonic frequency equals 3φ + 3. Researchers modeling ionosphere cavity modes or EEG-geophysical correlations would cite this reduction as the base case for the zero-parameter formula. The proof is a one-line wrapper that unfolds the general schumannRS definition at n=1 and simplifies via casting and ring.
Claim. The RS-predicted first Schumann harmonic satisfies $f(1) = 3φ + 3$, where $f(n) = (4n-1)φ + 3$ for $n ≥ 1$, φ is the golden ratio, and the coefficient 3 is the spatial dimension D.
background
The Earth-Brain Resonance module defines schumannRS(n) as the n-th predicted Schumann frequency via the zero-parameter expression (4n − 1)·φ + 3. Here φ is the golden ratio fixed by T6 self-similarity, while the leading 3 equals D, the spatial dimension forced by T8. The module documentation states that this formula reproduces the five measured harmonics (7.83 Hz to 33.8 Hz) within 0.4 % and places them at EEG band boundaries. The upstream definition schumannRS supplies the general closed form that the present theorem specializes at n = 1.
proof idea
This is a one-line wrapper proof. It unfolds the definition of schumannRS, applies push_cast to convert the natural-number index to a real, and invokes the ring tactic to reduce the resulting arithmetic expression to 3φ + 3.
why it matters
The identity anchors the coefficient reduction section of the module and is invoked by the four immediate downstream theorems: fundamental_eq_D_phi_sq rewrites it to D·φ², fundamental_eq_phi4_plus_1 rewrites it to φ⁴ + 1, while harmonic1_bounds and harmonic1_matches use it to obtain the numerical interval and error bound against the measured 7.83 Hz. It thereby supplies the concrete link between the T8 dimension, the T6 fixed point, and the observed Schumann spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.