Measurement Recognition Angle Angle Functional Equation Cos Satisfies Differenti

A regularity step for the cosine

The cosine function is a standard object of calculus: the periodic wave that starts at 1, has slope 0 at the origin, and satisfies the differential equation f''(t) = -f(t). The declaration cos_satisfies_differentiable_neg is a formal statement about one of its regularity properties. It says that if the cosine satisfies its own differential equation, then the cosine is differentiable. This is a modest fact, but it is a necessary link in a longer proof chain.

The chain begins with the d'Alembert functional equation, H(t+u) + H(t-u) = 2·H(t)·H(u), which appears across mathematics wherever a function of a sum can be split into products of the parts. The equation has two smooth solution families: the hyperbolic cosine (cosh) and the ordinary cosine (cos). A second-derivative condition at zero selects the branch: H''(0) = +1 gives cosh, while H''(0) = -1 gives cos. The theorem dAlembert_cos_solution packages four axioms: the d'Alembert equation, continuity, normalization H(0) = 1, and the calibration H''(0) = -1. Under these hypotheses, the only possible solution is H(t) = cos(t).

The declaration in question is not the master theorem. It is one of five regularity hypotheses that the master theorem requires, each stating that a certain smoothness property follows from the differential equation. The differentiable property is the third of these. The proof is immediate: the cosine is known to be differentiable, so the implication holds. The declaration does not define the cosine, does not prove the d'Alembert equation, and does not by itself select the cosine branch. It only certifies one regularity step, and it does so for the specific function Real.cos, not for an arbitrary solution H.

In the Recognition Science framework, this lemma is part of the angle coupling rigidity theorem, which the framework uses to derive the cosine as the unique angle coupling function. The framework models the angle between two recognition events as a function that must satisfy the d'Alembert equation, and the calibration H''(0) = -1 selects the periodic cosine branch rather than the exponential cosh branch. The payoff is that the framework's angle structure is forced to be periodic, not merely smooth. The lemma itself is a small, verified step; the master theorem is what carries the conceptual weight.

/-- cos is differentiable. -/
theorem cos_satisfies_differentiable_neg : ode_regularity_differentiable_hypothesis_neg Real.cos := by
  intro _ _
  exact Real.differentiable_cos

/-- **Main Theorem (d'Alembert Cosine Solution)**:

d'Alembert equation + calibration H''(0) = -1 ⟹ H = cos.

This is the "Angle T5" theorem, parallel to the "Cost T5" theorem
`dAlembert_cosh_solution` in `Cost.FunctionalEquation`. -/
theorem dAlembert_cos_solution
    (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_cont : Continuous H)
    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
    (h_deriv2_zero : deriv (deriv H) 0 = -1)
    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis_neg H)
    (h_ode_hyp : dAlembert_to_ODE_hypothesis_neg H)
    (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
    (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
    ∀ t, H t = Real.cos t := by
  -- d'Alembert + calibration → ODE H'' = -H
  have h_ode : ∀ t, deriv (deriv H) t = -H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
  -- d'Alembert → H is even
  have h_even : Function.Even H := Cost.FunctionalEquation.dAlembert_even H h_one h_dAlembert
  -- Even + differentiable → H'(0) = 0
  have h_deriv_zero : deriv H 0 = 0 := by
    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt
    exact Cost.FunctionalEquation.even_deriv_at_zero H h_even h_diff
  -- Apply ODE uniqueness
  exact ode_cos_uniqueness H h_ode h_one h_deriv_zero h_cont_hyp h_diff_hyp h_bootstrap_hyp

/-- **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

What this page does not claim

This declaration does not prove that the cosine satisfies the d'Alembert equation; that is a separate theorem. This declaration does not by itself force the cosine branch; the calibration H''(0) = -1 is needed. This declaration does not define the cosine or prove its differentiability from scratch; it uses the known differentiability of Real.cos.

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: