ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 Barenblatt profile has finite propagation

Statement

For $m > 1$ and $C > 0$ , put $β = \frac{1}{m + 1}, k = \frac{m - 1}{2 m (m + 1)}, u (t, x) = t^{- β} {(C - k x^{2} t^{- 2 β})}_{+}^{1 / (m - 1)} (t > 0, x \in R),$ where $r_{+} = \max (r, 0)$ . Then $u$ is a nonnegative distributional solution of the one-dimensional porous-medium equation $u_{t} = (u^{m})_{x x}$ on $(0, \infty) \times R$ . For every $t > 0$ it is supported in $∣ x ∣ \leq \sqrt{C / k} t^{1 / (m + 1)},$ so its support radius is finite and grows like $t^{1 / (m + 1)}$ .

Facts & Assumptions

Given: $m > 1$ , $C > 0$ , $t > 0$ , and the displayed profile.

[A1]

The exponent $m > 1$ and constant $C > 0$ are hypotheses; $r_{+}$ denotes $\max (r, 0)$ as defined in the statement.

Proof

1.1A1givenalgebra

Write $α = 1 / (m - 1)$ , $y = x t^{- β}$ , and $F (y) = (C - k y^{2})_{+}^{α}$ . Then $u = t^{- β} F (y)$ and $u^{m} = t^{- m β} G (y)$ , where $G (y) = (C - k y^{2})_{+}^{α + 1}$ . Inside the positivity set, $u_{t} = t^{- β - 1} (- β F - β y F^{'}), (u^{m})_{x x} = t^{- (m + 2) β} G^{''} .$ Equality of the time powers requires $β + 1 = (m + 2) β$ , giving $β = 1 / (m + 1)$ .

2.1A1step 1.1algebra

In the positivity set put $q = C - k y^{2} > 0$ . Direct differentiation gives $F^{'} = - 2 k α y q^{α - 1}, G^{''} = - 2 k (α + 1) q^{α - 1} (q - 2 k α y^{2}) = - 2 k (α + 1) (F + y F^{'}) .$ Choosing $2 k (α + 1) = β$ makes $G^{''} = - β (F + y F^{'})$ , exactly the remaining profile equation. Since $α + 1 = m / (m - 1)$ , this choice is $k = (m - 1) / (2 m (m + 1))$ . Thus the PDE holds pointwise wherever $u > 0$ ; both sides vanish in the open set where $u = 0$ .

3.1A1step 2.1algebra

The interface is $q = 0$ . The profile $u$ tends to zero there because $α > 0$ . The spatial flux $G$ and its first derivative $G^{'} = - 2 k (α + 1) y q_{+}^{α}$ also tend to zero at the interface, so distributional differentiation of $G$ creates no boundary delta. Its interior second derivative is locally integrable: its only possible singularity is proportional to $q^{α - 1}$ and $α - 1 > - 1$ . Likewise, $u_{t}$ has only a locally integrable $q^{α - 1}$ singularity; the moving interface contributes no time delta because the jump of $u$ across it is zero. Hence the pointwise identity of step 2.1 extends distributionally across the interface.

4.1A1step 1.1givenalgebra∎

The positivity condition is $C - k x^{2} t^{- 2 β} > 0$ , equivalent to $∣ x ∣ < \sqrt{C / k} t^{β}$ . Therefore the support is the stated closed interval, with radius proportional to $t^{β} = t^{1 / (m + 1)}$ . This proves finite propagation and the claimed scaling.

Used by

Nothing in the library uses this result yet.

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.