LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Outgoing spherical Hankel modes have positive flux and no positive-real zeros

Statement

For real $z > 0$ , let $h_{ℓ}^{(1)}$ be defined in Spherical Bessel and outgoing Hankel function conventions and set $h_{ℓ}^{(2)} (z) = \overline{h_{ℓ}^{(1)} (z)}$ . Then both solve the degree- $ℓ$ spherical radial Helmholtz equation, are linearly independent, and $Im (\overline{h_{ℓ}^{(1)} (z)} (h_{ℓ}^{(1)})^{'} (z)) = z^{- 2} .$ In particular, neither vanishes for $z > 0$ , and for $k > 0$ , $r > 0$ , $r^{2} Im (\overline{h_{ℓ}^{(1)} (k r)} \partial_{r} h_{ℓ}^{(1)} (k r)) = 1 / k .$

Facts & Assumptions

Given: The definitions and radial-solution result for spherical Bessel and Hankel functions.

[F1]

Spherical Bessel and outgoing Hankel function conventions: $j_{ℓ}$ and $h_{ℓ}^{(1)}$ are obtained from $\sin z / z$ and $- i e^{i z} / z$ using the same real differential operator $(- z)^{ℓ} (z^{- 1} d / d z)^{ℓ}$ .

[F2]

Spherical Bessel and outgoing Hankel recurrences solve the radial Helmholtz equation: $j_{ℓ}$ and $h_{ℓ}^{(1)}$ solve the same radial equation and $j_{ℓ} (h_{ℓ}^{(1)})^{'} - j_{ℓ}^{'} h_{ℓ}^{(1)} = i / z^{2}$ .

Proof

Given: Real $z > 0$ and the functions in [F1]–[F2].

1.1F1F2algebra

Conjugating the definition in [F1] commutes with its real differential operator; applying that operator to $i e^{- i z} / z$ defines $h_{ℓ}^{(2)} = \overline{h_{ℓ}^{(1)}}$ , which solves the same real-coefficient radial equation as its conjugate. The sine identity gives $j_{ℓ} = (h_{ℓ}^{(1)} + h_{ℓ}^{(2)}) / 2$ .

2.1F2step 1.1algebra

Put $h = h_{ℓ}^{(1)}$ . Substitution of $j = (h + \overset{ˉ}{h}) / 2$ into [F2] yields $(\overset{ˉ}{h} h^{'} - {\overset{ˉ}{h}}^{'} h) / 2 = i / z^{2}$ . The left side is $i Im (\overset{ˉ}{h} h^{'})$ , giving the stated identity. If $h (z) = 0$ , its left side is zero, contradicting $z^{- 2} > 0$ ; conjugation gives the same nonvanishing for $h_{ℓ}^{(2)}$ . The nonzero Wronskian also proves linear independence.

3.1step 2.1algebra∎

By the chain rule, $\partial_{r} h (k r) = k h^{'} (k r)$ . Multiplying the identity in step 2.1 by $k r^{2}$ gives $r^{2} Im (\overset{ˉ}{h} (k r) \partial_{r} h (k r)) = r^{2} k / (k^{2} r^{2}) = 1 / k$ .

Depends on

Used by

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

NIST Digital Library of Mathematical Functions, §10.50: Wronskians and Cross-Products (standard reference, not scraped)
Pierre Capel, Introduction to Scattering Theory, TALENT lecture notes (standard reference, not scraped)