all_harmonics_match
plain-language theorem explainer
Recognition Science predicts Schumann resonance frequencies via the zero-parameter formula f(n) = (4n-1)phi + 3. Geophysicists and neuroscientists examining cavity-brain coupling would cite the result to show that the five observed harmonics lie within 0.06 Hz of the predictions. The proof proceeds by applying the linarith tactic to each of the five individual harmonic match lemmas.
Claim. Let $f(n) = (4n-1)phi + 3$ with $phi = (1 + sqrt(5))/2$. Then $|f(1) - 7.83| < 0.06 land |f(2) - 14.3| < 0.06 land |f(3) - 20.8| < 0.06 land |f(4) - 27.3| < 0.06 land |f(5) - 33.8| < 0.06$.
background
In the Earth-Brain Resonance module the Schumann frequencies are generated from the Recognition Science constants. The function evaluates to (4n-1) times the golden ratio phi plus 3, where phi is fixed by the self-similar fixed point T6 and 3 is the spatial dimension D from T8. The module doc states that the formula uses only RS-forced quantities with zero free parameters. Upstream lemmas establish the match for each harmonic separately before this theorem combines them.
proof idea
The tactic proof invokes linarith on the first harmonic match lemma for the opening inequality, repeats the tactic on the second, third, and fourth lemmas, and discharges the final inequality directly from the fifth harmonic match lemma. No rewriting or case splits appear.
why it matters
The declaration completes the empirical verification step in the master theorem earthBrainResonance_forced, which packages the zero-parameter formula, the fundamental identity 3 phi squared equals phi to the fourth plus one, and the strict increase of the sequence. It directly supports the claim that the Recognition Composition Law forces the observed Earth-ionosphere spectrum and its alignment with EEG bands. The result touches the open question of whether higher harmonics continue to match without adjustment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.