def
definition
schumannRS
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.EarthBrainResonance on GitHub at line 96.
browse module
All declarations in this module, on Recognition.
explainer page
used by
-
all_harmonics_match -
EarthBrainResonanceCert -
fundamental_eq_D_phi_sq -
fundamental_eq_phi4_plus_1 -
fundamental_near_theta_alpha_boundary -
harmonic1_bounds -
harmonic1_eq -
harmonic1_in_theta -
harmonic1_matches -
harmonic2_bounds -
harmonic2_eq -
harmonic2_in_beta -
harmonic2_matches -
harmonic3_bounds -
harmonic3_eq -
harmonic3_in_beta -
harmonic3_matches -
harmonic4_bounds -
harmonic4_eq -
harmonic4_in_beta -
harmonic4_matches -
harmonic5_bounds -
harmonic5_eq -
harmonic5_in_gamma -
harmonic5_matches -
schumannMeasured -
schumannRS_strictMono -
schumann_spans_eeg_bands -
spacing_eq
formal source
93
94/-- RS-predicted n-th Schumann harmonic frequency.
95 f(n) = (4n − 1)·φ + 3, valid for n ≥ 1. -/
96def schumannRS (n : ℕ) : ℝ := (4 * (n : ℝ) - 1) * phi + 3
97
98/-- Measured Schumann resonance harmonics (Hz). -/
99def schumannMeasured : Fin 5 → ℝ
100 | ⟨0, _⟩ => 7.83
101 | ⟨1, _⟩ => 14.3
102 | ⟨2, _⟩ => 20.8
103 | ⟨3, _⟩ => 27.3
104 | ⟨4, _⟩ => 33.8
105
106/-! ## Part III: Coefficient Reduction
107
108Reduce schumannRS at each harmonic number to a clean φ-expression. -/
109
110theorem harmonic1_eq : schumannRS 1 = 3 * phi + 3 := by
111 unfold schumannRS; push_cast; ring
112
113theorem harmonic2_eq : schumannRS 2 = 7 * phi + 3 := by
114 unfold schumannRS; push_cast; ring
115
116theorem harmonic3_eq : schumannRS 3 = 11 * phi + 3 := by
117 unfold schumannRS; push_cast; ring
118
119theorem harmonic4_eq : schumannRS 4 = 15 * phi + 3 := by
120 unfold schumannRS; push_cast; ring
121
122theorem harmonic5_eq : schumannRS 5 = 19 * phi + 3 := by
123 unfold schumannRS; push_cast; ring
124
125/-! ## Part IV: Structural Identities
126