ode_zero_uniqueness_neg
plain-language theorem explainer
The zero function is the unique C² solution to the ODE f'' = -f that satisfies the homogeneous initial conditions f(0) = f'(0) = 0. Workers on the cosine branch of d'Alembert uniqueness cite the result to clear the trivial case before proving the normalized cosine solution. The argument applies the energy-invariance lemma at an arbitrary point and concludes by non-negativity of squares plus linear arithmetic.
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable. If $f''(t) = -f(t)$ for all real $t$, $f(0) = 0$, and $f'(0) = 0$, then $f(t) = 0$ for every real $t$.
background
The declaration belongs to the cosine branch of the d'Alembert functional equation in the AngleFunctionalEquation module. That module treats the two solution branches of H(t+u) + H(t-u) = 2 H(t) H(u): the cosh branch (H'' = H) that yields the J-cost functional, and the cos branch (H'' = -H) that yields the angle coupling function under the calibration H''(0) = -1. Axioms Aθ1–Aθ4 encode d'Alembert, regularity, normalization, and the negative-curvature condition that selects cosine.
proof idea
The proof is a short tactic sequence. It invokes the upstream energy lemma ode_neg_energy_constant at the arbitrary point t, which supplies the invariant f(t)² + (deriv f t)² equal to its value at zero. The initial conditions reduce the right-hand side to zero. Non-negativity of both squares, linarith, and nlinarith then force each square to vanish, hence f(t) = 0.
why it matters
The lemma supplies the zero-initial-data case required by the downstream theorem ode_cos_uniqueness_contdiff, which itself feeds the master result THEOREM_angle_coupling_rigidity. It closes the trivial-solution gap on the cosine branch, paralleling the corresponding step on the cost side, and supports the angle T5 uniqueness that selects cos under negative curvature. The result therefore anchors the angle half of the forcing chain (T5–T8) that derives spatial dimension and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.