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 point source produces a uniform expanding sphere

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $c > 0$ and fix $t > 0$ . Choose a nonnegative $ρ \in C_{c}^{\infty} (B_{1} (0))$ with $\int ρ = 1$ (normalise a nonnegative bump from A smooth bump between concentric Euclidean balls), and put $ρ_{ε} (y) : = ε^{- 3} ρ (y / ε)$ . Then $ρ_{ε}$ is a smooth unit-mass velocity datum supported in $B_{ε} (0)$ , and the Kirchhoff solution with $u_{0} = 0$ is $u_{ε} (x, t) = t M_{ρ_{ε}} (x, c t)$ . As $ε ↓ 0$ , for every continuous test function $φ$ , $\int_{R^{3}} φ (x) u_{ε} (x, t) d x ⟶ t \frac{1}{4 π} \int_{S^{2}} φ (c t ω) d σ (ω),$ so the limiting mass spreads uniformly over the sphere of radius $c t$ : the point source at the origin produces, at time $t$ , the uniform probability measure on the expanding sphere, scaled by $t$ . Equivalently the limiting surface density is $t / (4 π c^{2} t^{2})$ per unit area, whose total against the area $4 π c^{2} t^{2}$ is $t$ .

Facts & Assumptions

Given: Countable Choice, $c > 0$ , $t > 0$ , a nonnegative $ρ \in C_{c}^{\infty} (B_{1} (0))$ with unit integral, the rescaled datum $ρ_{ε} (y) = ε^{- 3} ρ (y / ε)$ , and a continuous test function $φ$ .

[F1]

With $u_{0} = 0$ the Kirchhoff solution is $u_{ε} (x, t) = t M_{ρ_{ε}} (x, c t)$ , a $C^{2}$ solution attaining the data (Kirchhoff's formula in three dimensions, The dimension formulas attain the Cauchy data).

[F2]

The spherical mean is the normalised sphere integral, $M_{ρ_{ε}} (x, c t) = \frac{1}{4 π c^{2} t^{2}} \int_{\partial B_{c t} (x)} ρ_{ε} (y) d S (y)$ (Spherical means and the weighted ball integral of space-dependent data, Sphere and ball measures scale in Rn with $ω_{2} = 4 π$ ).

[F3]

For integrable $F$ on the product of a compact set with $R^{3}$ , the order of integration may be interchanged (Fubini's theorem for L^1 functions on a sigma-finite product).

[F4]

The map $Ψ (y) : = \int_{\partial B_{c t} (y)} φ d S$ is continuous near $0$ : parameterizing it as $(c t)^{2} \int_{S^{2}} φ (y + c t ω) d σ (ω)$ , uniform continuity of $φ$ on a compact ball gives continuity. Also $\int ρ_{ε} = 1$ by linear change of variables and $∣ \int ρ_{ε} (y) Ψ (y) d y - Ψ (0) ∣ \leq \sup_{∣ y ∣ \leq ε} ∣ Ψ (y) - Ψ (0) ∣ \to 0$ ; the sphere scaling at $y = 0$ is Sphere and ball measures scale in Rn. The change of variables and compactness and uniform-continuity inputs are A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not, For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact and Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, respectively.

Verification

1.1F1F2F3F4algebra

Fubini on a fixed product. By [F1], $I_{ε} : = \int φ (x) u_{ε} (x, t) d x = \frac{t}{4 π} \int_{R^{3}} \int_{S^{2}} φ (x) ρ_{ε} (x + c t ω) d σ (ω) d x$ . The integrand vanishes unless $∣ x ∣ \leq c t + ε$ , where $φ$ is bounded; the absolute integrand is bounded by $C ∥ ρ_{ε} ∥_{\infty} 1_{{\overline{B}}_{c t + ε} (0) \times S^{2}}$ , with $C = \sup_{∣ x ∣ \leq c t + ε} ∣ φ (x) ∣ < \infty$ . This majorant is integrable because the product rectangle has finite measure. Thus [F3] applies to the fixed product $R^{3} \times S^{2}$ . Set $y = x + c t ω$ in the inner Euclidean integral, then reflect $ω \mapsto - ω$ using Reflection invariance and vanishing first moment of the sphere measure. This gives $I_{ε} = \frac{t}{4 π} \int ρ_{ε} (y) \int_{S^{2}} φ (y + c t ω) d σ (ω) d y = \frac{t}{4 π c^{2} t^{2}} \int ρ_{ε} (y) Ψ (y) d y$ , with the last equality supplied by sphere-measure scaling Agreement with the existing polar sphere measure.

2.1F4step 1.1algebra∎

By [F4], $\int ρ_{ε} Ψ \to Ψ (0)$ . Therefore $I_{ε} \to \frac{t}{4 π c^{2} t^{2}} \int_{\partial B_{c t} (0)} φ d S = \frac{t}{4 π} \int_{S^{2}} φ (c t ω) d σ (ω)$ . The limiting measure has total mass $t$ and constant surface density $t / (4 π c^{2} t^{2})$ ; dividing the measure by $t$ gives the uniform probability measure on that sphere.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

104 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

Victor Ivrii, Partial Differential Equations (University of Toronto, 2018, CC BY-SA) (standard reference, not scraped)
Sung-Jin Oh, Lecture Notes for Math 222A (UC Berkeley, 19 March 2024) (standard reference, not scraped)