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.
Volume integral scattering and partial wave error — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Approximation and Compactness in C(K)
- Areas of Elementary Plane Figures
- Banach Valued Integration and the Radon Nikodym Property
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compact Operators and Riesz Schauder Theory
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Coordinate and Path Transport
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Lp Spaces and Test-Function Conventions
- Complex Norms and Realification
- Complex Subspace Realification
- Complexification, Realification and Real Structures
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces Adjoint Operators and Annihilators
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Euclidean Surface Measure, Divergence, and Green Identities
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Geometric Hahn Banach and Convex Separation
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Hausdorff via the Diagonal
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measure-Preserving Systems and Mixing Criteria
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Orthonormal Bases, Parseval and Fourier Series
- Outer Measure and the Caratheodory Extension Theorem
- Outward rounded interval and ball arithmetic
- Partitions of Unity and Paracompactness
- pi: the Equivalent Characterizations
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Radon Measures and the Riesz Markov Kakutani Theorem
- Regular Surfaces and Surface Integrals
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Smooth Partitions of Unity and Exhaustions
- Stable special function recurrences and certified evaluation
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Analytic Hahn Banach Theorem
- The Baire Principles of Functional Analysis
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Divergence Theorem and Classical Stokes
- The Exponential Function
- The Fundamental Theorems of Calculus
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Urysohn's Lemma and the Tietze Extension Theorem
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Volume integral scattering and partial wave error
- Volumes of Elementary Solids and Solids of Revolution
- Weak Mixing and the Chacon Transformation
2 · Summary
These examples give a strict small-norm ball bound with an explicit Born tail, an exact conditional amplification factor for a near-unit eigenmode, exact zeroth-mode matching for a radial square well, and a forward-direction witness showing why a fixed angular cutoff fails for high-frequency plane waves. The eigenmode and exact square-well conclusions remain conditional calculations. For supplied positive-real parameter enclosure interfaces, the square-well verification additionally constructs the two generally non-dyadic spherical arguments and certifies the matching coefficients to any positive rational absolute tolerance using sufficiently large finite caps. Zero-containing coefficient enclosures carry no relative certificate. No physical resonance is asserted.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A fixed partial-wave cutoff misses the forward high-frequency plane wave
Example
Assume Countable Choice and Dependent Choice. For a fixed direction , consider the incident plane wave on the unit sphere. Let denote projection onto degrees . For each fixed , its value at the forward direction tends to zero as , whereas has modulus one. Thus a fixed angular cutoff has forward error tending to one; uniform high-frequency accuracy below one requires the cutoff to tend to infinity.
Verification
Given: , , and integer .
[F1] The addition kernel for degree is . Expanding the finite orthogonal projection in an orthonormal basis gives its kernel , so (Spherical harmonics form a complete basis with the addition formula).
[F2] In the coordinates , the map is a diffeomorphism from onto the open unit ball with its meridional half-plane removed, and . The omitted half-plane is null by the singular clause of the linear change-of-variables theorem. The change-of-variables theorem and the radial-cone definition of therefore give on this chart. Rotations preserve because they preserve radial cones and have determinant one (The polar surface set function on the unit sphere, Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions, A linear map of sends Lebesgue measurable sets to Lebesgue measurable sets, with when is invertible and Lebesgue null when it is not). Choosing a rotation taking to the north pole yields for every continuous .
[F3] For real , the complex derivative theorem gives ; this follows from the difference quotient with complex increment (The complex exponential is entire and its complex derivative is itself).
[F4] For real , (, , and ).
By [F1] and [F2], . For a fixed polynomial , integration by parts gives . Summing finitely many terms yields for a finite constant independent of .
Since , step 1.1 and the reverse triangle inequality give . If integer cutoffs failed to tend to infinity as , there would be and a sequence with ; the finite maximum would give the same lower bound along that sequence. Thus a cutoff with uniform error bounded by any fixed for all sufficiently large must satisfy .
A small-norm ball scatterer has a certified Born tail
Example
Assume Countable Choice. Take , constant contrast , real , and arbitrary . The general kernel estimate gives , so the Born series converges and its 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 and diameter (A closed three-dimensional ball of radius has volume ).
[F2] For the three-dimensional kernel, (The three-dimensional free-space scattering kernel is square integrable).
[F3] If , the equation has a unique solution and Born tail (Born truncation error for a small-norm volume integral operator).
Substituting , , and into [F2] gives .
Set . Step 1.1 gives , so [F3] applies and yields a unique solution and . The last inequality follows termwise from , which is increasing on .
A near-unit volume-operator mode amplifies forcing error
Example
Conditionally suppose a compact volume operator has a normalized eigenmode with eigenvalue , and suppose is injective. The Fredholm branch then applies. Forcing along is amplified by exactly ; this example does not claim that every physical contrast has such an eigenvalue.
Verification
Given: AC, the compact volume operator , injectivity of , and with and .
[F1] AC, compactness of , and injectivity of give a unique solution for each forcing and a bounded inverse (Fredholm solvability and residual stability for volume scattering).
[F2] The compactness hypothesis is supplied for the model by The volume integral scattering operator is compact.
By [F2], the model operator is compact; together with the assumed injectivity and , the Fredholm result [F1] applies. The vector satisfies . Uniqueness from [F1] identifies this with the solution for forcing , so .
For perturbed forcing , linearity and the same eigenvector calculation give . Therefore , while . As approaches through values unequal to , this exact amplification factor grows without bound; the eigenpair remains a conditional hypothesis.
Exact matching for the radial square well in the zeroth partial wave
Example
Assume Countable Choice and Dependent Choice. Let on , let , and put . In the reduced radial channel with incident regular mode , write the regular interior solution as and the exterior total mode as . Exact continuity of the value and derivative determines and below.
Verification
Given: Countable Choice, Dependent Choice, , and the matching statement of Radial volume scattering separates into matched partial-wave boundary problems.
[F1] For a constant radial contrast , the reduced equation is inside and outside; matching requires continuous (Radial volume scattering separates into matched partial-wave boundary problems).
[F2] The outgoing zeroth spherical Hankel function is , so a constant multiple of is a constant multiple of (Spherical Bessel and outgoing Hankel function conventions).
[F3] Soundness and eventual absolute precision for spherical Bessel enclosures and Scaled spherical Bessel evaluation on positive real arguments: positive represented real arguments admit containing enclosures for spherical values and their first argument derivatives at any positive rational absolute tolerance when sufficiently large finite caps are supplied. Fixed capped calls may return inconclusive instead; a zero-containing output has no relative certificate.
By [F1], the regular interior mode has form ; the exterior mode stated in the Example is the free regular incident mode plus the outgoing mode by [F2]. At , continuity of value gives .
For numerical comparison only, suppose additionally that are supplied by terminating dyadic enclosure interfaces whose widths on request are at most . Their exact values retain the unrestricted real domain in the Example. To supply either composed argument on a width request , scan , request all three parameter boxes at , and skip until they have positive lower endpoints. Denote them by and form the positive dyadic radicand box . Choose an integer with , by scanning positive integers. For each endpoint , start with and perform bisections: a dyadic midpoint replaces the lower endpoint if , and otherwise replaces the upper endpoint. The bracket always contains and its width is . Use the lower endpoint of the bracket and upper endpoint of the bracket to form . Form and , and return the requested one when its lower endpoint is positive and its width is at most ; otherwise continue the scan. Every operation before a scan increment is finite. The parameter boxes are eventually bounded and bounded away from zero, so is eventually bounded. Also , and . Interval product widths tend to zero by boundedness and the product-width inequality. Thus both returned intervals eventually have positive lower endpoints and the required width; every requested scan terminates. They contain exactly and , which need not be dyadic.
Continuity of derivative gives . Substitute step 1.1 and rearrange to obtain .
The denominator has squared modulus , because and sine and cosine cannot both vanish. Hence and . If , then , these formulas reduce to and , the unscattered solution.
For , the degree-zero definitions and their first derivatives give , and . At stage , use step 1.2 to enclose the arguments and parameters with widths at most ; invoke [F3] at the two represented arguments with absolute tolerance , setting all four evaluator caps successively to until each call succeeds. For this fixed the sufficient-cap assertion in [F3] proves that each search terminates. Reconstruct these elementary values by exact interval operations, enclose by dividing the enclosure by the positive enclosure, and use complex conjugation for . The exact denominator satisfies , since and . The shrinking enclosures therefore eventually exclude zero for and . Enclose as only when its real denominator interval has positive lower endpoint; the same shrinking-width argument eventually certifies this condition. Then the formulas in step 3.1 give containing rectangles for with widths tending to zero, because sums and products of bounded shrinking intervals shrink and these divisions have denominators bounded away from zero. Round the final coefficient endpoints outward to the dyadic grid , which adds at most to each component width and preserves containment. Consequently scanning until any specified positive rational absolute-radius tests pass terminates, although a prescribed finite cap can instead return inconclusive. This procedure proves a certified numerical comparison for represented parameters without altering the exact matching formulas for arbitrary positive real parameters. No relative accuracy for is asserted when , including the unscattered case.
Sources
- Pierre Capel, Introduction to Scattering Theory, TALENT lecture notes
- Maximilian Kreuzer, Quantum Theory: Lecture Notes, version July 15, 2009, Chapter 8
- Otmar Scherzer and Leonidas Mindrinos, Inverse Problems: Lecture Notes, Sommersemester 2015, Chapter 5, §5.2.6
- Habib Ammari, Brian Fitzpatrick, and Sanghyeon Yu, Mathematical and Computational Methods in Photonics: Tutorial Notes, §1.3
- Andreas Neubauer and Ronny Ramlau, Lecture Notes: Integral Equations and Boundary Value Problems, §3.3