dAlembert_to_ODE_hypothesis_neg
plain-language theorem explainer
This definition packages the hypothesis that a continuous function H satisfying the d'Alembert equation with H(0)=1 and second derivative at zero equal to -1 must obey the ODE H''(t)=-H(t) everywhere. Researchers establishing cosine uniqueness for angle coupling in Recognition Science cite it as the reusable interface for the negative branch. The declaration is a direct Prop definition that downstream regularity bundles and solution theorems apply without further proof steps.
Claim. Let $H : ℝ → ℝ$. The predicate holds when $H(0)=1$, $H$ is continuous, $H(t+u)+H(t-u)=2 H(t) H(u)$ for all real $t,u$, and $H''(0)=-1$, implying $H''(t)=-H(t)$ for all $t$.
background
In the Angle Functional Equation module the cosine branch develops in parallel to the cosh branch for the cost functional. The upstream H from CostAlgebra is the shifted cost H(x)=J(x)+1, converting the Recognition Composition Law into the standard d'Alembert form H(xy)+H(x/y)=2 H(x) H(y). The companion H in Cost.FunctionalEquation supplies the analogous reparametrization on the cost side. The module states axioms Aθ1–Aθ4: d'Alembert, continuity, normalization H(0)=1, and calibration H''(0)=-1 to select the oscillatory solution.
proof idea
This is a definition that directly states the Prop combining normalization, continuity, the d'Alembert equation, and the second-derivative calibration at zero. It functions as a one-line interface; downstream results such as cos_dAlembert_to_ODE discharge it by invoking the known second derivative of cosine.
why it matters
The declaration supplies the hypothesis interface for the cosine uniqueness proof, feeding into AngleStandardRegularity (the bundled regularity structure) and dAlembert_cos_solution (the main Angle T5 theorem). It mirrors the positive-branch hypothesis on the cost side, completing the T5 step that selects cos over cosh via the negative calibration. This enforces the angle coupling required for the eight-tick octave and D=3 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.