Measurement Recognition Angle Angle Functional Equation Cos Satisfies Continuous

The cosine branch

The cosine function is the familiar wave that repeats every 2π and starts at 1 when its argument is 0. It also satisfies a less famous identity: for any two angles t and u, cos(t+u) + cos(t-u) equals 2·cos(t)·cos(u). This is the d'Alembert functional equation, named after Jean le Rond d'Alembert, who studied it in the 1740s while working on vibrating strings. The equation has many solutions, not just cosine. Any function built from exponential terms, such as cosh, also obeys it. The difference between the branches shows up in the second derivative at zero: cosh has positive curvature there, while cosine has negative curvature.

The declaration cos_satisfies_continuous_neg establishes one small piece of a larger proof: cosine itself is continuous. That fact is not surprising, but it matters because the proof strategy needs to move from continuity to smoothness, then from smoothness to a differential equation, and finally to uniqueness. The declaration confirms that cosine meets the continuity requirement for the negative-curvature branch. Its companion declarations show that cosine also satisfies the differentiability and smoothness requirements, and that it obeys the initial conditions cos(0) = 1 and cos'(0) = 0.

In Recognition Science, the framework models angle coupling through a function H that satisfies the d'Alembert equation together with three other axioms: H(0) = 1, H is continuous, and H''(0) = -1. The last condition, called calibration, selects the cosine branch rather than the cosh branch. The master theorem THEOREM_angle_coupling_rigidity packages these axioms and concludes that H must be exactly cos. The declaration in question is one of the regularity hypotheses that the master theorem requires; it verifies that cosine is continuous, so the proof can proceed.

The declaration does not claim that cosine is the only continuous solution of the d'Alembert equation. Without the calibration condition H''(0) = -1, other continuous solutions exist, including cosh and constant functions. It also does not claim that any function satisfying the four axioms must be cosine; that is the job of the master theorem, which uses this declaration as one ingredient. Finally, it does not claim anything about the physical meaning of the angle: the framework's bridge from recognition to physical angle measurement remains an open target.

What the declaration and its companions do establish is a clean uniqueness result: within the framework's axioms, the cosine branch is forced. A reader can now see why the framework's angle coupling is not a free choice. The structure of the d'Alembert equation plus the calibration condition leaves exactly one possibility, and cosine is it.

/-- cos is continuous. -/
theorem cos_satisfies_continuous_neg : ode_regularity_continuous_hypothesis_neg Real.cos := by
  intro _
  exact Real.continuous_cos

/-- **THEOREM (Angle Coupling Rigidity / Angle T5)**:

Any function satisfying axioms Aθ1–Aθ4 with standard regularity equals cos.

This is the master theorem that makes the angle coupling "forced":
there is no freedom in the choice of H once the axioms are specified. -/
theorem THEOREM_angle_coupling_rigidity
    (H : ℝ → ℝ)
    (hAxioms : AngleCouplingAxioms H)
    (hReg : AngleStandardRegularity H) :
    ∀ t, H t = Real.cos t :=
  dAlembert_cos_solution H
    hAxioms.normalized
    hAxioms.continuous
    hAxioms.dAlembert
    hAxioms.calibrated
    hReg.smooth
    hReg.ode
    hReg.cont
    hReg.diff
    hReg.boot

/-- cos satisfies the d'Alembert equation. -/
theorem cos_dAlembert : ∀ t u, Real.cos (t+u) + Real.cos (t-u) = 2 * Real.cos t * Real.cos u := by
  intro t u
  rw [Real.cos_add, Real.cos_sub]
  ring

What this page does not claim

Cosine is the only continuous solution of the d'Alembert equation without calibration. The declaration alone forces the angle coupling; the master theorem does that. The framework has derived the physical meaning of angle from recognition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/RecognitionAngle/AngleFunctionalEquation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: