cos_initials
plain-language theorem explainer
The real cosine function satisfies the initial conditions cos(0) = 1 and its derivative at zero equals zero. Researchers establishing the cosine branch of the d'Alembert equation for angle coupling in Recognition Science cite this to fix the negative-curvature calibration. The proof is a direct term-mode application of standard trigonometric library facts.
Claim. $cos(0) = 1$ and the derivative of $cos(x)$ at $x=0$ equals zero.
background
This theorem belongs to the module on the cosine branch of d'Alembert uniqueness for angle coupling. The module contrasts the cosh branch (H'' = H, selecting the cost functional) with the cos branch (H'' = -H). Upstream, the shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into the standard d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The module axioms Aθ1–Aθ4 require the functional equation, continuity, H(0) = 1, and H''(0) = -1.
proof idea
The term-mode proof uses constructor to split the conjunction. The left conjunct applies the library fact Real.cos_zero. The right conjunct rewrites the derivative via Real.deriv_cos and simplifies with Real.sin_zero.
why it matters
This supplies the initial conditions for ode_cos_uniqueness in the same module, which supports dAlembert_cos_solution and the master theorem THEOREM_angle_coupling_rigidity packaging Aθ1–Aθ4. It completes the calibration step for the negative-curvature branch, parallel to the cosh uniqueness in Cost.FunctionalEquation and the T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.