`BookProof.ChapterSolidHarmonic.solidHarmonic_spherical` {l μ : ℕ} (hμ : μ ≤ l) {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : 0 ≤ Real.sin θ) (φ : ℝ) : solidHarmonic u v e l μ (spherePt u v e
DisprovedBookProof.ChapterSolidHarmonic.solidHarmonic_sphericalProve the following Lean 4 theorem from ChapterSolidHarmonic.
BookProof.ChapterSolidHarmonic.solidHarmonic_spherical {l μ : ℕ} (hμ : μ ≤ l) {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : 0 ≤ Real.sin θ) (φ : ℝ) : solidHarmonic u v e l μ (spherePt u v e r θ φ) = r ^ l * assocLegendre l μ (Real.cos θ) * Real.cos (μ * φ)
Formalization note: Lean 4 identifier BookProof.ChapterSolidHarmonic.solidHarmonic_spherical.
Retired 2026-10-30 — superseded by a corrected statement, not withdrawn. The exported target lost the frame hypotheses (section variables absent from the type), so it claimed the spherical form of a solid harmonic for an arbitrary triple of vectors rather than for an orthonormal frame.
Where the fix lives. In the source of record the hypothesis is an explicit binder of the declaration, so a re-export cannot lose it:
BookProof.ChapterSolidHarmonic.solidHarmonic_spherical_frames_explicitintimepiece/BookProof/HarmonicAnalysis/ChapterSolidHarmonic.lean(Lean 4.28 tree),BookProof.ChapterSolidHarmonic.solidHarmonic_spherical_frames_explicitintimepiece331/BookProof/ChapterSolidHarmonic.lean(Lean 4.33.1 tree).
It is published on the platform as BookProof.ChapterSolidHarmonic.solidHarmonic_spherical_frames_explicit. This record stays readable and importable for anything already citing it; its proof status is unchanged.
-- Generated from ChapterSolidHarmonic.lean — theorem BookProof.ChapterSolidHarmonic.solidHarmonic_spherical
import Definitions.Def_ChapterRadialLaplacian
import Definitions.Def_ChapterLaplacianProduct
import Definitions.Def_ChapterSolidHarmonicTools
import Mathlib
import Definitions.Def_ChapterSolidHarmonic
import Definitions.Def_ChapterLegendrePolynomial
open BookProof.ChapterLegendrePolynomial
open BookProof.ChapterSolidHarmonic
open Laplacian InnerProductSpace Polynomial
open BookProof.ChapterRadialLaplacian BookProof.ChapterLaplacianProduct
open BookProof.ChapterSolidHarmonicTools BookProof.ChapterLegendrePolynomial
open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
variable {u v e : E} (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) (he : ‖e‖ = 1)
(huv : ⟪u, v⟫_ℝ = 0) (hue : ⟪u, e⟫_ℝ = 0) (hve : ⟪v, e⟫_ℝ = 0)theorem BookProof.ChapterSolidHarmonic.solidHarmonic_spherical {l μ : ℕ} (hμ : μ ≤ l) {r : ℝ} (hr : 0 < r) {θ : ℝ}
(hθ : 0 ≤ Real.sin θ) (φ : ℝ) :
solidHarmonic u v e l μ (spherePt u v e r θ φ)
= r ^ l * assocLegendre l μ (Real.cos θ) * Real.cos (μ * φ) := by sorry