cos_satisfies_regularity
Cosine satisfies the standard regularity bundle for the angle branch of the d'Alembert functional equation. Researchers establishing uniqueness of angle coupling functions in Recognition Science cite this when closing the cos solution path. The proof assembles five pre-established component theorems into the AngleStandardRegularity structure via a direct term construction.
claimThe function $H=cos$ satisfies the standard regularity bundle: it is smooth, converts the d'Alembert equation into the ODE $H''=-H$, and meets the continuity, differentiability, and bootstrap hypotheses required by Aczél theory under the calibration $H''(0)=-1$.
background
AngleStandardRegularity packages the Aczél theory hypotheses for the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with negative curvature. The structure requires smoothness (continuous implies $C^∞$), conversion to the ODE $H''=-H$, plus continuity, differentiability, and linear regularity bootstrap conditions. This module develops the cosine branch parallel to the cosh branch in the Cost module, with axioms Aθ1–Aθ4 specifying the functional equation, regularity, normalization $H(0)=1$, and calibration $H''(0)=-1$ that selects cosine.
proof idea
The proof is a term-mode construction of the AngleStandardRegularity structure. It directly supplies the five fields: smooth from cos_dAlembert_smooth, ode from cos_dAlembert_to_ODE, cont from cos_satisfies_continuous_neg, diff from cos_satisfies_differentiable_neg, and boot from cos_satisfies_bootstrap_neg.
why it matters in Recognition Science
This result closes the regularity verification for the cosine solution, enabling the master theorem THEOREM_angle_coupling_rigidity that packages Aθ1–Aθ4 to conclude $H=cos$. It parallels the cosh uniqueness in the cost functional and supports the angle T5 step in the forcing chain, where negative curvature selects the trigonometric solution.
scope and limits
- Does not establish uniqueness of the solution to the functional equation.
- Does not derive the d'Alembert equation from more primitive axioms.
- Does not address the positive curvature cosh branch.
- Does not provide numerical verification or physical interpretation.
formal statement (Lean)
365theorem cos_satisfies_regularity : AngleStandardRegularity Real.cos where
366 smooth := cos_dAlembert_smooth
proof body
Term-mode proof.
367 ode := cos_dAlembert_to_ODE
368 cont := cos_satisfies_continuous_neg
369 diff := cos_satisfies_differentiable_neg
370 boot := cos_satisfies_bootstrap_neg
371
372end AngleFunctionalEquation
373end RecognitionAngle
374end Measurement
375end IndisputableMonolith