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.

Constant initial velocity in three dimensions

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $c > 0$ , let $u_{1} \equiv v_{0} \in R$ and $u_{0} \equiv g_{0} \in R$ be constant. Then the Kirchhoff expression of Kirchhoff's formula in three dimensions is $u (x, t) = \frac{\partial}{\partial t} [t g_{0}] + t v_{0} = g_{0} + t v_{0},$ since a constant has spherical mean itself. This satisfies $u_{t t} = 0 = c^{2} Δ u$ , $u (\cdot, 0) = g_{0}$ and $u_{t} (\cdot, 0) = v_{0}$ , and the spherical means $M_{g_{0}} \equiv g_{0}$ , $M_{v_{0}} \equiv v_{0}$ use the normalisation $\frac{1}{4 π} \int_{S^{2}} d σ = 1$ of Spherical means and the weighted ball integral of space-dependent data. Replacing the average by an unnormalised integral of the data over the sphere would multiply by $4 π c^{2} t^{2}$ , so the check pins the factor in the constant.

Facts & Assumptions

Given: Countable Choice, $c > 0$ , constants $g_{0}, v_{0} \in R$ , and the means $M_{g_{0}}$ , $M_{v_{0}}$ .

[F1]

The spherical mean of a constant $g_{0}$ is $M_{g_{0}} (x, r) = g_{0}$ for every $x, r$ , because the defining integral is normalised by $ω_{2} = σ (S^{2})$ , and likewise for $v_{0}$ (Spherical means and the weighted ball integral of space-dependent data).

[F2]

The Kirchhoff expression defines a $C^{2}$ solution of $u_{t t} = c^{2} Δ u$ on $R^{3} \times (0, \infty)$ (Kirchhoff's formula in three dimensions).

[F3]

The Kirchhoff expression attains its data in the limit sense (The dimension formulas attain the Cauchy data); uniqueness in the class of $C^{2}$ solutions is left to the energy statement of the wave-energy page.

Verification

1.1F1F2algebra

Means and expression. By [F1] the means are constant, $M_{g_{0}} \equiv g_{0}$ and $M_{v_{0}} \equiv v_{0}$ , so the Kirchhoff expression becomes $\partial_{t} [t g_{0}] + t v_{0} = g_{0} + t v_{0}$ ; this is $C^{\infty}$ , satisfies $\partial_{t}^{2} u = 0 = c^{2} Δ u$ and has the prescribed values $u (\cdot, 0) = g_{0}$ , $\partial_{t} u (\cdot, 0) = v_{0}$ .

2.1F1F3algebra∎

Normalisation check. A constant has mean itself on the sphere, so any unnormalised sphere integral $\int_{\partial B_{c t} (x)} u_{0} d S$ would equal $4 π c^{2} t^{2}$ times the mean for $u_{0}$ constant on the sphere of radius $c t$ ; the constant-data check therefore detects exactly that factor, confirming the normalisation $1 / (4 π)$ in the Kirchhoff expression.

Depends on

Used by

Replacing the sphere measure by the ball measure in Kirchhoff's formula Counterexample

Dependency tree · two levels

37 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)