No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
142theorem fundamental_eq_phi4_plus_1 : schumannRS 1 = phi ^ 4 + 1 := by
proof body
Term-mode proof.
143 rw [harmonic1_eq, ← three_phi_sq_eq_phi4_plus_1, phi_sq_eq]; ring
144
145/-- Consecutive Schumann harmonics are spaced by exactly 4φ = (D+1)·φ. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
phi_sq_eq
in IndisputableMonolith.Constants
decl_use
-
phi_sq_eq
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
harmonic1_eq
in IndisputableMonolith.Physics.EarthBrainResonance
decl_use
-
schumannRS
in IndisputableMonolith.Physics.EarthBrainResonance
decl_use
-
three_phi_sq_eq_phi4_plus_1
in IndisputableMonolith.Physics.EarthBrainResonance
decl_use