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.

Odd reflection at a Dirichlet endpoint

Example

Assume the Axiom of Countable Choice. Let $c > 0$ , let $u_{0} \in C_{c}^{2} (R)$ and $u_{1} \in C_{c}^{1} (R)$ be odd — equivalently, data on the half-line $x > 0$ extended oddly — and let $U$ be the d'Alembert solution of the whole-line problem with data $(u_{0}, u_{1})$ (d'Alembert's formula and uniqueness in one dimension). Then:

(i) $U (\cdot, t)$ is odd for every $t$ , so $u : = U ∣_{x > 0}$ solves the Dirichlet half-line problem $u_{t t} = c^{2} u_{x x}$ on $x > 0$ with $u (0, t) = 0$ and data $u_{0} ∣_{x > 0}$ , $u_{1} ∣_{x > 0}$ ;

(ii) for data obtained by oddly extending $u_{0} = ϕ$ , $u_{1} = c ϕ^{'}$ from $x > 0$ , where $ϕ \in C_{c}^{2} ((0, \infty))$ , the reflected part re-enters with reversed sign:

$u (x, t) = ϕ (x + c t) - ϕ (c t - x) (0 < x < c t);$

(iii) the half-line energy $E_{(0, \infty)} (t) = \frac{1}{2} \int_{0}^{\infty} (u_{t}^{2} + c^{2} u_{x}^{2}) d x$ equals half the whole-line energy of $U$ and is constant in $t$ (Ivrii's Dirichlet case of the half-line energy problem).

Facts & Assumptions

Given: ${A C}_{ω}$ ; $c > 0$ ; odd compactly supported data $u_{0} \in C_{c}^{2} (R)$ , $u_{1} \in C_{c}^{1} (R)$ ; the d'Alembert solution $U$ of the whole-line problem, and for part (ii) a fixed $ϕ \in C_{c}^{2} ((0, \infty))$ with $u_{0} = ϕ$ , $u_{1} = c ϕ^{'}$ on $x > 0$ .

[F1]

D'Alembert's formula: for $U_{0} \in C^{2} (R)$ , $U_{1} \in C^{1} (R)$ the whole-line solution is $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} (s) d s$ , a $C^{2}$ classical solution of $u_{t t} = c^{2} u_{x x}$ . (d'Alembert's formula and uniqueness in one dimension)

[F2]

Conservation in case (a): a homogeneous solution whose spatial support is contained in a fixed compact set throughout a time interval has constant total energy on that interval. (Conservation of total wave energy in three admissible settings)

[F3]

The energy density is $e = \frac{1}{2} (U_{t}^{2} + c^{2} U_{x}^{2})$ . By [F1] and the support definition, the spatial support of $U (\cdot, t)$ is contained in $(supp U_{0} \cup supp U_{1}) + [- c t, c t]$ . (Wave energy density, energy flux and total energy, The support of a function on $R^{n}$ and its compactly supported Riemann integral)

[F4]

The integral of a continuous derivative on a closed interval equals the endpoint difference; its Darboux, Riemann and Lebesgue integrals agree. (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)$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ , A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral)

[F5]

Closed bounded Euclidean sets are compact; continuous functions on nonempty compact sets are bounded and uniformly continuous. (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous)

Verification

1.1givenF1algebra

Oddness is preserved and the half-line problem is solved: if $U_{0} = u_{0}$ and $U_{1} = u_{1}$ are odd, then each term of [F1] is odd in $x$ : for the first term, replacing $x$ by $- x$ interchanges the two arguments of the odd function $U_{0}$ and changes the sign, and for the integral term the substitution $s \mapsto - s$ together with oddness of $U_{1}$ reverses the orientation of the interval and the sign of the integrand, leaving the integral odd in $x$ ; hence $U (\cdot, t)$ is odd for every $t$ , so $U (0, t) = 0$ ; therefore $u : = U ∣_{x > 0}$ is a $C^{2}$ solution of $u_{t t} = c^{2} u_{x x}$ on $x > 0$ with trace $u (0, t) = 0$ and the prescribed initial data $u_{0} ∣_{x > 0}$ , $u_{1} ∣_{x > 0}$ , which is (i).

2.1givenstep 1.1F1F4algebra

Reflection with reversed sign: take $u_{0} = ϕ$ and $u_{1} = c ϕ^{'}$ with $ϕ$ compactly supported in $(0, \infty)$ , extended oddly, and $0 < x < c t$ ; in [F1] the first term is $\frac{1}{2} [ϕ (x + c t) - ϕ (c t - x)]$ because $x - c t < 0 < x + c t$ and $U_{0} (- ξ) = - ϕ (ξ)$ for $ξ > 0$ ; the integral term is $\frac{1}{2 c} [c ϕ (x + c t) - c ϕ (c t - x)]$ by [F4] applied to the odd extension of $c ϕ^{'}$ on the two subintervals cut by $0$ ; adding, $u (x, t) = ϕ (x + c t) - ϕ (c t - x)$ as claimed; for $x > c t$ the same computation gives $u (x, t) = ϕ (x + c t)$ , the incoming left-moving profile, so the second term is precisely the reflection.

3.1givenstep 1.1F1F2F3algebraF5∎

Half-line energy: for each $t$ the density $e (U) (x, t) = \frac{1}{2} (U_{t}^{2} + c^{2} U_{x}^{2})$ is even in $x$ , because $U (\cdot, t)$ odd makes $U_{t} (\cdot, t)$ odd and $U_{x} (\cdot, t)$ even; hence $\int_{R} e d x = 2 \int_{0}^{\infty} e d x$ , that is, $E_{(0, \infty)} (t) = \frac{1}{2} E_{R} (t)$ ; fix $T_{0} > 0$ ; by [F3] the support of $U (\cdot, t)$ is contained in the fixed compact set $K : = (supp u_{0} \cup supp u_{1}) + [- c T_{0}, c T_{0}]$ for every $t \in [0, T_{0}]$ , so [F2] makes $E_{R}$ constant on $(0, T_{0})$ ; moreover $E_{R} (t) = \int_{K} e (U) (x, t) d x$ there and at the endpoints, and uniform continuity of $e (U)$ on $K \times [0, T_{0}]$ together with the finite measure of $K$ makes this energy continuous on $[0, T_{0}]$ , so the constancy extends to both endpoints; hence $E_{(0, \infty)} = \frac{1}{2} E_{R}$ is constant on $[0, T_{0}]$ , and since $T_{0}$ was arbitrary it is constant on $[0, \infty)$ , which is (iii).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

117 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)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, AMS Graduate Studies in Mathematics) (standard reference, not scraped)