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 compactly supported velocity datum produces an expanding interval

Example

Let $c > 0$ , $a > 0$ , $u_{0} = 0$ and $u_{1} = 1_{[- a, a]}$ . Although this indicator is not in the classical data class of d'Alembert's formula and uniqueness in one dimension, its displayed integral expression extends directly to this bounded datum and gives $u (x, t) = \frac{1}{2 c} ∣ [x - c t, x + c t] \cap [- a, a] ∣, t \geq 0,$ i.e. the length over $2 c$ of the overlap of the moving interval with the data interval. For $t > 0$ the nonzero set is exactly ${x : ∣ x ∣ < a + c t}$ and its topological support is the closed interval $[- a - c t, a + c t]$ ; at $t = 0$ the profile is identically zero and its support is empty. Once $c t \geq a$ , the profile equals $a / c$ throughout ${∣ x ∣ \leq c t - a}$ ; the two wavefronts travel outward at speed $c$ and the disturbance never reaches $∣ x ∣ > a + c t$ .

Facts & Assumptions

Given: a speed $c > 0$ , a half-width $a > 0$ , the data $u_{0} = 0$ , $u_{1} = 1_{[- a, a]}$ , and the displayed function $u$ .

[F1]

For admissible data, the d'Alembert expression is the unique classical solution (d'Alembert's formula and uniqueness in one dimension); its velocity integral is well defined for the bounded compactly supported indicator used here as well.

Verification

1.1F1algebra

Substituting $u_{0} = 0$ into the velocity integral gives $u (x, t) = \frac{1}{2 c} \int_{x - c t}^{x + c t} 1_{[- a, a]} (y) d y = \frac{1}{2 c} ∣ [x - c t, x + c t] \cap [- a, a] ∣$ , since the integral of the indicator is the overlap length. For smooth admissible approximations, the same d'Alembert expression is a classical solution by [F1].

1.2algebra

Nonzero set and plateau. For $t > 0$ , the overlap has positive length exactly when $x - c t < a$ and $x + c t > - a$ , that is $∣ x ∣ < a + c t$ ; its closure, the topological support, is $[- a - c t, a + c t]$ . At $t = 0$ the moving interval is a singleton, so the overlap has length zero for every $x$ and the support is empty. The overlap is the full data interval, of length $2 a$ , when $∣ x ∣ \leq c t - a$ (which requires $c t \geq a$ ), giving value $a / c$ there.

2.1algebra∎

The formula therefore has expanding nonzero set $(- a - c t, a + c t)$ for $t > 0$ , closed support $[- a - c t, a + c t]$ , zero support at $t = 0$ , and the stated full-data plateau when $c t \geq a$ .

Depends on

d'Alembert's formula and uniqueness in one dimension

Used by

Displacement data versus velocity data in one dimension Example

Dependency tree · two levels

7 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

Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #10: Introduction to the Wave Equation (Fall 2011) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (revised 18 June 2014, UC Davis) (standard reference, not scraped)