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 two-dimensional interior tail
Example
Assume the Axiom of Countable Choice (The Axiom of Countable Choice ()). Let , and choose a nonnegative with , for example the bump equal to one on supplied by A smooth bump between concentric Euclidean balls. Fix and : the support of is strictly inside the disk , and it is disjoint from the sphere . Poisson's formula of Poisson's formula in two dimensions by descent gives because the weight is strictly positive on the interior and is positive on a set of positive measure. Thus the value at time is affected by data strictly inside the wavefront: the two-dimensional solution has an interior tail, in contrast to the three-dimensional evaluation depending on data near the sphere only, as recorded in Sphere-supported versus interior-supported free wave kernels.
Facts & Assumptions
Given: Countable Choice, , , and a nonnegative smooth compactly supported datum with .
Poisson's formula for , reads for (Poisson's formula in two dimensions by descent with by Spherical means and the weighted ball integral of space-dependent data).
The odd-dimensional evaluation depends on the data through a neighbourhood of the sphere , while in even dimensions data supported strictly inside the ball contribute (Sphere-supported versus interior-supported free wave kernels).
Verification
At , , [F1] gives . The integrand is nonnegative, the weight is strictly positive and bounded below by (and above by ) on the support of , and is positive on a set of positive measure; hence the integral is strictly positive.
The support of lies strictly inside and is disjoint from , so the value is produced by data at distance at most from the origin, strictly behind the wavefront of radius ; by [F2] this is exactly the two-dimensional interior tail, in contrast with the odd-dimensional evaluation, which reads the data near the sphere.
Depends on
- Poisson's formula in two dimensions by descent
- The dimension formulas attain the Cauchy data
- Spherical means and the weighted ball integral of space-dependent data
- Sphere-supported versus interior-supported free wave kernels
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- A smooth bump between concentric Euclidean balls
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
38 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
- Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)
- Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)