def
definition
schumannMeasured
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.EarthBrainResonance on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
127The formula's structure is forced by D = 3 and φ. -/
128
129/-- The RS-forced spatial dimension (from T8). -/