Physics theoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Controlled Fraunhofer and Fresnel estimates for the scalar aperture model, with intensity-error transfer

Physical scope

Conditional model predictions for scalar aperture diffraction: the outgoing model field $u = G_{k} * α$ , its Fraunhofer and Fresnel approximations with the explicit field-error terms of the outgoing-source lemma, the transfer of those errors to the model squared field $I = \frac{1}{2} ∣ u ∣^{2}$ , and the trace caveat that the aperture datum is not the exact screen boundary data. Excluded: exact Maxwell validity, vector or polarization content, aperture back-reaction, well-posedness of simultaneously prescribed aperture traces, absolute radiometric calibration, apparatus and sampling models, and every measured or empirical claim.

Statement

Assume Countable Choice ( ${A C}_{ω}$ ) as carried by Outgoing source Helmholtz field: fundamental solution, Fraunhofer and Fresnel error terms and Exact Helmholtz boundary representation with actual traces (The Axiom of Countable Choice ( ${A C}_{ω}$ )), whose trace qualification is used in clause (d); the full-Choice modal branch of the latter is not used. Adopt the scalar aperture model and its notation from The adopted scalar aperture-diffraction model: frequency $ω > 0$ , $k = ω / c$ , aperture radius $a > 0$ , finite complex aperture distribution $α$ supported in the planar aperture $S \subset {y_{3} = 0} \cap {y : ∣ y ∣ \leq a}$ , model field $u = G_{k} * α$ , real field $U (x, t) = Re (u (x) e^{- i ω t})$ and $T = 2 π / ω$ (Framework-local SI units, the vacuum constants and the exact/measured status of their values, Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields, The complex exponential by its power series, Real and imaginary parts, complex conjugation, and modulus, Integration against a signed or complex measure, and the class L^1(nu) = L^1(|nu|)). Set $I (x) : = (1 / 2) ∣ u (x) ∣^{2}$ . Then: (a) [Model field and Fraunhofer estimate] $u$ is $C^{\infty}$ on the half-space ${x_{3} > 0}$ and on $R^{3} ∖ S$ , satisfies $(Δ + k^{2}) u = 0$ there, and is outgoing in the sense of Outgoing source Helmholtz field: fundamental solution, Fraunhofer and Fresnel error terms: for $x = r n$ with $r \geq 2 a$ and $n \in S^{2}$ , $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. (b) [Fresnel estimate] write $y_{t} = (y_{1}, y_{2})$ and $ξ = (ξ_{1}, ξ_{2})$ for transverse vectors; for the planar aperture and observation $x = (ξ_{1}, ξ_{2}, z)$ with $z > 0$ , $b \geq 0$ , $∣ ξ ∣ \leq b$ and any declared fixed small-angle range $(a + b) / z \leq η_{0} < 1$ , where $0 < η_{0} < 1$ , the Fresnel approximation replaces $R = ∣ x - y ∣$ by $z + ∣ ξ - y_{t} ∣^{2} / (2 z)$ and $1 / R$ by $1 / z$ in the model integral with phase error $O (k (a + b)^{4} / z^{3})$ , relative amplitude error $O ((a + b)^{2} / z^{2})$ and absolute field error $O (∥ α ∥_{T V} z^{- 1} [(a + b)^{2} / z^{2} + k (a + b)^{4} / z^{3}])$ . (c) [Intensity and error transfer] at every $x$ with $x_{3} > 0$ the model period average satisfies $\frac{1}{T} \int_{0}^{T} U (x, s)^{2} d s = I (x)$ (Period averages of products of real parts of complex exponentials). If $u_{a p p r o x}$ is any approximation of $u$ with $∣ u_{a p p r o x} (x) - u (x) ∣ \leq δ (x)$ , then $∣ \frac{1}{2} ∣ u_{a p p r o x} (x) ∣^{2} - I (x) ∣ \leq \frac{1}{2} δ (x) (∣ u (x) ∣ + ∣ u_{a p p r o x} (x) ∣)$ ; if moreover $u (x) \neq 0$ and $∣ u_{a p p r o x} (x) - u (x) ∣ \leq ϵ (x) ∣ u (x) ∣$ , the relative intensity error is at most $2 ϵ (x) + ϵ (x)^{2}$ . In particular the Fraunhofer and Fresnel field errors of (a) and (b) bound the corresponding intensity errors; no new approximation is introduced by passing to $I$ . (d) [Trace and scope] the aperture distribution $α$ is an adopted model datum and is not identified with the exact Maxwell boundary data on the screen; assigning both $u$ and $\partial_{n} u$ on the aperture independently does not produce a well-posed exact boundary problem (Exact Helmholtz boundary representation with actual traces). The construction ignores polarization and aperture back-reaction, makes no claim that $u$ or $U$ satisfies the Maxwell equations exactly, and makes no measured-intensity, apparatus, sampling or empirical claim; only comparisons of $I$ between observation points are read as model predictions.

Facts & Assumptions

Given: The model data of the Statement: $ω > 0$ , $k = ω / c$ , $a > 0$ , the compact planar aperture $S \subset {y_{3} = 0} \cap {∣ y ∣ \leq a}$ , the finite complex measure $α$ supported in $S$ , the model field $u = G_{k} * α$ with $G_{k} (z) = e^{i k ∣ z ∣} / (4 π ∣ z ∣)$ for $z \neq 0$ , the real field $U (x, t) = Re (u (x) e^{- i ω t})$ , and $I = \frac{1}{2} ∣ u ∣^{2}$ . All lengths are in the laboratory chart of Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields, and $c$ , $ε_{0}$ , $μ_{0}$ are those of Framework-local SI units, the vacuum constants and the exact/measured status of their values.

[F1]

Model interface: the aperture distribution is a finite complex measure with total variation $∥ α ∥_{T V}$ supported in the compact $S$ , read in volts; for every $x$ with $x_{3} > 0$ the pairing $\int G_{k} (x - y) d α (y)$ is defined by Integration against a signed or complex measure, and the class L^1(nu) = L^1(|nu|) and equals the model field $u (x)$ ; the same formula defines $u$ at every $x \notin S$ , and $U$ , $I$ are as in the Statement (The adopted scalar aperture-diffraction model, The total variation |nu|(E) from countable measurable partitions, Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields, Framework-local SI units, the vacuum constants and the exact/measured status of their values).

[F2]

Outgoing-source and trace suppliers: assume ${A C}_{ω}$ ; $G_{k}$ is locally integrable, $(- Δ - k^{2}) G_{k} = δ_{0}$ distributionally, and for a finite complex measure supported in a closed ball the field $G_{k} * α$ is $C^{\infty}$ outside its support, solves $(Δ + k^{2}) w = 0$ there, is outgoing with the Fraunhofer and Fresnel error terms of that item, and the aperture data are an explicitly specified scalar source, not the exact Maxwell boundary traces; assigning both aperture values independently is not a well-posed exact boundary problem (Outgoing source Helmholtz field: fundamental solution, Fraunhofer and Fresnel error terms, Exact Helmholtz boundary representation with actual traces, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F3]

Finite-measure integral bound: let $h$ be Borel measurable and bounded on the support of the finite complex measure $α$ , with $M_{h} : = \sup_{supp α} ∣ h ∣ < + \infty$ ; then $h \in L^{1} (α) = L^{1} (∣ α ∣)$ and $∣ \int h d α ∣ \leq \int ∣ h ∣ d ∣ α ∣ \leq M_{h} ∥ α ∥_{T V}$ : the modulus bound for a general integrand is Integrals against signed or complex measures are bounded by total variation, integrability in $L^{1} (α) = L^{1} (∣ α ∣)$ is the definition of Integration against a signed or complex measure, and the class L^1(nu) = L^1(|nu|), and since $α$ is supported in $S$ the variation $∣ α ∣$ vanishes off $S$ by its defining supremum over partitions (The total variation |nu|(E) from countable measurable partitions) and is finite (The total variation of a signed or complex measure is a positive measure, Every complex measure has finite total variation), so monotonicity of the integral of nonnegative measurable functions gives $\int ∣ h ∣ d ∣ α ∣ \leq \int M_{h} d ∣ α ∣ = M_{h} ∥ α ∥_{T V}$ (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F4]

Period average: for $ω > 0$ , $T = 2 π / ω$ and $u \in C$ , $\frac{1}{T} \int_{0}^{T} Re (u e^{- i ω t})^{2} d t = \frac{1}{2} ∣ u ∣^{2}$ (Period averages of products of real parts of complex exponentials).

[F5]

Modulus and conjugation: $z \overline{z} = ∣ z ∣^{2}$ , $∣ z ∣ \geq 0$ , $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ , and $∣ ∣ z ∣ - ∣ w ∣ ∣ \leq ∣ z - w ∣$ for all $z, w \in C$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Real and imaginary parts, complex conjugation, and modulus).

[F6]

Elementary toolbox: $∣ a + b i ∣ = \sqrt{a^{2} + b^{2}}$ and $e^{i θ} = \cos θ + i \sin θ$ for real $θ$ , with the addition law $e^{z + w} = e^{z} e^{w}$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential), $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , $∣ \cos θ ∣ \leq 1$ and $\cos^{2} θ + \sin^{2} θ = 1$ (Real and imaginary parts, complex conjugation, and modulus, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine); the Taylor remainder bound $∣ R_{n, a} f (x) ∣ \leq M s^{n + 1} / (n + 1)!$ when $∣ f^{(n + 1)} ∣ \leq M$ on the interval, with $R_{n, a} f = f - T_{n, a} f$ (A uniform derivative bound gives a uniform Taylor remainder bound, Taylor polynomials and their remainders); the real-power derivatives $(x^{α})^{'} = α x^{α - 1}$ on $(0, \infty)$ (Continuity and derivatives of positive-base real powers); the chain and algebra of derivatives (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 Euclidean norm and inner product with $\sqrt{}$ the nonnegative square root (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , The complex exponential by its power series).

Proof

technique · direct; instantiate the supplier's off-support regularity on the declared closed ball, re-derive the sharp closed-radius Fraunhofer and outgoing estimates from the explicit kernel with elementary Taylor bounds, establish the Fresnel estimates through the exact substitution $R=z\sqrt{1+s}$, and transfer the field errors to the intensity with the modulus inequalities

1.1givenF1F2

[Off-support regularity and the Helmholtz equation] Since $S$ is compact and contained in the closed ball $\overline{B_{a} (0)}$ , $α$ is a finite complex measure supported in that closed ball, exactly as required by [F2]. By [F2] the field $G_{k} * α$ is $C^{\infty}$ outside the support of $α$ and solves $(Δ + k^{2}) w = 0$ there; since the support of $α$ is contained in $S$ , the field $u$ of [F1] is $C^{\infty}$ on $R^{3} ∖ S$ and satisfies $(Δ + k^{2}) u = 0$ there; the half-space ${x_{3} > 0}$ is disjoint from the plane containing $S$ , hence is contained in $R^{3} ∖ S$ , so $u$ is $C^{\infty}$ there as well.

1.2givenF6algebra

[Elementary bounds: phase, radial expansion, kernel residual] First, for every real $θ$ one has $∣ e^{i θ} - 1 ∣ \leq ∣ θ ∣$ : by [F6], $2 (1 - \cos θ) = ∣ e^{i θ} - 1 ∣^{2}$ and $∣ \cos θ ∣ \leq 1$ , and the Taylor bound for $\cos$ at $0$ with $n = 1$ gives $∣ \cos θ - 1 ∣ \leq θ^{2} / 2$ , because $∣ \cos^{''} ∣ \leq 1$ ; hence $∣ e^{i θ} - 1 ∣^{2} = 2 (1 - \cos θ) \leq θ^{2}$ . Second, fix $y \in S$ , $r \geq 2 a$ , $n \in S^{2}$ , and put $R : = ∣ r n - y ∣$ and $h (s) : = ∣ r n - s y ∣$ for $s \in [0, 1]$ ; then $h$ is $C^{2}$ on $[0, 1]$ with $h (0) = r$ , $h (1) = R$ , $h^{'} (0) = - n \cdot y$ , $h^{'} (s) = - (r n - s y) \cdot y / h (s)$ , $h^{''} (s) = ∣ y ∣^{2} / h (s) - ((r n - s y) \cdot y)^{2} / h (s)^{3}$ , so $∣ h^{''} ∣ \leq 2 ∣ y ∣^{2} / h (s) \leq 2 a^{2} / (r - a) \leq 4 a^{2} / r$ by $h (s) \geq r - a \geq r / 2$ ; the Taylor bound at $0$ with $n = 1$ gives $∣ R - r + n \cdot y ∣ \leq 2 a^{2} / r$ , and then $∣ r / R - 1 ∣ = ∣ r - R ∣ / R \leq (a + 2 a^{2} / r) / (r / 2) = 2 a / r + 4 a^{2} / r^{2} \leq 4 a / r$ since $∣ r - R ∣ \leq ∣ n \cdot y ∣ + 2 a^{2} / r \leq a + a = 2 a$ , $R \geq r / 2$ , and $r \geq 2 a$ gives $4 a^{2} / r^{2} \leq 2 a / r$ . Third, with $R$ as above, $\partial_{r} R = (r - n \cdot y) / R$ satisfies $∣ \partial_{r} R ∣ \leq 1$ and $∣ \partial_{r} R - 1 ∣ \leq ∣ R - r + n \cdot y ∣ / R \leq 4 a^{2} / r^{2}$ , and the exact kernel derivatives give $\partial_{r} G_{k} (r n - y) = \partial_{r} R (i k - 1 / R) e^{i k R} / (4 π R)$ and hence $∣ \partial_{r} G_{k} - i k G_{k} ∣ \leq (1 / (4 π R)) [k ∣ \partial_{r} R - 1 ∣ + ∣ \partial_{r} R ∣ / R] \leq 2 k a^{2} / (π r^{3}) + 1 / (π r^{2})$ .

1.3givenF1F6algebra

[Fresnel substitution and estimates] Fix the planar observation $x = (ξ_{1}, ξ_{2}, z)$ with $z > 0$ , $∣ ξ ∣ \leq b$ , and let $y \in S$ with transverse part $y_{t}$ ; put $d_{0} : = a + b$ , $s : = ∣ ξ - y_{t} ∣^{2} / z^{2}$ , so that $0 \leq s \leq η_{0}^{2} < 1$ on the declared range. Decomposing the Euclidean norm by [F6], $R = ∣ x - y ∣ = z \sqrt{1 + s}$ , hence $1 / R = (1 / z) (1 + s)^{- 1 / 2}$ and the Fresnel replacements are $R_{F} : = z (1 + s / 2)$ and $1 / z$ . The Taylor bound of [F6] at $0$ with $n = 1$ gives $∣ \sqrt{1 + s} - 1 - s / 2 ∣ \leq s^{2} / 8$ , because $∣ (d^{2} / d t^{2}) \sqrt{1 + t} ∣ = ∣ ⁣ - ⁣ \frac{1}{4} (1 + t)^{- 3 / 2} ∣ \leq 1 / 4$ on $[0, s]$ ; the Taylor bound with $n = 0$ gives $∣ (1 + s)^{- 1 / 2} - 1 ∣ \leq s / 2$ , because $∣ (d / d t) (1 + t)^{- 1 / 2} ∣ = \frac{1}{2} (1 + t)^{- 3 / 2} \leq 1 / 2$ . Consequently the phase error satisfies $k ∣ R - R_{F} ∣ = k z ∣ \sqrt{1 + s} - 1 - s / 2 ∣ \leq k d_{0}^{4} / (8 z^{3})$ , and the relative amplitude error satisfies $∣ 1 - (1 + s)^{- 1 / 2} ∣ \leq s / 2 \leq d_{0}^{2} / (2 z^{2})$ , where $s \leq d_{0}^{2} / z^{2}$ by $∣ ξ - y_{t} ∣ \leq d_{0}$ .

1.4givenF4algebra

[Period average equals the model intensity] Fix $x$ with $x_{3} > 0$ and write $u = u (x) \in C$ ; then $U (x, s) = Re (u e^{- i ω s})$ , so [F4] applied with the complex number $u$ in both slots gives $\frac{1}{T} \int_{0}^{T} U (x, s)^{2} d s = \frac{1}{2} ∣ u ∣^{2} = I (x)$ .

2.1step 1.2F1F2F3F6algebra

[Fraunhofer estimate at the closed radius] Fix $y \in S$ , $r \geq 2 a$ and $n \in S^{2}$ , and write $R = ∣ r n - y ∣$ . Using only the bounds of step 1.2 and the addition law of the exponential for $e^{i k (r - n \cdot y)} = e^{i k r} e^{- i k n \cdot y}$ from [F6], one has $∣ G_{k} (r n - y) - e^{i k r} e^{- i k n \cdot y} / (4 π r) ∣ = ∣ e^{i k R} (r / R - 1) + e^{i k R} - e^{i k (r - n \cdot y)} ∣ / (4 π r) \leq (1 / (4 π r)) [4 a / r + k \cdot 2 a^{2} / r] \leq (1 / (π r)) [a / r + k a^{2} / r]$ , since $4 / (4 π) = 1 / π$ and $2 / (4 π) \leq 1 / π$ , and because the middle term was bounded by $∣ e^{i θ} - 1 ∣ \leq ∣ θ ∣$ with $θ : = k (R - r + n \cdot y)$ and $∣ θ ∣ \leq 2 k a^{2} / r$ . Integrating against $α$ with the bound of [F3], applied to the bounded continuous function $y \mapsto G_{k} (r n - y) - e^{i k r} e^{- i k n \cdot y} / (4 π r)$ on the compact support, gives $∣ u (r n) - e^{i k r} (4 π r)^{- 1} \int e^{- i k n \cdot y} d α (y) ∣ \leq ∥ α ∥_{T V} (π r)^{- 1} [a / r + k a^{2} / r]$ , uniformly in $n$ ; this is the displayed Fraunhofer estimate with a universal constant.

2.2step 1.3F1F2F3F6algebra

[Absolute field error of the Fresnel replacement] With the substitutions of step 1.3, for $y \in S$ : $∣ G_{k} (x - y) - e^{i k R_{F}} / (4 π z) ∣ \leq (1 / (4 π)) ∣ 1 / R - 1 / z ∣ + (1 / (4 π z)) ∣ e^{i k R} - e^{i k R_{F}} ∣ \leq (1 / (4 π)) d_{0}^{2} / (2 z^{3}) + (1 / (4 π z)) k d_{0}^{4} / (8 z^{3}) = (1 / (4 π z)) [d_{0}^{2} / (2 z^{2}) + k d_{0}^{4} / (8 z^{3})]$ , where the first summand used $∣ 1 / R - 1 / z ∣ = (1 / z) ∣ (1 + s)^{- 1 / 2} - 1 ∣ \leq d_{0}^{2} / (2 z^{3})$ and the second used $∣ e^{i k R} - e^{i k R_{F}} ∣ \leq k ∣ R - R_{F} ∣ \leq k d_{0}^{4} / (8 z^{3})$ from the phase estimate of step 1.3. Integrating against $α$ with [F3] gives $∣ u (x) - u_{F r e s n e l} (x) ∣ \leq ∥ α ∥_{T V} (4 π z)^{- 1} [d_{0}^{2} / (2 z^{2}) + k d_{0}^{4} / (8 z^{3})]$ , the displayed absolute field error with universal constants; the phase and relative amplitude errors of step 1.3 are those displayed in (b).

3.1step 1.2step 2.1F1F2F3algebra

[Outgoing residual] With the third bound of step 1.2 and the same integration against the total variation [F3], $r ∣ \partial_{r} u (r n) - i k u (r n) ∣ \leq r \int ∣ \partial_{r} G_{k} (r n - y) - i k G_{k} (r n - y) ∣ d ∣ α ∣ (y) \leq ∥ α ∥_{T V} [2 k a^{2} / (π r^{2}) + 1 / (π r)]$ , which is uniformly $O (∥ α ∥_{T V} r^{- 1})$ in direction; this and step 2.1 give clause (a).

3.2step 1.4step 2.1step 2.2F5algebra

[Intensity error transfer] Let $u_{a p p r o x}$ satisfy $∣ u_{a p p r o x} (x) - u (x) ∣ \leq δ (x)$ at the point $x$ . By the reverse triangle inequality of [F5], $∣ ∣ u_{a p p r o x} ∣ - ∣ u ∣ ∣ \leq ∣ u_{a p p r o x} - u ∣ \leq δ$ , and by $∣ z ∣^{2} = z \overline{z}$ and multiplicativity of the modulus [F5], $∣ ∣ u_{a p p r o x} ∣^{2} - ∣ u ∣^{2} ∣ = ∣ ∣ u_{a p p r o x} ∣ - ∣ u ∣ ∣ (∣ u_{a p p r o x} ∣ + ∣ u ∣) \leq δ (x) (∣ u (x) ∣ + ∣ u_{a p p r o x} (x) ∣)$ ; multiplying by $\frac{1}{2}$ and comparing with step 1.4 gives the first bound of (c). If additionally $u (x) \neq 0$ and $∣ u_{a p p r o x} - u ∣ \leq ϵ (x) ∣ u (x) ∣$ , then $∣ u_{a p p r o x} ∣ \leq (1 + ϵ (x)) ∣ u (x) ∣$ , so the absolute intensity error is at most $\frac{1}{2} ϵ (x) ∣ u (x) ∣ (2 + ϵ (x)) ∣ u (x) ∣ = (ϵ (x) + \frac{1}{2} ϵ (x)^{2}) ∣ u (x) ∣^{2} = (2 ϵ (x) + ϵ (x)^{2}) I (x)$ , which is the stated relative bound; applying these two estimates to the Fraunhofer and Fresnel field errors of steps 2.1, 3.1 and 2.2 gives the final sentence of (c) with no new approximation.

4.1step 3.1step 2.2step 3.2F1F2F4given∎

[Trace caveat, scope and choice accounting] The aperture distribution $α$ is the adopted datum of [F1] and is not identified with the exact Maxwell boundary data on the screen; by [F2] assigning both $u$ and $\partial_{n} u$ on the aperture independently is not a well-posed exact boundary problem, so no such identification or well-posedness is made. The construction never asserts that $u$ or $U$ satisfies the Maxwell equations; it ignores polarization and aperture back-reaction, and it makes no measured-intensity, apparatus, sampling or empirical claim, only model comparisons of $I$ between observation points; this is clause (d). The only choice principle used is the Countable Choice carried by the two suppliers of [F2] and used in their trace and kernel interfaces; the period average of step 1.4 uses only the choice-free period-average lemma, and all other steps are explicit estimates and finite computations, so no further choice is invoked.

Remarks

The two big-O statements of (a) are established by the proof in the quantitative form $∣ u (r n) - e^{i k r} (4 π r)^{- 1} \int e^{- i k n \cdot y} d α ∣ \leq ∥ α ∥_{T V} (π r)^{- 1} [a / r + k a^{2} / r]$ and $r ∣ \partial_{r} u - i k u ∣ \leq ∥ α ∥_{T V} (2 k a^{2} / (π r^{2}) + 1 / (π r))$ , both uniform in direction; the big-O form is the same statement with a universal constant.
The Fresnel error transfer is an error statement about the adopted model field, not about any measured optical intensity; the model comparison is between observation points of $I = \frac{1}{2} ∣ u ∣^{2}$ only.

Controlled Fraunhofer and Fresnel estimates for the scalar aperture model, with intensity-error transfer

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources