Measurement Recognition Angle Angle Functional Equation Theorem Angle Coupling R

The cosine rigidity theorem

The cosine function, cos(θ), is the familiar waveform that describes alternating current, pendulum motion, and the projection of a rotating vector. Its defining property is that its second derivative is the negative of the function itself: f''(θ) = -f(θ). This single differential equation, together with the starting conditions f(0) = 1 and f'(0) = 0, has exactly one solution, and that solution is cos(θ). This is the classical uniqueness theorem for the cosine, known since the development of ordinary differential equations in the eighteenth century.

The Recognition Science framework asks a stronger question: can the cosine be forced without assuming the differential equation at all? The answer, proved in the framework's machine-checked library of formal theorems, is yes. The theorem THEOREM_angle_coupling_rigidity starts from four axioms. The first is the d'Alembert functional equation, H(t+u) + H(t-u) = 2·H(t)·H(u), which expresses a symmetry between addition and subtraction of angles. The second is continuity, a standard regularity condition. The third is normalization, H(0) = 1. The fourth is calibration, H''(0) = -1, which selects the cosine branch rather than the hyperbolic cosine branch. From these four conditions alone, the theorem derives that H(θ) = cos(θ) for every real number θ.

The proof proceeds by showing that the d'Alembert equation plus continuity implies the function is smooth, then that the calibration condition forces the differential equation f'' = -f, and finally that this differential equation has the unique solution cos. The framework's library formalizes each step in the theorem dAlembert_cos_solution, which packages the full derivation. The result mirrors the framework's cost functional theorem, where the same d'Alembert equation with the opposite calibration H''(0) = +1 forces the hyperbolic cosine branch and hence the cost function J(x) = (x + 1/x)/2 - 1.

What the theorem does not claim is that any physical angle measurement must follow the cosine law. The theorem is a mathematical statement about functions satisfying the axioms; the physical interpretation of H as an angle coupling is a modeling choice, not a consequence of the proof. The theorem also does not claim that the cosine is the only continuous solution to the d'Alembert equation; without the calibration condition H''(0) = -1, other solutions exist. The calibration is the load-bearing assumption that selects the cosine branch, and the framework's contribution is showing that this single condition, together with the other three axioms, is sufficient to force the entire cosine function.

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

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

/-- **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 any physical angle measurement must follow the cosine law. The theorem does not claim that the cosine is the only continuous solution to the d'Alembert equation without the calibration condition. The theorem does not claim that the angle coupling axioms are derived from deeper physical principles within the framework.

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: