Measurement Recognition Angle Angle Functional Equation

The angle functional equation

The angle functional equation is a mathematical rule that describes how angles combine. In plain terms, it states that the cosine of a sum of two angles plus the cosine of their difference equals twice the product of their individual cosines: cos(t+u) + cos(t-u) = 2·cos(t)·cos(u). This is the d'Alembert functional equation, named after Jean le Rond d'Alembert, who studied it in the 18th century. The equation is remarkable because it has only two families of continuous solutions: the hyperbolic cosine (cosh) and the ordinary cosine (cos).

The difference between the two branches comes down to a single number, the second derivative at zero. If that derivative is positive, the solution is cosh; if it is negative, the solution is cos. This is the calibration condition. In Recognition Science, the framework models measurement recognition, the process by which a system assigns a numerical value to an observed event, as a function that must satisfy this equation. The framework's library, a machine-checked collection of formal theorems, proves that when the calibration is negative, the only possible angle coupling function is the cosine.

The proof proceeds through several steps. First, the framework shows that any continuous solution to the d'Alembert equation is smooth, meaning it has derivatives of all orders. Then it converts the functional equation into an ordinary differential equation, f'' = -f, with initial conditions f(0) = 1 and f'(0) = 0. The framework proves that this differential equation has a unique solution, and that solution is the cosine. This is the theorem THEOREM_angle_coupling_rigidity, which packages the four axioms of the angle coupling function into the conclusion that H(t) = cos(t) for all t.

In Recognition Science, this result is called the Angle T5 theorem, and it mirrors the cost functional equation that forces the cost function J(x) = ½(x + 1/x) - 1. The two results together form a forcing chain: the same d'Alembert structure, with a different calibration, produces either the cost of recognition or the angle of measurement. The framework proves that the cosine is not chosen arbitrarily; it is the only function that satisfies the axioms. This means that within the framework, the geometry of angles is not a convention but a necessity.

What this establishes in plain language is that the standard trigonometric cosine is not one of many possible angle functions. Given the four axioms, continuity, normalization to 1 at zero, the d'Alembert composition law, and the negative curvature calibration, the cosine is forced. The framework's library verifies this proof with machine-checked precision, meaning every step is validated by a computer. The result is a rigorous foundation for why angles behave as they do, and it connects the measurement of angles to the same structural principles that govern the cost of recognition.

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

/-- ODE cosine uniqueness with regularity hypotheses. -/
theorem ode_cos_uniqueness (H : ℝ → ℝ)
    (h_ODE : ∀ t, deriv (deriv H) t = -H t)
    (h_H0 : H 0 = 1)
    (h_H'0 : deriv H 0 = 0)
    (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
  have h_cont : Continuous H := h_cont_hyp h_ODE
  have h_diff : Differentiable ℝ H := h_diff_hyp h_ODE h_cont
  have h_C2 : ContDiff ℝ 2 H := h_bootstrap_hyp h_ODE h_cont h_diff
  exact ode_cos_uniqueness_contdiff H h_C2 h_ODE h_H0 h_H'0

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

This answer does not claim that the angle functional equation is the only way to define angles in all of mathematics. This answer does not claim that the framework derives the fine-structure constant or any other specific physical constant from this equation. This answer does not claim that the d'Alembert equation has only the cosine and cosh as solutions without the continuity assumption.

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: