Pipeline-generated

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.

Angular-spectrum optics and controlled paraxial limits — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)Open item page →

A small angular cone can accumulate order-one phase error

Physical scope

Counterexample inside the ideal band-limited scalar angular-spectrum model in a fixed inertial chart and SI units. Its spectra are square-integrable plane data and are not asserted to be outputs of a compact finite aperture. It is a conditional model calculation, not an observed optical result.

Statement refuted

For every sequence $(δ_{n})_{n \geq 1}$ with $δ_{n} \in (0, 1)$ and $δ_{n} \to 0$ , every fixed $k_{0} > 0$ , every nonzero scalar input $u_{0, n} \in L^{2} (R^{2}; C)$ whose Fourier support lies in $∣ 2 π ξ ∣ \leq δ_{n} k_{0}$ , and every sequence of forward distances $z_{n} > 0$ satisfying $z_{n} k_{0} δ_{n}^{4} = 8 π$ , the relative exact-to-paraxial error tends to zero:

$\frac{∥ u_{e x a c t, n} (z_{n}) - u_{p a r, n} (z_{n}) ∥_{2}}{∥ u_{0, n} ∥_{2}} ⟶ 0.$

Statement references

Forward angular-spectrum beam

Paraxial phase and longitudinal-field bounds

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$

The complex exponential by its power series

Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive

Facts & Assumptions

Given: The scalar propagators and Fourier convention of the angular-spectrum Definition; countable choice as assumed by its $L^{2}$ Plancherel supplier.

[F1]

The exact and paraxial Fourier multipliers are respectively $e^{i z k_{0} \sqrt{1 - s}}$ and $e^{i z k_{0} (1 - s / 2)}$ , where $s = ∣ 2 π ξ ∣^{2} / k_{0}^{2}$ . Forward angular-spectrum beam

[F2]

The exact remainder is $R (s) = s^{2} / [4 (1 - s / 2 + \sqrt{1 - s})]$ , and for real phases $a, b$ the local lemma gives $∣ e^{i a} - e^{i b} ∣ \leq ∣ a - b ∣$ . Uniform phase-multiplier bound for the square-root dispersion law

[F3]

The Fourier transform $F_{2}$ is unitary on complex $L^{2}$ under countable choice. Plancherel theorem The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F4]

Under countable choice, each nondegenerate box has Lebesgue measure equal to the product of its side lengths. A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included Axis-parallel rectangles in $R^{m}$ and their volume The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F5]

The complex exponential addition law holds; its power-series definition gives $e^{0} = 1$ . The Cartesian/modulus corollary states $∣ e^{i t} ∣ = e^{0}$ for real $t$ , so $∣ e^{i t} ∣ = 1$ ; it also gives Euler's identity $e^{i π} = - 1$ . Consequently, for $Δ \in R$ , $∣ e^{- i Δ} - 1 ∣ = ∣ e^{i Δ} - 1 ∣ .$ Indeed, the addition law gives $e^{- i Δ} e^{i Δ} = e^{0} = 1$ , so $e^{- i Δ} - 1 = e^{- i Δ} (1 - e^{i Δ})$ ; modulus multiplicativity and $∣ e^{- i Δ} ∣ = 1$ give the identity. For any real $b$ , the addition law also gives $e^{i (b - Δ)} - e^{i b} = e^{i b} (e^{- i Δ} - 1)$ , so the modulus of this phase-multiplier difference is $∣ e^{i Δ} - 1 ∣$ . $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive

[F6]

The A-page estimate is proportional to the scaled distance $∣ z ∣ k_{0} δ^{4}$ ; it makes no convergence claim when that quantity is fixed and nonzero. Paraxial phase and longitudinal-field bounds

[F7]

Complex modulus is subadditive and multiplicative. For $u, v \in C$ , $∣ u ∣ \leq ∣ u - v ∣ + ∣ v ∣$ and $∣ v ∣ \leq ∣ v - u ∣ + ∣ u ∣ = ∣ u - v ∣ + ∣ u ∣$ , so $∣ ∣ u ∣ - ∣ v ∣ ∣ \leq ∣ u - v ∣$ ; the equality $∣ v - u ∣ = ∣ u - v ∣$ follows from $v - u = - (u - v)$ , multiplicativity, and $∣ - 1 ∣ = 1$ from the modulus definition. Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive

Counterexample

Given: Fix $k_{0} > 0$ and choose one constant spectral norm $A_{⋆} > 0$ (in volts for scalar fields measured in $V m^{- 1}$ ).

1.1givenF4algebra

Set $δ_{n} : = 1 / (n + 2)$ and $R_{n} : = δ_{n} k_{0} / (2 π)$ . Let $Ξ_{n} : = [R_{n} (1 - δ_{n} / 4), R_{n} (1 - δ_{n} / 8)] \times [0, R_{n} δ_{n} / 8]$ . Its side lengths are both $R_{n} δ_{n} / 8 > 0$ , so [F4] gives $0 < ∣ Ξ_{n} ∣ = R_{n}^{2} δ_{n}^{2} / 64 < \infty$ . Define ${\hat{u}}_{0, n} : = A_{⋆} ∣ Ξ_{n} ∣^{- 1 / 2} 1_{Ξ_{n}}$ ; then $∥ {\hat{u}}_{0, n} ∥_{2} = A_{⋆}$ . For $q = 2 π ξ$ with $ξ \in Ξ_{n}$ , $q_{x} \geq δ_{n} k_{0} (1 - δ_{n} / 4) > δ_{n} k_{0} (1 - δ_{n})$ and $∣ q ∣^{2} \leq δ_{n}^{2} k_{0}^{2} [(1 - δ_{n} / 8)^{2} + (δ_{n} / 8)^{2}] \leq δ_{n}^{2} k_{0}^{2}$ ; hence this nonzero spectrum lies in the angular cone and concentrates near its outer radius.

2.1step 1.1F3F6algebra

Let $u_{0, n} : = F_{2}^{- 1} {\hat{u}}_{0, n}$ and $z_{n} : = 8 π / (k_{0} δ_{n}^{4}) > 0$ . This fixes the scale in [F6] at $8 π$ . By [F3], $∥ u_{0, n} ∥_{2} = A_{⋆}$ , so each input is nonzero and admissible for the refuted statement.

2.2step 1.1F2algebra

For $ξ \in Ξ_{n}$ , put $s_{n} : = ∣ 2 π ξ ∣^{2} / k_{0}^{2}$ . Step 1.1 gives $(1 - δ_{n} / 4)^{2} \leq s_{n} / δ_{n}^{2} \leq 1$ , so this ratio tends to $1$ uniformly on $Ξ_{n}$ . Also $0 \leq s_{n} \leq δ_{n}^{2}$ , and $∣ 1 - \sqrt{1 - s_{n}} ∣ = s_{n} / (1 + \sqrt{1 - s_{n}}) \leq s_{n}$ , so $1 - s_{n} / 2 + \sqrt{1 - s_{n}} \to 2$ uniformly. By [F2], the relative phase difference is $Δ_{n} : = z_{n} k_{0} R (s_{n}) = 2 π (s_{n} / δ_{n}^{2})^{2} / (1 - s_{n} / 2 + \sqrt{1 - s_{n}})$ , which tends uniformly to $π$ .

3.1step 2.2F2F5F7algebra

The actual exact-minus-paraxial phase is $- Δ_{n}$ , so [F5] makes the modulus of the multiplier difference $∣ e^{i Δ_{n}} - 1 ∣$ . Put $u = e^{i Δ_{n}} - 1$ and $v = e^{i π} - 1$ . By [F7], $∣ ∣ u ∣ - ∣ v ∣ ∣ \leq ∣ u - v ∣$ ; [F5] gives $∣ v ∣ = 2$ , and [F2] gives $∣ u - v ∣ = ∣ e^{i Δ_{n}} - e^{i π} ∣ \leq ∣ Δ_{n} - π ∣ \to 0$ uniformly on $Ξ_{n}$ . Thus the multiplier-difference modulus tends uniformly to $2$ .

4.1step 1.1step 2.1step 3.1F1F3algebra∎

By [F3], the squared relative $L^{2}$ error is the average of $∣ e^{i Δ_{n}} - 1 ∣^{2}$ over $Ξ_{n}$ with respect to normalized Lebesgue measure. Since step 3.1 gives uniform convergence of that modulus to $2$ , the averages of its square tend to $4$ ; the relative errors are nonnegative, so they tend to $2$ , not $0$ . This contradicts the Statement refuted and proves the claimed counterexample.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)Open item page →

An oblique plane wave with a nonzero longitudinal electric component

Physical scope

Exact plane-wave example in the smooth, source-free vacuum Maxwell model and the propagating cone of the ideal angular-spectrum model. It illustrates the longitudinal component required by Maxwell's equations for its specified transverse polarization; it asserts no measured field, focal apparatus, or torque.

Example

Let $0 < κ \leq δ k_{0}$ , $q = (κ, 0)$ , $k_{z} : = \sqrt{k_{0}^{2} - κ^{2}}$ , and choose a real $E_{0} \neq 0$ in $V m^{- 1}$ . Put $e : = (E_{0}, 0, - κ E_{0} / k_{z}), b : = (0, \frac{k_{0}^{2} E_{0}}{ω k_{z}}, 0), ϕ (x, t) : = κ x + k_{z} z - ω t .$ The real fields $E (x, t) : = Re (e e^{i ϕ (x, t)})$ and $B (x, t) : = Re (b e^{i ϕ (x, t)})$ are an exact, forward, source-free vacuum plane-wave mode. In particular, $e_{z} = - \frac{κ E_{0}}{\sqrt{k_{0}^{2} - κ^{2}}} \neq 0, \frac{∣ e_{z} ∣}{∣ E_{0} ∣} = \frac{κ}{\sqrt{k_{0}^{2} - κ^{2}}} \leq \frac{δ}{\sqrt{1 - δ^{2}}} .$ Thus setting $e_{z} = 0$ while keeping this transverse amplitude would not give an exact Maxwell mode.

Example references

Forward angular-spectrum beam

Paraxial phase and longitudinal-field bounds

Facts & Assumptions

Given: A fixed SI laboratory chart, $c > 0$ , $ω > 0$ , $k_{0} = ω / c$ , $0 < δ < 1$ , $0 < κ \leq δ k_{0}$ , and real $E_{0} \neq 0$ in $V m^{- 1}$ .

[F1]

The SI chart has spatial coordinates in metres and time in seconds, $k_{0} = ω / c$ , and $E$ and $B$ have units $V m^{- 1}$ and tesla. The electric and magnetic fields as fixed-time spatial vector fields 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 Forward angular-spectrum beam

[F2]

The plane-wave convention uses the real part of complex amplitudes times $e^{i (K \cdot x - ω t)}$ . Complex plane-wave fields: real parts of complex exponentials

[A1]

The adopted smooth source-free vacuum Maxwell equations, with $ρ = 0$ and $J = 0$ , are $div E = div B = 0$ , $curl E = - \partial_{t} B$ , and $curl B = c^{- 2} \partial_{t} E$ ; $ρ$ and $J$ are the charge and current densities of the source definition, and divergence and curl are the coordinate operators of the fixed spatial chart. The microscopic vacuum Maxwell equations: smooth and weak branches Charge parameter, frame charge and current densities, volume charge and flux, and the four-current Divergence and curl of a $C^{1}$ vector field

[F3]

