Encyclopedia Measurement Measurement Recognition Angle Angle Functional Equation Ode Cos Uniqueness Contd

ARTICLE 3 claims 2 theorems 1 model

Measurement Recognition Angle Angle Functional Equation Ode Cos Uniqueness Contd

A single differential equation, with two starting values, can have only one smooth solution: the familiar cosine function.

Verify this page

The cosine uniqueness theorem

The cosine function is the unique solution to a simple differential equation. The equation is f''(t) = -f(t), where f'' is the second derivative. The two starting values are f(0) = 1 and f'(0) = 0. The theorem ode_cos_uniqueness_contdiff states that if a function H is twice continuously differentiable, satisfies this equation for all real t, and has these two starting values, then H(t) = cos(t) for every real t. This is a standard result in the theory of ordinary differential equations, often proved by showing that the quantity H(t)^2 + H'(t)^2 is constant.

The result is part of a larger chain of reasoning in the Recognition Science framework. The framework models angle coupling, the strength of the angular relationship between two recognized events, as a function H that satisfies the d'Alembert functional equation H(t+u) + H(t-u) = 2·H(t)·H(u). This equation has two solution branches: the hyperbolic cosine branch, selected by the calibration H''(0) = +1, and the ordinary cosine branch, selected by H''(0) = -1. The theorem ode_cos_uniqueness_contdiff proves that the cosine branch is the only possible smooth solution under the negative calibration. The framework's library of machine-checked formal theorems contains this proof, along with the companion result that the hyperbolic cosine branch is forced by the positive calibration.

The theorem does not claim that the d'Alembert equation alone forces the cosine. Without the calibration condition H''(0) = -1, the equation admits a family of solutions, including the hyperbolic cosine. It also does not claim that the cosine function is the only solution to the differential equation without the regularity condition of twice continuous differentiability. Pathological solutions exist if the regularity condition is dropped. The theorem is a uniqueness result within a precisely stated set of assumptions: the differential equation, the two initial conditions, and the smoothness condition.

In the framework, this theorem is one step in forcing the recognition angle to be the ordinary angle of Euclidean geometry. The angle coupling function, once forced to be the cosine, means that the angle between two recognized events behaves exactly as the angle between two lines in a plane. This is a structural result: it does not by itself determine the numerical value of any physical constant, nor does it specify how recognition events are linked into spatial dimensions. Those are separate steps in the framework's forcing chain.

THEOREM ode_cos_uniqueness_contdiff · IndisputableMonolith/Measurement/RecognitionAngle/AngleFunctionalEquation.lean
ode_cos_uniqueness_contdiff · IndisputableMonolith/Measurement/RecognitionAngle/AngleFunctionalEquation.lean:136 
/-- **Theorem (ODE Cos Uniqueness)**: The unique solution to H'' = -H with H(0) = 1, H'(0) = 0 is cos. -/
theorem ode_cos_uniqueness_contdiff (H : ℝ → ℝ)
    (h_diff : ContDiff ℝ 2 H)
    (h_ode : ∀ t, deriv (deriv H) t = -H t)
    (h_H0 : H 0 = 1)
    (h_H'0 : deriv H 0 = 0) :
    ∀ t, H t = Real.cos t := by
  let g := fun t => H t - Real.cos t
  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
  have hg_ode : ∀ t, deriv (deriv g) t = -g t := by
    intro t
    have h1 : deriv g = fun s => deriv H s - deriv (fun x => Real.cos x) s := by
      ext s
      apply deriv_sub
      · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
      · exact Real.differentiable_cos.differentiableAt
    have h2 : deriv (deriv g) t = deriv (deriv H) t - deriv (deriv (fun x => Real.cos x)) t := by
      have hH_diff1 : ContDiff ℝ 1 (deriv H) := by
        rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
        rw [contDiff_succ_iff_deriv] at h_diff
        exact h_diff.2.2
      have hcos_diff1 : ContDiff ℝ 1 (deriv (fun x => Real.cos x)) := by
        simpa [Real.deriv_cos] using (Real.contDiff_sin.neg)
      rw [h1]
      apply deriv_sub
      · exact hH_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
      · exact hcos_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
    rw [h2, h_ode t, cos_second_deriv_eq t]
    ring
  have hg0 : g 0 = 0 := by
    simp [g, h_H0, Real.cos_zero]
  have hg'0 : deriv g 0 = 0 := by
    have h1 : deriv g 0 = deriv H 0 - deriv (fun x => Real.cos x) 0 := by
      apply deriv_sub
      · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
      · exact Real.differentiable_cos.differentiableAt
    rw [h1, h_H'0, Real.deriv_cos]
    simp [Real.sin_zero]
  have hg_zero := ode_zero_uniqueness_neg g hg_diff hg_ode hg0 hg'0
  intro t
  have hgt := hg_zero t
  simp [g] at hgt
  linarith
MODEL AngleCouplingAxioms · IndisputableMonolith/Measurement/RecognitionAngle/AngleFunctionalEquation.lean
AngleCouplingAxioms · IndisputableMonolith/Measurement/RecognitionAngle/AngleFunctionalEquation.lean:304 
/-- **Structure: Angle Coupling Axioms (Aθ1–Aθ4)**

A function H : ℝ → ℝ is a valid angle coupling if it satisfies:
- Aθ1: d'Alembert functional equation
- Aθ2: Continuity (regularity)
- Aθ3: Normalization H(0) = 1
- Aθ4: Calibration H''(0) = -1 (selects cos branch)
-/
structure AngleCouplingAxioms (H : ℝ → ℝ) : Prop where
  /-- Aθ1: d'Alembert functional equation -/
  dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u
  /-- Aθ2: Continuity -/
  continuous : Continuous H
  /-- Aθ3: Normalization -/
  normalized : H 0 = 1
  /-- Aθ4: Calibration (selects cosine branch) -/
  calibrated : deriv (deriv H) 0 = -1
THEOREM dAlembert_cos_solution · IndisputableMonolith/Measurement/RecognitionAngle/AngleFunctionalEquation.lean
dAlembert_cos_solution · IndisputableMonolith/Measurement/RecognitionAngle/AngleFunctionalEquation.lean:269 
/-- **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

What this page does not claim

The theorem does not claim that the d'Alembert equation alone forces the cosine, without the calibration condition. The theorem does not claim that the cosine is the only solution without the twice continuous differentiability regularity condition. The theorem does not determine the numerical value of any physical constant or specify how recognition events link into spatial dimensions.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND