cos_dAlembert
plain-language theorem explainer
The cosine function satisfies the d'Alembert functional equation H(t+u) + H(t-u) = 2 H(t) H(u) for all real t and u. Researchers deriving the angle coupling branch in Recognition Science cite this as the T5 step that selects cos under negative curvature calibration. The proof is a direct algebraic verification that expands the left-hand side via addition and subtraction formulas then normalizes with ring simplification.
Claim. $H(t+u) + H(t-u) = 2 H(t) H(u)$ holds for $H = $cos and all real $t,u$.
background
The module develops the cosine branch of the d'Alembert equation for angle coupling, mirroring the cosh branch in Cost.FunctionalEquation. The equation takes the form H(t+u) + H(t-u) = 2 H(t) H(u) with normalization H(0)=1; the calibration H''(0)=-1 selects the cosine solution, while H''(0)=+1 selects cosh. Upstream, CostAlgebra defines H(x) = J(x) + 1 = ½(x + x^{-1}), under which the Recognition Composition Law reduces to this d'Alembert identity. The parallel result dAlembert_cosh_solution assumes the positive second-derivative calibration to conclude the cosh form.
proof idea
The proof is a one-line term-mode wrapper. It introduces t and u, rewrites the left-hand side with the real cosine addition and subtraction lemmas, and finishes with the ring tactic for algebraic normalization.
why it matters
This supplies the d'Alembert axiom for the cosine function and feeds directly into cos_satisfies_axioms, which verifies that cos meets all angle coupling axioms Aθ1–Aθ4. It completes the Angle T5 step in the forcing chain, parallel to dAlembert_cosh_solution on the cost side. In the Recognition Science framework this selects the cosine branch via negative curvature, enabling the subsequent eight-tick octave and D=3 spatial dimension forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.