TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

d'Alembert's formula solves the wave equation, is the unique $C^{2}$ solution, and the fixed-end sine modes solve it exactly

Statement

Let $c > 0$ .

(a) The formula. For every $f \in C^{2} (R)$ and $g \in C^{1} (R)$ , the function

$u (t, x) : = \frac{f (x - c t) + f (x + c t)}{2} + \frac{1}{2 c} \int_{x - c t}^{x + c t} g (s) d s ((t, x) \in R^{2})$

is of class $C^{2}$ ( $C^{k}$ Euclidean maps and diffeomorphisms) and satisfies

$u_{t t} = c^{2} u_{x x}, u (0, x) = f (x), u_{t} (0, x) = g (x)$

for every $x \in R$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

(b) Uniqueness. If $u \in C^{2} (R^{2})$ satisfies $u_{t t} = c^{2} u_{x x}$ with $u (0, \cdot) = f$ and $u_{t} (0, \cdot) = g$ for $f \in C^{2} (R)$ , $g \in C^{1} (R)$ , then $u$ equals the formula in (a).

(c) Fixed ends and modes. Let $L > 0$ and, for each integer $n \geq 1$ ,

$u_{n} (t, x) : = \sin ⁣ (\frac{n π x}{L}) \cos ⁣ (\frac{n π c t}{L}) .$

Then each $u_{n}$ is $C^{\infty}$ on $R^{2}$ , satisfies $u_{t t} = c^{2} u_{x x}$ , vanishes at $x = 0$ and $x = L$ for every $t$ , and has $u_{n} (0, x) = \sin (n π x / L)$ , $\partial_{t} u_{n} (0, x) = 0$ . Every finite sum $\sum_{n \leq N} α_{n} u_{n} + β_{n} v_{n}$ with the companion modes $v_{n} (t, x) : = \sin (n π x / L) \sin (n π c t / L) / (n π c / L)$ also solves the equation, vanishes at both ends and has the corresponding finite initial data.

Facts & Assumptions

Given: The wave speed $c > 0$ ; data $f \in C^{2} (R)$ , $g \in C^{1} (R)$ in (a), (b); $L > 0$ and the modes in (c).

[F1]

The integral function $F (x) : = \int_{0}^{x} g$ is $C^{2}$ with $F^{'} = g$ , and for $a < b$ the oriented integral satisfies $\int_{a}^{b} g = F (b) - F (a)$ , $\int_{a}^{b} = - \int_{b}^{a}$ , and additivity over subintervals; continuous functions are integrable on compact intervals (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ , The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , A function integrable on $[a, b]$ is integrable on every closed subinterval, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

[F2]

Chain rule and algebra of derivatives for compositions with the affine maps $(t, x) \mapsto x \pm c t$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , 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$ , $C^{k}$ Euclidean maps and diffeomorphisms).

[F3]

Trigonometric values and derivatives: $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , $\sin (n π) = 0$ and $\cos (0) = 1$ (The derivatives of sine and cosine are cosine and minus sine, The zero sets of sine and cosine and the least positive common period 2 pi, Parity and the Pythagorean identity for sine and cosine, Sine and cosine defined by their real power series).

[F4]

If $q$ is $C^{2}$ on an open neighbourhood of a point $(t, x)$ , then $q_{t x} = q_{x t}$ there. For small $h, k > 0$ , the divided rectangular increment of $q$ over $[t, t + h] \times [x, x + k]$ equals the average of each mixed partial in its corresponding iterated order, by the one-variable fundamental theorem; continuity of the second partials makes the two averages tend to the respective mixed partial values, which must therefore agree (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

Proof

technique · direct; differentiate the explicit formula, then split the solution into the two characteristic combinations for uniqueness, and verify the modes by substitution

1.1givenF1F2algebra

By [F1] write $F (x) = \int_{0}^{x} g$ ; then $u (t, x) = \frac{f (x - c t) + f (x + c t)}{2} + \frac{F (x + c t) - F (x - c t)}{2 c}$ . By [F2] (affine chain rule) and [F1], this is $C^{2}$ in $(t, x)$ and $u_{t} = \frac{- c f^{'} (x - c t) + c f^{'} (x + c t)}{2} + \frac{g (x + c t) + g (x - c t)}{2}, u_{x} = \frac{f^{'} (x - c t) + f^{'} (x + c t)}{2} + \frac{g (x + c t) - g (x - c t)}{2 c} .$

1.2givenF2F4algebra

(Uniqueness.) For a $C^{2}$ solution $u$ set $v : = u_{t} + c u_{x}$ and $w : = u_{t} - c u_{x}$ . By [F2] and the mixed-partial identity [F4], $v_{t} - c v_{x} = u_{t t} + c u_{x t} - c u_{t x} - c^{2} u_{x x} = 0$ and $w_{t} + c w_{x} = u_{t t} - c u_{x t} + c u_{t x} - c^{2} u_{x x} = 0$ . Hence $s \mapsto v (s, x_{0} - c s)$ is constant for every fixed $x_{0}$ : its derivative is $v_{t} - c v_{x} = 0$ by [F2], so $v (t, x) = v (0, x + c t) = g (x + c t) + c f^{'} (x + c t)$ for every $(t, x)$ . Likewise $w (t, x) = w (0, x - c t) = g (x - c t) - c f^{'} (x - c t)$ .

2.1step 1.1F1F2algebra

Differentiating again by [F2] and [F1], $u_{t t} = \frac{c^{2} f^{''} (x - c t) + c^{2} f^{''} (x + c t)}{2} + \frac{c g^{'} (x + c t) - c g^{'} (x - c t)}{2}, u_{x x} = \frac{f^{''} (x - c t) + f^{''} (x + c t)}{2} + \frac{g^{'} (x + c t) - g^{'} (x - c t)}{2 c} .$ Hence $u_{t t} = c^{2} u_{x x}$ . Evaluating step 1.1 at $t = 0$ gives $u (0, x) = f (x)$ and $u_{t} (0, x) = \frac{- c f^{'} (x) + c f^{'} (x)}{2} + \frac{g (x) + g (x)}{2} = g (x)$ . This proves (a).

2.2step 1.2F1F2algebra

From step 1.2, $u_{t} = \frac{v + w}{2} = \frac{g (x + c t) + g (x - c t)}{2} + \frac{c f^{'} (x + c t) - c f^{'} (x - c t)}{2}$ . Since $s \mapsto u (s, x)$ is differentiable with derivative $u_{t} (s, x)$ , the fundamental theorem [F1] gives $u (t, x) - f (x) = \int_{0}^{t} u_{t} (s, x) d s$ . Substituting step 1.2 and integrating with [F1] (the substitutions $y = x + c s$ and $y = x - c s$ are affine) yields $\int_{0}^{t} \frac{g (x + c s) + g (x - c s)}{2} d s = \frac{F (x + c t) - F (x - c t)}{2 c}, \int_{0}^{t} \frac{c f^{'} (x + c s) - c f^{'} (x - c s)}{2} d s = \frac{f (x + c t) + f (x - c t)}{2} - f (x) .$ Adding and cancelling $f (x)$ identifies $u$ with the formula of (a). This proves (b).

3.1givenF2F3algebra∎

(Modes.) Fix $n \geq 1$ and put $θ : = n π x / L$ , $φ : = n π c t / L$ . By [F2], $u_{n}$ is $C^{\infty}$ with $u_{n, t t} = - (n π c / L)^{2} u_{n}$ and $u_{n, x x} = - (n π / L)^{2} u_{n}$ , so $u_{n, t t} = c^{2} u_{n, x x}$ . By [F3], $u_{n} (t, 0) = \sin 0 = 0$ and $u_{n} (t, L) = \sin (n π) \cos φ = 0$ ; $u_{n} (0, x) = \sin θ \cos 0 = \sin θ$ and $\partial_{t} u_{n} (0, x) = - (n π c / L) \sin θ \sin 0 = 0$ . The companion mode $v_{n} = (L / (n π c)) \sin θ \sin φ$ satisfies $v_{n, t t} = - (n π c / L)^{2} v_{n}$ and $v_{n, x x} = - (n π / L)^{2} v_{n}$ by the same computation, has $v_{n} (0, x) = 0$ and $\partial_{t} v_{n} (0, x) = \sin θ$ , and vanishes at both ends. Finite sums solve the linear equation and the boundary conditions because derivatives and finite sums commute; they have the corresponding finite initial data. This proves (c).

Remarks

Parts (a) and (b) are stated on all of $R^{2}$ for $C^{2}$ data; no weaker regularity, no distributional solutions, and no boundary conditions enter. The formula requires $f \in C^{2}$ , $g \in C^{1}$ exactly so that the displayed second derivatives exist and are continuous.
The modes in (c) are exact solutions of the equation and of the two endpoint conditions; they are not asserted to exhaust the solutions with fixed ends, and no infinite-series representation is claimed here. The companion modes $v_{n}$ are normalized so that $\partial_{t} v_{n} (0, \cdot) = \sin (n π x / L)$ ; their amplitude factor has time units divided by the corresponding velocity when units are declared in a consuming model.

d'Alembert's formula solves the wave equation, is the unique $C^{2}$ solution, and the fixed-end sine modes solve it exactly

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

d'Alembert's formula solves the wave equation, is the unique C2C2 solution, and the fixed-end sine modes solve it exactly

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

d'Alembert's formula solves the wave equation, is the unique $C^{2}$ solution, and the fixed-end sine modes solve it exactly