THEOREM_angle_coupling_rigidity
plain-language theorem explainer
Any real-valued function H satisfying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u), continuity, normalization H(0)=1, and calibration H''(0)=-1 must equal the cosine function for all t. Recognition Science workers on the angle branch of the forcing chain cite this result to establish unique angle coupling. The proof is a direct one-line application of the d'Alembert cosine solution lemma to the bundled axioms and regularity hypotheses.
Claim. Let $H : ℝ → ℝ$ be continuous and satisfy $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, with $H(0)=1$ and $H''(0)=-1$. Then $H(t) = cos(t)$ for all real $t$.
background
The module treats the cosine branch of d'Alembert uniqueness, parallel to the cosh branch developed for the cost functional in Cost.FunctionalEquation. The d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) admits two smooth solution families distinguished solely by the sign of the second derivative at zero: positive curvature selects the hyperbolic cosine (cost side), while negative curvature selects the ordinary cosine (angle coupling).
proof idea
The proof is a one-line wrapper that applies dAlembert_cos_solution to H, supplying the normalized, continuous, dAlembert, and calibrated fields from the axioms bundle together with the smooth, ode, cont, diff, and boot fields from the regularity bundle.
why it matters
This is the master theorem (Angle T5) that forces the angle coupling to be exactly cosine once the four axioms are fixed, leaving no residual freedom. It mirrors the cost-side T5 uniqueness for the J-functional and completes the Recognition Angle segment of the forcing chain. The argument rests on Aczél regularity theory together with the explicit calibration H''(0)=-1 that selects the trigonometric branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.