`BookProof.ChapterSolidHarmonic.inner_v_spherePt` (r θ φ : ℝ) : ⟪v, spherePt u v e r θ φ⟫_ℝ = r * Real.sin θ * Real.sin φ

Prove the following Lean 4 theorem from ChapterSolidHarmonic.

BookProof.ChapterSolidHarmonic.inner_v_spherePt (r θ φ : ℝ) : ⟪v, spherePt u v e r θ φ⟫_ℝ = r * Real.sin θ * Real.sin φ

Formalization note: Lean 4 identifier BookProof.ChapterSolidHarmonic.inner_v_spherePt.

Retired 2026-10-30 — superseded by a corrected statement, not withdrawn. The exported target lost the frame hypotheses hu hv he huv hue hve: they were section variables that do not occur in the type of the theorem, so Lean quantified over arbitrary vectors $u$, $v$, $e$ instead of an orthonormal frame, and the identity $\langle v, \mathrm{spherePt}\rangle = r\sin\theta\sin\varphi$ is false for them.

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.inner_v_spherePt_frames_explicit in timepiece/BookProof/HarmonicAnalysis/ChapterSolidHarmonic.lean (Lean 4.28 tree),
• BookProof.ChapterSolidHarmonic.inner_v_spherePt_frames_explicit in timepiece331/BookProof/ChapterSolidHarmonic.lean (Lean 4.33.1 tree).

It is published on the platform as BookProof.ChapterSolidHarmonic.inner_v_spherePt_frames_explicit. This record stays readable and importable for anything already citing it; its proof status is unchanged.