The complex exponential satisfies $\exp^{'} = \exp$ and the chain rule; real parts commute with these real partial derivatives. The plane-wave fields are therefore $C^{1}$ . Use the Euclidean dot and cross products on the spatial vectors. Complex plane-wave fields: real parts of complex exponentials The complex exponential is entire and its complex derivative is itself The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ The cross product in $R^{3}$

[F4]

For an exact mode with these $q, k_{z}$ , the longitudinal relation and cone bound are as stated in the paraxial error theorem. Paraxial phase and longitudinal-field bounds

Verification

1.1givenF1algebra

Since $κ \leq δ k_{0} < k_{0}$ , $k_{z} = \sqrt{k_{0}^{2} - κ^{2}}$ is positive. The definitions give $κ^{2} + k_{z}^{2} = k_{0}^{2}$ , $κ E_{0} + k_{z} e_{z} = 0$ , and $ω b_{y} = k_{0}^{2} E_{0} / k_{z}$ . Thus $K = (κ, 0, k_{z})$ is a forward wavevector of length $k_{0}$ , and $e$ is transverse to it.

2.1step 1.1F1F2F3A1algebra

By [F3], for each spatial coordinate $x_{j}$ , $\partial_{x_{j}} E = Re (i K_{j} e e^{i ϕ})$ componentwise, and $\partial_{t} E = Re (- i ω e e^{i ϕ})$ ; the same formulas hold with $B, b$ in place of $E, e$ . From [step 1.1], $K \cdot e = κ E_{0} + k_{z} e_{z} = 0, K \cdot b = 0,$ $K \times e = (0, k_{z} E_{0} - κ e_{z}, 0) = (0, \frac{k_{0}^{2} E_{0}}{k_{z}}, 0) = ω b,$ and $K \times b = (- k_{z} b_{y}, 0, κ b_{y}) = (- \frac{k_{0}^{2} E_{0}}{ω}, 0, \frac{κ k_{0}^{2} E_{0}}{ω k_{z}}) = - \frac{ω}{c^{2}} e,$ where the last equality uses $k_{0} = ω / c$ . Summing the spatial derivatives therefore yields $div E = Re (i (K \cdot e) e^{i ϕ}) = 0, div B = Re (i (K \cdot b) e^{i ϕ}) = 0,$ $curl E = Re (i (K \times e) e^{i ϕ}) = - \partial_{t} B, curl B = Re (i (K \times b) e^{i ϕ}) = c^{- 2} \partial_{t} E .$ Thus all four source-free Maxwell equations in [A1] hold pointwise, so these real fields are an exact mode.

3.1givenstep 1.1F4algebra∎

The constructed transverse amplitude is $(E_{0}, 0)$ . Applying [F4] gives $e_{z} = - q \cdot e_{⊥} / k_{z} = - κ E_{0} / k_{z}$ and $∣ e_{z} ∣ / ∣ E_{0} ∣ \leq δ / \sqrt{1 - δ^{2}}$ . Since $κ > 0$ , $E_{0} \neq 0$ , and $k_{z} > 0$ , $e_{z} \neq 0$ . Hence the alternative $e_{z} = 0$ with this same transverse amplitude is incompatible with source-free Maxwell transversality.

Remarks

For the illustrative case $δ = 3 / 4$ and $κ / k_{0} = 1 / 2$ , the normalized x-z projections are $K / k_{0} = (1 / 2, \sqrt{3} / 2)$ and $e / E_{0} = (1, - 1 / \sqrt{3})$ ; their dot product is zero. The arrows use these separate dimensionless normalizations, and the figure is schematic only. The Maxwell verification is the component proof in step 2.1, not the drawing.

\begin{tikzpicture}[x=2.5cm,y=2cm,>=stealth]
  \draw[->] (-0.12,0) -- (1.25,0) node[right] {$x$ component};
  \draw[->] (0,-0.8) -- (0,1.15) node[above] {$z$ component};
  \draw[dashed,gray] (0,0) -- (0.5,0);
  \draw[dashed,gray] (0.5,0) -- (0.5,{sqrt(3)/2});
  \draw[very thick,->] (0,0) -- (0.5,{sqrt(3)/2})
    node[above right] {$\mathbf K/k_0$};
  \draw[very thick,->,blue] (0,0) -- (1,{-1/sqrt(3)})
    node[below right] {$\mathbf e/E_0$};
  \node[below] at (0.5,0) {$\kappa/k_0=1/2$};
  \node[right] at (0.5,0.53) {$k_z/k_0=\sqrt3/2$};
\end{tikzpicture}

5 · Examples, experiments and counterexamples

None yet.

Angular-spectrum optics and controlled paraxial limits — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

A small angular cone can accumulate order-one phase error

Statement refuted

Statement references

Facts & Assumptions

Counterexample

An oblique plane wave with a nonzero longitudinal electric component

Example

Example references

Facts & Assumptions

Verification

Remarks

5 · Examples, experiments and counterexamples

Sources