TheoremStatement: AI-adaptedProof: AI-generatedPipeline-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.

Coercive discrete energy for the Dirichlet leapfrog wave scheme

Statement

For the homogeneous Dirichlet recurrence of Centered leapfrog wave recurrence with Dirichlet and periodic rows, let $0 < ν = c k / h < 1$ , $V^{n} = (U^{n + 1} - U^{n}) / k$ , and ${\overset{ˉ}{U}}^{n} = (U^{n + 1} + U^{n}) / 2$ . Define $E^{n + 1 / 2} = \frac{1}{2} ∥ V^{n} ∥_{h}^{2} + \frac{c^{2}}{2} ⟨ D_{+} U^{n + 1}, D_{+} U^{n} ⟩_{e, h} .$ Then $E^{n + 1 / 2}$ is independent of $n$ and $E^{n + 1 / 2} \geq \frac{1 - ν^{2}}{2} ∥ V^{n} ∥_{h}^{2} + \frac{c^{2}}{2} ∥ D_{+} {\overset{ˉ}{U}}^{n} ∥_{e, h}^{2} .$ Consequently it is a positive quadratic form on adjacent zero-boundary states. For mesh families with fixed wave speed $c > 0$ , fixed interval length $L$ , and $ν \leq ν_{0} < 1$ , it controls the interior state and its discrete velocity with constants independent of $h$ .

Facts & Assumptions

Given: A fixed wave speed $c > 0$ , mesh sizes $h, k > 0$ , homogeneous Dirichlet endpoint values, and the source-free centered leapfrog recurrence.

[F1]

The recurrence is $δ_{t}^{2} U^{n} = c^{2} Δ_{h} U^{n}$ , with $U_{0}^{n} = U_{N}^{n} = 0$ (Centered leapfrog wave recurrence with Dirichlet and periodic rows).

[F2]

For zero endpoint values, $⟨ u, - Δ_{h} v ⟩_{h} = ⟨ D_{+} u, D_{+} v ⟩_{e, h}$ ; this is symmetric in $u, v$ (One-dimensional discrete summation by parts with boundary terms).

[F3]

If $w_{0} = w_{N} = 0$ on length $L = N h$ , then $∥ w ∥_{h} \leq L ∥ D_{+} w ∥_{e, h}$ (A finite-grid Poincare inequality for zero endpoint values).

Proof

1.1F1algebra

In the quadratic term, $D_{+} U^{n + 1} = D_{+} {\overset{ˉ}{U}}^{n} + \frac{k}{2} D_{+} V^{n}$ and $D_{+} U^{n} = D_{+} {\overset{ˉ}{U}}^{n} - \frac{k}{2} D_{+} V^{n}$ . Expanding their real edge inner product gives $E^{n + 1 / 2} = \frac{1}{2} ∥ V^{n} ∥_{h}^{2} + \frac{c^{2}}{2} ∥ D_{+} {\overset{ˉ}{U}}^{n} ∥_{e, h}^{2} - \frac{c^{2} k^{2}}{8} ∥ D_{+} V^{n} ∥_{e, h}^{2} .$

2.1givenstep 1.1algebra

For any zero-endpoint grid function $v$ , $(v_{j + 1} - v_{j})^{2} \leq 2 v_{j + 1}^{2} + 2 v_{j}^{2}$ and summing over edges gives $∥ D_{+} v ∥_{e, h}^{2} = \frac{1}{h} \sum_{j = 0}^{N - 1} (v_{j + 1} - v_{j})^{2} \leq \frac{4}{h^{2}} ∥ v ∥_{h}^{2} .$ Apply this to $V^{n}$ , and use $ν = c k / h$ , in step 1.1 to obtain the asserted lower bound. Since $1 - ν^{2} > 0$ , zero energy forces $V^{n} = 0$ and $D_{+} {\overset{ˉ}{U}}^{n} = 0$ .

3.1F3step 2.1algebra

A zero-endpoint grid function with $D_{+} w = 0$ is constant across all edges and therefore zero. Hence step 2.1 shows $E^{n + 1 / 2} = 0$ only when $V^{n} = 0$ and ${\overset{ˉ}{U}}^{n} = 0$ , equivalently $U^{n + 1} = U^{n} = 0$ . For uniform state control, [F3] bounds $∥ {\overset{ˉ}{U}}^{n} ∥_{h}$ by $L ∥ D_{+} {\overset{ˉ}{U}}^{n} ∥_{e, h}$ , and $U^{n + 1}, U^{n} = {\overset{ˉ}{U}}^{n} \pm (k / 2) V^{n}$ ; when $ν \leq ν_{0} < 1$ , the lower-bound coefficients and $k \leq ν_{0} L / (N c) \leq ν_{0} L / c$ are uniform in the mesh.

4.1F1F2step 1.1algebra∎

Let $δ_{t}^{0} U^{n} = (U^{n + 1} - U^{n - 1}) / (2 k)$ . Taking the interior inner product of $δ_{t}^{2} U^{n} + c^{2} (- Δ_{h}) U^{n} = 0$ with $δ_{t}^{0} U^{n}$ , the first term is $(∥ V^{n} ∥_{h}^{2} - ∥ V^{n - 1} ∥_{h}^{2}) / (2 k)$ . By [F2], the second is $\frac{c^{2}}{2 k} (⟨ D_{+} U^{n + 1}, D_{+} U^{n} ⟩_{e, h} - ⟨ D_{+} U^{n}, D_{+} U^{n - 1} ⟩_{e, h}) .$ Their sum is $(E^{n + 1 / 2} - E^{n - 1 / 2}) / k = 0$ . Thus the energy is conserved.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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

Endre Süli, B6.1 Numerical Solution of Partial Differential Equations (standard reference, not scraped)