Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass
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 pulse has a tail inside the cone

Example

Assume the Axiom of Countable Choice. Let c>0, x0∈R2, r>0, and let u1∈Cc2(R2) be nonnegative and not identically zero with support in Br(x0); let u be the Poisson solution with data (0,u1) (Poisson's formula in two dimensions by descent). Then for every t>r/c

u(x0,t)=12πc∫Bct(x0)u1(y)c2t2−∣y−x0∣2 dy>0.

The centre of the forward cone keeps seeing the pulse after the front has passed: the two-dimensional pulse has a tail inside the cone, in contrast with the quiet three-dimensional interior of A three-dimensional spherical pulse leaves a quiet interior.

Facts & Assumptions

Given: ACω; c>0, x0∈R2, r>0, and a nonnegative u1∈Cc2(R2), u1≢0, supported in Br(x0); the Poisson solution u with data (0,u1).

[F1]

Poisson's formula for data (0,u1): u(x,t)=12πc∫Bct(x)(c2t2−∣y−x∣2)−1/2u1(y) dy for t>0. (Poisson's formula in two dimensions by descent)

[F2]

In dimension two, strong Huygens fails: admissible data supported strictly inside the base disk Bct(x) can affect the value u(x,t) at its vertex. (Wave tails in one and even spatial dimensions: strong Huygens fails)

[F3]

The nonnegative integral is monotone and positively homogeneous, and has value zero exactly for a function vanishing almost everywhere. A continuous function positive at a point is bounded below by a positive constant on a smaller ball, whose measure is positive. (Monotonicity and nonnegative homogeneity of the nonnegative integral, A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere, Sphere and ball measures scale in Rn)

Verification

1.1givenF1algebra

The value at the centre: setting x=x0 in [F1] gives the displayed formula u(x0,t)=12πc∫Bct(x0)(c2t2−∣y−x0∣2)−1/2u1(y) dy, the integrand being defined and continuous on the open disk because ∣y−x0∣<ct there.

2.1givenstep 1.1F3algebra

Positivity: if t>r/c then B‾r(x0)⊆Bct(x0), and on that closed support ball ∣y−x0∣≤r<ct gives c2t2−∣y−x0∣2≤ct, hence the weight (c2t2−∣y−x0∣2)−1/2≥1/(ct)>0. Since u1≥0 is continuous and nonzero, it is positive on a nonempty open subset of Br(x0), so [F3] gives ∫Bct(x0)u1(y) dy>0 and the displayed integral is at least (2πc)−1(ct)−1∫Bct(x0)u1(y) dy>0; this shows that the centre still sees a positive displacement at every time after the front ∣x−x0∣=ct has passed beyond the support, that is, for t>r/c.

3.1givenstep 2.1F2∎

The tail is carried by the interior: for t>r/c the data are supported strictly inside Bct(x0) and vanish near its boundary, yet step 2.1 gives u(x0,t)>0. This is the interior tail and illustrates the failure of sphere-only dependence in [F2].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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