The Wave Equation
The first three chapters of this corpus share one toolkit: a static bilinear form, coercivity, Lax–Milgram. That toolkit is elliptic machinery, and it does not extend to this chapter. The wave equation is genuinely second-order in time — it needs both an initial position and an initial velocity to be well-posed — and its natural well-posedness argument is the energy method: multiply by the time derivative, integrate by parts, and track a conserved quantity directly, rather than inverting a stationary operator. Completing the elliptic/parabolic/hyperbolic triad this deliberately is also what makes the comparison to the heat equation's own Part V exact rather than rhetorical, which is the real payoff of this chapter.
The model
Take the 1D wave equation on (0,1) with homogeneous Dirichlet boundary conditions and both initial position and initial velocity data:
Unlike the heat equation, there is no mass term and no dissipation anywhere in this equation — nothing to make a stationary bilinear form coercive, because there is no stationary bilinear form to begin with. What replaces it is a quantity that is exactly conserved along trajectories.
The energy method
Multiply the equation by ut and integrate over (0,1):
The left side is ½ d/dt ∫ut²dx. Integrating the right side by parts gives a boundary term [uxut]₀¹, which vanishes exactly: the Dirichlet condition u(0,t)=u(1,t)=0 for all t forces ut(0,t)=ut(1,t)=0 as well, so both endpoints kill the term regardless of what ux does there — the same vanishing-boundary-term step every earlier chapter in this corpus has used, applied here to the time derivative of the boundary condition rather than to a test function. What remains is −½ d/dt ∫ux²dx. Together:
E(t) is exactly conserved, not merely bounded. This single identity is the whole well-posedness argument for this class of problems in outline: a Galerkin approximation (project onto finitely many Dirichlet eigenmodes, solve the resulting finite-dimensional ODE system exactly, and pass to the limit) inherits the same energy identity at every finite level, which supplies the a priori bound needed to extract a convergent subsequence. No coercive bilinear form and no Lax–Milgram appear anywhere in that argument — energy conservation does the entire job elliptic coercivity did in the earlier chapters.
The exact mirror of the heat equation's H-theorem
The heat equation chapter's Part V (Prop. 20.1) proves H(t) := ½∫u²dx is strictly decreasing along solutions — the same multiply-and-integrate-by-parts technique, applied to u itself rather than ut, because the heat equation is only first-order in time. That decay is irreversible: Corollary 20.3 there notes the forward solution map loses information, since two different initial states can decay toward indistinguishable states as t → ∞, and nothing recovers the initial data from a late-time snapshot. This chapter's E(t) is the structurally identical computation with the opposite outcome: because the equation is second-order in time, the boundary term that killed the mass term's contribution here instead preserves both the kinetic (ut²) and potential (ux²) pieces exactly, and the solution map (u₀,u₁) ↦ (u(·,T),ut(·,T)) is invertible — run time backward from any snapshot and the original data returns exactly, because u(x,−t) solves the same equation whenever u(x,t) does. Heat loses information; waves do not. Same corpus, same integration-by-parts step, opposite conclusion — which is exactly what a second-order-in-time versus first-order-in-time distinction should produce, not a coincidence needing further explanation.
Finite propagation speed
The other qualitative break from the heat equation is how information travels. The heat equation's Green's function is a Gaussian supported on all of ℝ for any t>0 — a localized disturbance is felt everywhere instantly, however faintly. The wave equation on the whole line admits the classical d'Alembert solution
which shows the value at (x,t) depends only on initial data within the interval [x−t,x+t] — a finite domain of dependence, propagation speed exactly 1 in these units. A compactly supported disturbance stays compactly supported, expanding at a fixed rate rather than spreading into a tail everywhere at once.
| Statement | Status | Notes |
|---|---|---|
| Energy identity d/dt E(t) = 0 | derived + numerically checked | Verified against the exact standing-wave solution over 3+ periods, not just at t=0 |
| Time-reversibility / invertible solution map | derived | Follows from u(x,-t) solving the same equation; contrasted directly against the heat equation's Cor. 20.3 |
| Finite propagation speed (d'Alembert) | derived + numerically checked | Exact light-cone support confirmed on a fine grid, whole-line case |
| Galerkin / energy-method well-posedness on (0,1) | sorry | Outlined above; the finite-dimensional ODE step and the passage to the limit are not yet formalized |
| Lean / AXLE formalization | not started | No scaffold file yet; would need a genuinely new object (u_t as an independent field) rather than reusing H10 alone |
What this chapter shows: the energy identity and the finite-propagation
result, both derived honestly and both checked against an exact
solution or exact formula, not merely asserted. What it does not show:
a formalized existence-uniqueness theorem on the bounded domain
(0,1) — the Galerkin argument is described, not carried out in
Lean, and no scaffold file exists yet for this chapter, unlike the heat
equation's HeatEquation_Step1.lean. The energy method
outlined here is the standard textbook route (Evans, Partial
Differential Equations, §7.2), not a novel result; the
contribution of this chapter is placing it inside this corpus's own
honest-ledger convention and making its contrast with the heat
equation's H-theorem explicit rather than left implicit.