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.

The heat kernel is a self-similar solution with conserved unit mass

Example

Assume Countable Choice. Let $n \geq 1$ and $u (x, t) : = Γ (x, t)$ on $R^{n} \times (0, \infty)$ . Then $u$ solves the heat equation and is invariant under parabolic dilations with amplitude $λ^{n}$ : $u (λ x, λ^{2} t) = λ^{- n} u (x, t), equivalently λ^{n} u (λ x, λ^{2} t) = u (x, t), λ > 0,$ and its total mass is conserved: $\int_{R^{n}} u (x, t) d x = 1$ for every $t > 0$ .

Facts & Assumptions

Given: Countable Choice, $n \geq 1$ , $t > 0$ , $λ > 0$ and $x \in R^{n}$ .

[A1]

Countable Choice is the standing hypothesis of the kernel facts cited in [F1] and [F2] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For every $t > 0$ the kernel satisfies the unit-mass identity $\int_{R^{n}} Γ (x, t) d x = 1$ , the parabolic scaling identity $Γ (λ x, λ^{2} t) = λ^{- n} Γ (x, t)$ for every $λ > 0$ , is $C^{\infty}$ on $R^{n} \times (0, \infty)$ , and solves $\partial_{t} Γ = Δ_{x} Γ$ there (Normalisation, parabolic scaling, heat equation and derivative bounds for the heat kernel, The heat kernel on $R^{n}$ and its causal extension).

[F2]

For all $s, t > 0$ , $Γ_{t} * Γ_{s} = Γ_{t + s}$ (The heat kernel semigroup identity $Γ_{t} * Γ_{s} = Γ_{t + s}$ ), and the evolution $H_{t}$ of The heat evolution $H_{t}$ of initial data acts by convolution with $Γ_{t}$ .

Verification

technique · direct

1.1A1F1given

Solving the heat equation: by the smoothness and heat-equation clauses of [F1], the function $u (x, t) = Γ (x, t)$ is $C^{\infty}$ on $R^{n} \times (0, \infty)$ and satisfies $\partial_{t} u (x, t) = \partial_{t} Γ (x, t) = Δ_{x} Γ (x, t) = Δ_{x} u (x, t)$ at every point.

2.1step 1.1F1givenalgebra

Parabolic self-similarity: the scaling clause of [F1] reads $Γ (λ x, λ^{2} t) = λ^{- n} Γ (x, t)$ for every $λ > 0$ ; multiplying both sides by $λ^{n}$ gives the equivalent form $λ^{n} u (λ x, λ^{2} t) = u (x, t)$ , equivalently $u (x, λ^{2} t) = λ^{- n} u (x / λ, t)$ , so the profile at time $λ^{2} t$ has spatial scale multiplied by $λ$ and amplitude multiplied by $λ^{- n}$ .

2.2step 1.1F1given

Conserved mass: the unit-mass clause of [F1] gives $\int_{R^{n}} u (x, t) d x = \int_{R^{n}} Γ (x, t) d x = 1$ for every $t > 0$ , independently of $t$ .

3.1step 1.1step 2.1step 2.2F2given∎

Steps 1.1, 2.1 and 2.2 show that $u = Γ$ solves the heat equation, satisfies the stated parabolic dilation law with amplitude $λ^{n}$ , and has unit total mass at every positive time; the semigroup identity [F2] records the equivalent convolution form of the same one-parameter family.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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)
Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #5: The Fundamental Solution for the Heat Equation (Fall 2011) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)