cos_satisfies_axioms
plain-language theorem explainer
The real cosine function satisfies the AngleCouplingAxioms structure, which requires the d'Alembert functional equation, continuity, normalization to 1 at zero, and second derivative -1 at zero. Recognition Science researchers cite this when selecting the trigonometric solution branch for angle coupling functions. The tactic proof directly populates each axiom field using dedicated lemmas for the functional equation and derivative identity together with standard library facts for continuity and value at zero.
Claim. The function $H(x) = x$ satisfies the angle coupling axioms: $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, $H$ is continuous, $H(0) = 1$, and the second derivative of $H$ at zero equals $-1$.
background
This module develops the cosine branch of the d'Alembert functional equation for angle coupling in Recognition Science. The AngleCouplingAxioms structure encodes Aθ1–Aθ4: the d'Alembert equation, continuity, normalization H(0)=1, and calibration H''(0)=-1 which selects the cosine solution over the hyperbolic one. Upstream, cos_dAlembert establishes the functional equation for cosine, while cos_second_deriv_eq shows that the second derivative satisfies the ODE cos'' = -cos. The normalized definition from NavierStokes is used only for the normalization field here. The local setting is the forcing chain for recognition angle, where the negative curvature calibration distinguishes the angle coupling from the cost functional J.
proof idea
The tactic proof constructs an instance of AngleCouplingAxioms for Real.cos by supplying each field. It uses the theorem cos_dAlembert to witness the d'Alembert property, Real.continuous_cos for continuity, Real.cos_zero for normalization, and for calibration applies cos_second_deriv_eq at zero followed by rewriting and simplification using cos_zero to obtain -1.
why it matters
This declaration verifies that cosine meets the axioms for the angle branch, mirroring the cosh uniqueness in the Cost.FunctionalEquation module. It supports the Angle T5 step in the forcing chain, where calibration H''(0)=-1 selects cos, leading toward the master theorem THEOREM_angle_coupling_rigidity. No open questions are directly touched, but it closes the verification for the cosine solution branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.