TheoremStatement: Literature-sourcedProof: 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.

The forced one-dimensional wave formula over the characteristic triangle

Statement

Let $c > 0$ , $u_{0} \in C^{2} (R)$ , $u_{1} \in C^{1} (R)$ and let $f$ be of class $C^{1}$ on $R \times [0, \infty)$ , so that $f$ , $\partial_{x} f$ and $\partial_{t} f$ are continuous. Then $u (x, t) = \frac{1}{2} (u_{0} (x - c t) + u_{0} (x + c t)) + \frac{1}{2 c} \int_{x - c t}^{x + c t} u_{1} (y) d y + \frac{1}{2 c} \int_{0}^{t} \int_{x - c (t - s)}^{x + c (t - s)} f (y, s) d y d s$ is the unique classical solution of $u_{t t} = c^{2} u_{x x} + f$ with $u (\cdot, 0) = u_{0}$ , $u_{t} (\cdot, 0) = u_{1}$ . The source integral is over the backward characteristic triangle with vertex $(x, t)$ : $0 \leq s \leq t$ , $∣ y - x ∣ \leq c (t - s)$ , and its coefficient is $1 / (2 c)$ .

Facts & Assumptions

Given: a speed $c > 0$ , data $u_{0} \in C^{2} (R)$ , $u_{1} \in C^{1} (R)$ , a source $f \in C^{1} (R \times [0, \infty))$ , and the displayed function $u$ .

[F1]

Let $α, β \in C^{1} (I)$ with $α < β$ and let $F$ be continuous on $I \times J$ with continuous $\partial_{t} F$ , where $J$ contains the closure of the union of the intervals $[α (t), β (t)]$ . Then $G (t) = \int_{α (t)}^{β (t)} F (t, y) d y$ is $C^{1}$ with $G^{'} (t) = F (t, β (t)) β^{'} (t) - F (t, α (t)) α^{'} (t) + \int_{α (t)}^{β (t)} \partial_{t} F (t, y) d y$ (Differentiating an integral with moving endpoints).

[F2]

For continuous $φ$ , the function $x \mapsto \int_{a (x)}^{b (x)} φ$ has derivative $φ (b (x)) b^{'} (x) - φ (a (x)) a^{'} (x)$ ; more generally the primitive of a continuous function is recovered by evaluation at the endpoints (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ ).

[F3]

With data $u_{0}, u_{1}$ the homogeneous d'Alembert expression is the unique $C^{2}$ solution of $u_{t t} = c^{2} u_{x x}$ with those data (d'Alembert's formula and uniqueness in one dimension).

[F4]

Sums, products, constant multiples of differentiable functions are differentiable with the usual rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

Proof

1.1F1F2F4algebra

The source term. Extend $f (y, s)$ to $s < 0$ by $f (y, 0)$ ; its value and first spatial derivative remain continuous. Define $Φ (x, t, s) : = \int_{x - c (t - s)}^{x + c (t - s)} f (y, s) d y$ as an oriented integral, also when $t < s$ . Primitives [F2] give $Φ_{t} = c [f (x + c (t - s), s) + f (x - c (t - s), s)]$ and $Φ_{x} = f (x + c (t - s), s) - f (x - c (t - s), s)$ on an open rectangle in $(t, s)$ , including $s = t$ . Since $Φ (x, t, t) = 0$ , [F1] gives $D_{t} = \frac{1}{2} \int_{0}^{t} [f (x + c (t - s), s) + f (x - c (t - s), s)] d s$ for $D = (2 c)^{- 1} \int_{0}^{t} Φ d s$ . The compact-rectangle theorem Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral permits spatial differentiation under this fixed $s$ -integral. Thus $D_{x} = (2 c)^{- 1} \int_{0}^{t} [f (x + c (t - s), s) - f (x - c (t - s), s)] d s$ and $D_{x x} = (2 c)^{- 1} \int_{0}^{t} [f_{x} (x + c (t - s), s) - f_{x} (x - c (t - s), s)] d s$ .

2.1F1F4step 1.1algebra

Equation and regularity. Differentiating $D_{t}$ by [F1] gives $D_{t t} = f (x, t) + \frac{c}{2} \int_{0}^{t} [f_{x} (x + c (t - s), s) - f_{x} (x - c (t - s), s)] d s = f + c^{2} D_{x x}$ . The chain rule The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ gives the displayed integrand derivatives; differentiation of $D_{t}$ in $x$ gives $D_{t x} = \frac{1}{2} \int_{0}^{t} [f_{x} (x + c (t - s), s) + f_{x} (x - c (t - s), s)] d s$ , also equal to $D_{x t}$ by differentiating $D_{x}$ . All these derivatives are continuous because their integrands are continuous on local compact rectangles. At zero, $D, D_{x}, D_{t}, D_{x x}, D_{x t}$ tend to zero and $D_{t t} \to f (x, 0)$ locally uniformly, proving the asserted $C^{2}$ regularity up to the initial time.

3.1F3step 1.1step 2.1algebra

Data and uniqueness. At $t = 0$ the source integral vanishes, so $u (\cdot, 0) = u_{0}$ and $u_{t} (\cdot, 0) = u_{1}$ are exactly the statements of [F3] for the homogeneous part. If $v$ is any classical solution of the forced problem with the same data, then $w : = u - v$ is $C^{2}$ with $w_{t t} = c^{2} w_{x x}$ and zero data, so $w = 0$ by the uniqueness clause of [F3]; hence $u$ is the unique classical solution.

4.1given∎

The double integral runs over $0 \leq s \leq t$ and $∣ y - x ∣ \leq c (t - s)$ , the backward characteristic triangle with vertex $(x, t)$ , and its coefficient is $1 / (2 c)$ ; this completes the identification of the displayed solution.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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)
Per Kristen Jakobsen, An Introduction to Partial Differential Equations (arXiv:1901.03022) (standard reference, not scraped)
Jared Speck, MIT 18.152 Introduction to Partial Differential Equations, Class Meeting #10: Introduction to the Wave Equation (Fall 2011) (standard reference, not scraped)