LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Charged radial equation on subextremal electric RN

Statement

Let the metric, gauge, parameters, tortoise coordinate, harmonic $Y$ , and operator be exactly those of the charged radial scattering definition. For $ϖ (r) : = ω - e Q / r$ , a smooth separated solution $ψ = A_{i n} e^{- i ω t} Y (Ω) u (r_{*}) / r$ of $□_{g, A} ψ = 0$ has radial function satisfying $\frac{d^{2} u}{d r_{*}^{2}} + [{(ω - \frac{e Q}{r})}^{2} - f (r) (\frac{ℓ (ℓ + 1)}{r^{2}} + \frac{f^{'} (r)}{r})] u = 0.$ Here $f^{'}$ denotes the derivative with respect to $r$ , and derivatives of $u$ are with respect to $r_{*}$ .

Statement references

Massless charged-scalar radial scattering data

Facts & Assumptions

Given: The exact subextremal electric RN exterior and charged wave operator from the charged scattering definition, a smooth real normalized spherical harmonic $Y$ of degree $ℓ$ , and a smooth separated solution with nonzero incident normalization $A_{i n}$ .

[F1]

Massless charged-scalar radial scattering data: $g = - f d t^{2} + f^{- 1} d r^{2} + r^{2} γ_{S^{2}}$ , $A_{t} = - Q / r$ , $D_{t} = \partial_{t} + i e Q / r$ , $□_{g, A} = - f^{- 1} D_{t}^{2} + r^{- 2} \partial_{r} (r^{2} f \partial_{r}) + r^{- 2} Δ_{γ_{S^{2}}}$ , $d r_{*} / d r = f^{- 1}$ , and $Δ_{γ_{S^{2}}} Y = - ℓ (ℓ + 1) Y$ with $\int Y^{2} d ω_{S^{2}} = 1$ .

[A1]

$M > 0$ , $0 < ∣ Q ∣ < M$ , $e \in R$ , $ω > 0$ , and $ℓ \in N_{0}$ . The complex function $u$ is twice differentiable in $r_{*}$ .

Proof

1.1givenF1A1algebra

Put $ϖ (r) = ω - e Q / r$ . Since $A_{t}$ is independent of $t$ , $D_{t} (e^{- i ω t} u Y / r) = - i ϖ (r) e^{- i ω t} u Y / r$ and $D_{t}^{2} (e^{- i ω t} u Y / r) = - ϖ (r)^{2} e^{- i ω t} u Y / r$ . The angular term is $- ℓ (ℓ + 1) e^{- i ω t} u Y / r$ . Substitution into $□_{g, A} ψ = 0$ and division only by the nonzero factor $A_{i n} e^{- i ω t}$ gives $Y (Ω) B (t, r) = 0$ , where $B (t, r) = \frac{ϖ (r)^{2}}{f (r)} \frac{u}{r} + \frac{1}{r^{2}} \partial_{r} ⁣ (r^{2} f (r) \partial_{r} \frac{u}{r}) - \frac{ℓ (ℓ + 1)}{r^{3}} u .$ Multiplying by $Y$ and integrating over $S^{2}$ gives $B (t, r) = 0$ because $\int_{S^{2}} Y^{2} d ω_{S^{2}} = 1$ ; no division by $Y$ at its zeros is used.

2.1givenF1A1step 1.1algebra∎

Since $d r_{*} / d r = f^{- 1}$ , $\partial_{r_{*}} = f \partial_{r}$ , so $r^{2} f \partial_{r} (u / r) = r \partial_{r_{*}} u - f u$ . Multiplying $B = 0$ by $f r$ , the radial derivative term becomes $\frac{f}{r} \partial_{r} (r \partial_{r_{*}} u - f u) = \frac{1}{r} \partial_{r_{*}} (r \partial_{r_{*}} u - f u) = \partial_{r_{*}}^{2} u - \frac{f f^{'}}{r} u,$ where $\partial_{r_{*}} r = f$ and $\partial_{r_{*}} f = f f^{'}$ . The other terms become $ϖ^{2} u$ and $- f ℓ (ℓ + 1) u / r^{2}$ . Their sum is the asserted radial equation.

Remarks

This is a conditional separation identity for the explicitly supplied harmonic and mode. It proves neither existence of a spherical harmonic nor existence of a scattering solution.

Depends on

Massless charged-scalar radial scattering data