LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (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.

Outgoing source Helmholtz field: fundamental solution, Fraunhofer and Fresnel error terms

Statement

Assume Countable Choice ( ${A C}_{ω}$ ), with the exact meaning of The Axiom of Countable Choice ( ${A C}_{ω}$ ). For $k > 0$ define $G_{k} (x) = e^{i k ∣ x ∣} / (4 π ∣ x ∣)$ off the origin, a locally integrable complex function. Then

$(- Δ - k^{2}) G_{k} = δ_{0}$

distributionally: for every $ψ \in C_{c}^{\infty} (R^{3}; C)$ , $T_{G_{k}} (ψ) = \int G_{k} ψ$ , $δ_{0} (ψ) = ψ (0)$ , and $⟨ \partial_{i} T, ψ ⟩ = - ⟨ T, \partial_{i} ψ ⟩$ (Locally integrable functions as regular distributions, Distributional derivative, Dirac delta and its derivatives); thus the displayed identity means $\int G_{k} (- Δ - k^{2}) ψ = ψ (0)$ . For $a > 0$ and a finite complex measure $α$ supported in the closed ball $\overline{B_{a} (0)}$ , the field $u = G_{k} * α$ is smooth outside the support, solves $(Δ + k^{2}) u = 0$ there and is outgoing: for $x = r n$ , $r \geq 2 a$ ,

$u (r n) = \frac{e^{i k r}}{4 π r} \int e^{- i k n \cdot y} d α (y) + O ⁣ (\frac{∥ α ∥_{T V}}{r} [\frac{a}{r} + \frac{k a^{2}}{r}])$

uniformly in direction, and $r (\partial_{r} u - i k u) = O (r^{- 1})$ uniformly. For a planar aperture $y = (y_{1}, y_{2}, 0)$ with observation $x = (ξ_{1}, ξ_{2}, z)$ , $z > 0$ , $∣ ξ ∣ \leq b$ , $0 \leq b$ and $(a + b) / z < 1$ , the Fresnel approximation replaces $R = ∣ x - y ∣$ by $z + ∣ ξ - y ∣^{2} / (2 z)$ and $1 / R$ by $1 / z$ with phase error $O (k (a + b)^{4} / z^{3})$ and relative amplitude error $O ((a + b)^{2} / z^{2})$ , hence absolute field error $O (∥ α ∥_{T V} z^{- 1} [(a + b)^{2} / z^{2} + k (a + b)^{4} / z^{3}])$ . Aperture data are an explicitly specified scalar source, not asserted to be the unknown exact Maxwell boundary traces, and no uniqueness or existence for arbitrary obstacle boundary data is claimed.

Facts & Assumptions

Given: Countable Choice, $k > 0$ , a radius $a > 0$ , the kernel $G_{k}$ (with arbitrary value $G_{k} (0) = 0$ for the integral representation), a finite complex measure $α$ on the Borel sets of $R^{3}$ supported in $\overline{B_{a} (0)}$ , meaning $∣ α ∣ (R^{3} ∖ \overline{B_{a} (0)}) = 0$ , and, for $x \notin supp α$ , the field $u (x) = \int G_{k} (x - y) d α (y)$ . No value on the source support is needed.

[F1]

Radial Laplacian and derivative rules. For a $C^{2}$ function $f$ of $r = ∣ x ∣$ one has $Δ f = f^{''} (r) + 2 f^{'} (r) / r$ for $x \neq 0$ (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ); the modulus $∣ G_{k} (x) ∣ = 1 / (4 π ∣ x ∣)$ is the real fundamental kernel, which is locally integrable (Local integrability of the Laplace fundamental kernel).

[F2]

Second Green identity. On a bounded $C^{1}$ domain, $\int_{Ω} (v Δ u - u Δ v) = \int_{\partial Ω} (v \partial_{ν} u - u \partial_{ν} v)$ with outward normal (Second Green identity); apply the real identity to real and imaginary components and combine complex-bilinearly.

[F3]

General measure integrals and total variation. The integral is that of Integration against a signed or complex measure, and the class L^1(nu) = L^1(|nu|): $L^{1} (α) = L^{1} (∣ α ∣)$ , and its value is the limit of the simple integrals of $L^{1} (∣ α ∣)$ approximants. The total variation is $∥ α ∥_{T V} = ∣ α ∣ (R^{3})$ (The total variation |nu|(E) from countable measurable partitions). For a Borel function $h$ with $∣ h ∣ \leq M$ $∣ α ∣$ -almost everywhere, $\int ∣ h ∣ d ∣ α ∣ \leq M ∥ α ∥_{T V} < \infty$ , so $h \in L^{1} (α)$ and $∣ \int h d α ∣ \leq \int ∣ h ∣ d ∣ α ∣ \leq M ∥ α ∥_{T V}$ (Integrals against signed or complex measures are bounded by total variation). Kernels continuous and bounded on the compact source support extended by zero off that closed support are Borel, and their values off that support do not affect the integral. The integral triangle bound is The modulus of an integral is bounded by the integral of the modulus.

[F4]

Real calculus and norm conventions. The real Newton–Leibniz theorem Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative applies to continuous functions on a closed interval with the stated integrable interior derivative. Positive real powers have derivatives $(x^{p})^{'} = p x^{p - 1}$ and $(x^{p})^{''} = p (p - 1) x^{p - 2}$ by applying the first-derivative rule twice (Continuity and derivatives of positive-base real powers), supplying the square-root and reciprocal-square-root derivatives below. The Euclidean inner product and norm are those of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

[F5]

Complex exponential. $\exp z$ is the convergent power-series exponential of The complex exponential by its power series. Its addition law is $\exp (z + w) = \exp z \exp w$ and it extends the real exponential ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential). For real $t$ , $\exp (i t) = \cos t + i \sin t$ and $∣ \exp (i t) ∣ = 1$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ). It is entire with $\exp^{'} (z) = \exp z$ (The complex exponential is entire and its complex derivative is itself); equivalently, along a real parameter, the sine/cosine derivatives and chain rule give $(\exp (i k t))^{'} = i k \exp (i k t)$ and all higher derivatives.

[F6]

Phase norm and Lipschitz tools. $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ (The derivatives of sine and cosine are cosine and minus sine) and $\cos^{2} t + \sin^{2} t = 1$ (Parity and the Pythagorean identity for sine and cosine). The complex modulus is the Euclidean norm of its two real coordinates, is multiplicative and satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive). Clause 2 of If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz says that a continuous curve $v : [A, B] \to R^{m}$ , differentiable inside with $∥ v^{'} ∥_{2} \leq M$ , is $M$ -Lipschitz.

[F7]

Distribution conventions. A locally integrable complex kernel defines $T_{f} (ψ) = \int f ψ$ (Locally integrable functions as regular distributions), distributional derivatives pair by $⟨ \partial_{i} T, ψ ⟩ = - ⟨ T, \partial_{i} ψ ⟩$ (Distributional derivative), and $δ_{0} (ψ) = ψ (0)$ (Dirac delta and its derivatives). Pairings are complex-bilinear, without conjugating the test.

Proof

technique · direct

1.1F5F6algebra

For real $θ \neq 0$ , set $A = \min (0, θ)$ , $B = \max (0, θ)$ and $v (t) = (\cos t, \sin t)$ on $[A, B]$ . By [F6] this curve is continuous on the closed interval and differentiable inside, with $v^{'} (t) = (- \sin t, \cos t)$ and $∥ v^{'} (t) ∥_{2} = 1$ . The Lipschitz clause with $m = 2$ , $M = 1$ gives $∥ v (θ) - v (0) ∥_{2} \leq ∣ θ ∣$ . Euler's formula [F5] and the modulus convention [F6] identify this with $∣ e^{i θ} - 1 ∣ \leq ∣ θ ∣$ ; for $θ = 0$ the inequality is equality. For real $P, Q$ , the addition law and unit modulus [F5] give $∣ e^{i P} - e^{i Q} ∣ = ∣ e^{i Q} (e^{i (P - Q)} - 1) ∣ \leq ∣ P - Q ∣$ . Thus the phase bound holds for either sign and for every real phase pair, without differentiating a modulus.

1.2givenF1F5F6F7algebra

For $x \neq 0$ write $r = ∣ x ∣$ ; then $\partial_{i} r = x_{i} / r$ and the chain and algebra rules [F1] give $Δ (f \circ r) = f^{''} (r) + 2 f^{'} (r) / r$ for $C^{2}$ functions $f$ of one variable, and with $f (r) = e^{i k r} / (4 π r)$ a direct computation gives $f^{''} + 2 f^{'} / r = - k^{2} f$ , so $(Δ + k^{2}) G_{k} = 0$ off the origin; since $∣ G_{k} (x) ∣ = 1 / (4 π ∣ x ∣)$ is locally integrable, $G_{k}$ defines a regular distribution.

1.3givenF4algebra

For fixed $x = r n$ with $r \geq 2 a$ and $y \in \overline{B_{a} (0)}$ put $h (s) = ∣ x - s y ∣$ , $R = h (1)$ ; then $h$ is $C^{2}$ with $h (0) = r$ , $h^{'} (0) = - n \cdot y$ , $h^{''} (s) = ∣ y ∣^{2} / ∣ x - s y ∣ - ((x - s y) \cdot y)^{2} / ∣ x - s y ∣^{3}$ and $∣ h^{''} (s) ∣ \leq 2 a^{2} / (r - a) \leq 4 a^{2} / r$ because $∣ x - s y ∣ \geq r - s ∣ y ∣ \geq r - a \geq r / 2$ ; hence two applications of the FTC [F4] give $∣ R - r + n \cdot y ∣ \leq \sup ∣ h^{''} ∣ / 2 \leq 2 a^{2} / r$ and, since $R \geq r - a \geq r / 2$ and $∣ R - r ∣ \leq a + 2 a^{2} / r \leq 2 a$ , also $∣ r / R - 1 ∣ \leq 4 a / r$ .

2.1step 1.2step 1.1F2F3F5F7algebra

For $ψ \in C_{c}^{\infty} (R^{3}; C)$ choose $R$ with $supp ψ \subset B_{R} (0)$ and $0 < δ < R$ , and apply the second Green identity [F2] on $Ω_{δ} = B_{R} (0) ∖ {\overline{B}}_{δ} (0)$ to $u = G_{k}$ , $v = ψ$ : since $Δ G_{k} = - k^{2} G_{k}$ there, $\int_{Ω_{δ}} G_{k} (Δ + k^{2}) ψ = \int_{\partial Ω_{δ}} (G_{k} \partial_{ν} ψ - ψ \partial_{ν} G_{k})$ ; the outer sphere term vanishes because $ψ$ vanishes there, and on the inner sphere, where the outward normal of $Ω_{δ}$ is $- x / δ$ , one has $G_{k} = 1 / (4 π δ) + O (1)$ and $\partial_{r} G_{k} = - 1 / (4 π δ^{2}) + O (1 / δ)$ , so the boundary summand $- \int ψ \partial_{ν} G_{k}$ contributes $- ψ (0) + o (1)$ and the derivative-test term is $O (δ)$ ; hence $\int_{R^{3}} G_{k} (Δ + k^{2}) ψ = - ψ (0)$ , that is $⟨ (- Δ - k^{2}) T_{G_{k}}, ψ ⟩ = ψ (0)$ , so $(- Δ - k^{2}) G_{k} = δ_{0}$ distributionally.

2.2step 1.2F3F1algebra

If $α = 0$ , the integral and every asserted field bound vanish. Otherwise the field $u (x) = \int G_{k} (x - y) d α (y)$ is smooth outside $supp α$ and solves $(Δ + k^{2}) u = 0$ there: on a compact observation set $K$ with $d = dist (K, supp α) > 0$ the kernel and all its parameter derivatives are continuous and uniformly bounded on $K \times supp α$ , so the difference-quotient limits pass through the measure integral by the total-variation bound [F3], giving all derivatives by differentiation under the integral sign, and the two spatial derivatives may be moved inside to apply step 1.2 at $x - y \neq 0$ .

2.3step 1.3step 1.1F3F4F5F6algebra

For $r \geq 2 a$ the kernel difference from the Fraunhofer product is bounded by $∣ G_{k} (x - y) - \frac{e^{i k r}}{4 π r} e^{- i k n \cdot y} ∣ \leq \frac{1}{4 π} [\frac{∣ e^{i k R} - e^{i k (r - n \cdot y)} ∣}{R} + \frac{∣ r - R ∣}{r R}] \leq \frac{1}{4 π} [\frac{k ∣ R - r + n \cdot y ∣}{R} + \frac{∣ r - R ∣}{r R}] \leq \frac{C}{r} [\frac{a}{r} + \frac{k a^{2}}{r}]$ , using $∣ e^{i θ} - 1 ∣ \leq ∣ θ ∣$ from step 1.1 with the phase error of step 1.3 and $R \geq r / 2$ ; integrating this difference against $α$ with the total-variation bound [F3] gives the displayed Fraunhofer formula with the stated error, uniformly in the direction $n = x / r$ .

3.1step 2.2step 1.3F3F5F6algebra

For the outgoing relation compute $\partial_{r} G_{k} (x - y) - i k G_{k} (x - y) = \frac{e^{i k R}}{4 π R} [i k (\partial_{r} R - 1) - \partial_{r} R / R]$ with $\partial_{r} R = (r - n \cdot y) / R$ , $∣ \partial_{r} R ∣ \leq 1$ and $∣ \partial_{r} R - 1 ∣ = ∣ R - r + n \cdot y ∣ / R \leq 4 a^{2} / r^{2}$ and $1 / R \leq 2 / r$ by step 1.3, so $∣ \partial_{r} G_{k} (x - y) - i k G_{k} (x - y) ∣ \leq C (k a^{2} / r^{3} + 1 / r^{2})$ ; integrating against $α$ [F3] and multiplying by $r$ gives $r (\partial_{r} u - i k u) = O (∥ α ∥_{T V} r^{- 1} (1 + k a^{2} / r)) = O (r^{- 1})$ uniformly, the term $k a^{2} / r$ being bounded because $r \geq 2 a$ .

4.1step 1.3step 1.1F3F4F5F6algebra∎

For the planar aperture write $x = (ξ, z)$ , $y = (y_{1}, y_{2}, 0)$ and $s = ∣ ξ - y ∣^{2} / z^{2}$ , so $R = z \sqrt{1 + s}$ ; on the declared range $s \leq s_{0} < 1$ the derivatives in [F4] give $∣ (\sqrt{1 + σ})^{''} ∣ = \frac{1}{4} (1 + σ)^{- 3 / 2} \leq 1 / 4$ and $∣ ((1 + σ)^{- 1 / 2})^{'} ∣ = \frac{1}{2} (1 + σ)^{- 3 / 2} \leq 1 / 2$ on $[0, s]$ ; integrating the second-derivative bound twice and the first-derivative bound once by the FTC gives $∣ \sqrt{1 + s} - 1 - s / 2 ∣ \leq s^{2} / 8$ and $∣ (1 + s)^{- 1 / 2} - 1 ∣ \leq s / 2$ ; hence the phase error is $k z ∣ \sqrt{1 + s} - 1 - s / 2 ∣ \leq k z s^{2} / 8 = k ∣ ξ - y ∣^{4} / (8 z^{3}) \leq k (a + b)^{4} / (8 z^{3})$ , the relative amplitude error is $∣ 1 / R - 1 / z ∣ / (1 / z) = ∣ z / R - 1 ∣ \leq s / 2 \leq (a + b)^{2} / (2 z^{2})$ , and with $∣ e^{i θ} - 1 ∣ \leq ∣ θ ∣$ from step 1.1 the kernel error is at most $C z^{- 1} [(a + b)^{2} / z^{2} + k (a + b)^{4} / z^{3}]$ ; integrating against $α$ with [F3] gives the stated absolute field error, while the aperture datum remains an explicitly specified scalar source and no uniqueness or existence statement for obstacle boundary data is made; Countable Choice is inherited from the cited Green, surface and measure interfaces and no stronger principle is used.

Outgoing source Helmholtz field: fundamental solution, Fraunhofer and Fresnel error terms

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources