Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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 (ACω)). Let c=1, u0=0 and choose a nonnegative u1∈Cc∞(B1/2(0)) with ∫u1>0, for example the bump equal to one on B‾1/4(0) supplied by A smooth bump between concentric Euclidean balls. Fix x=0 and t=1: the support of u1 is strictly inside the disk B1(0), and it is disjoint from the sphere ∂B1(0). Poisson's formula of Poisson's formula in two dimensions by descent gives u(0,1)=12π∫B1(0)u1(y)1−∣y∣2 dy>0, because the weight is strictly positive on the interior and u1≥0 is positive on a set of positive measure. Thus the value at time t=1 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, c=1, u0=0, and a nonnegative smooth compactly supported datum u1∈Cc∞(B1/2(0)) with ∫u1>0.

[F1]

Poisson's formula for c=1, u0=0 reads u(x,t)=12π∫Bt(x)u1(y)(t2−∣y−x∣2)−1/2dy for t>0 (Poisson's formula in two dimensions by descent with Wu1(x,t)=12π∫Bt(x)u1(y)(t2−∣y−x∣2)−1/2dy by Spherical means and the weighted ball integral of space-dependent data).

[F2]

The odd-dimensional evaluation depends on the data through a neighbourhood of the sphere ∂Bct(x), while in even dimensions data supported strictly inside the ball contribute (Sphere-supported versus interior-supported free wave kernels).

Verification

1.1F1algebra

At x=0, t=1, [F1] gives u(0,1)=12π∫B1(0)u1(y)(1−∣y∣2)−1/2dy. The integrand is nonnegative, the weight (1−∣y∣2)−1/2 is strictly positive and bounded below by 1 (and above by 2/3) on the support B1/2(0) of u1, and u1 is positive on a set of positive measure; hence the integral is strictly positive.

2.1F2given∎

The support of u1 lies strictly inside B1(0) and is disjoint from ∂B1(0), so the value u(0,1) is produced by data at distance at most 1/2 from the origin, strictly behind the wavefront of radius 1; by [F2] this is exactly the two-dimensional interior tail, in contrast with the (n≥3) odd-dimensional evaluation, which reads the data near the sphere.

Depends on

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