ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-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.

A small-norm ball scatterer has a certified Born tail

Example

Assume Countable Choice. Take $D = B (0, 1) \subset R^{3}$ , constant contrast $q = 1 / 2$ , real $k$ , and arbitrary $f \in L^{2} (D)$ . The general kernel estimate gives $∥ K_{k} ∥ \leq 1 / \sqrt{6} < 1$ , so the Born series converges and its $m$ th partial sum has an explicit geometric error bound.

Verification

Given: Countable Choice, the ball, contrast and volume operator from The three-dimensional volume integral scattering model.

[F1] The ball has volume $4 π / 3$ and diameter $2$ (A closed three-dimensional ball of radius $r \geq 0$ has volume $4 π r^{3} / 3$ ).

[F2] For the three-dimensional kernel, $∥ K_{k} ∥ \leq ∥ q ∥_{\infty} \sqrt{∣ D ∣ diam (D) / (4 π)}$ (The three-dimensional free-space scattering kernel is square integrable).

[F3] If $∥ K_{k} ∥ = ρ < 1$ , the equation has a unique solution and Born tail $∥ u - \sum_{j = 0}^{m} K_{k}^{j} f ∥_{2} \leq ρ^{m + 1} ∥ f ∥_{2} / (1 - ρ)$ (Born truncation error for a small-norm volume integral operator).

1.1F1F2algebra

Substituting $∣ D ∣ = 4 π / 3$ , $diam (D) = 2$ , and $∥ q ∥_{\infty} = 1 / 2$ into [F2] gives $∥ K_{k} ∥ \leq (1 / 2) \sqrt{(4 π / 3) 2 / (4 π)} = 1 / \sqrt{6} < 1$ .

2.1F3step 1.1algebra∎

Set $ρ = ∥ K_{k} ∥$ . Step 1.1 gives $0 \leq ρ \leq 1 / \sqrt{6} < 1$ , so [F3] applies and yields a unique solution and ${∥ u - \sum_{j = 0}^{m} K_{k}^{j} f ∥}_{2} \leq \frac{ρ^{m + 1}}{1 - ρ} ∥ f ∥_{2} \leq \frac{(1 / \sqrt{6})^{m + 1}}{1 - 1 / \sqrt{6}} ∥ f ∥_{2}$ . The last inequality follows termwise from $ρ^{m + 1} / (1 - ρ) = \sum_{n = m + 1}^{\infty} ρ^{n}$ , which is increasing on $[0, 1)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 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

Otmar Scherzer and Leonidas Mindrinos, Inverse Problems: Lecture Notes, Sommersemester 2015, Chapter 5, §5.2.6 (standard reference, not scraped)
Habib Ammari, Brian Fitzpatrick, and Sanghyeon Yu, Mathematical and Computational Methods in Photonics: Tutorial Notes, §1.3 (standard reference, not scraped)