IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation

   1import Mathlib
   2import Mathlib.Analysis.Calculus.Deriv.Basic
   3import Mathlib.Analysis.Calculus.MeanValue
   4import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
   5import IndisputableMonolith.Cost.FunctionalEquation
   6
   7/-!
   8# Angle Functional Equation: Cosine Branch of d'Alembert Uniqueness
   9
  10This module provides the "Angle T5" theorem: the cosine uniqueness proof for
  11angle coupling functions, mirroring the cosh uniqueness proof in `Cost.FunctionalEquation`.
  12
  13## The Forcing Chain for Recognition Angle
  14
  15The d'Alembert functional equation `H(t+u) + H(t-u) = 2·H(t)·H(u)` has two solution branches:
  16- **Cosh branch** (H'' = H): Forces J(x) = ½(x + 1/x) - 1 (the cost functional)
  17- **Cos branch** (H'' = -H): Forces H(θ) = cos(θ) (the angle coupling)
  18
  19The key difference is the **calibration**:
  20- Cost T5: `H''(0) = +1` selects cosh
  21- Angle T5: `H''(0) = -1` selects cos
  22
  23## Axioms (Aθ1–Aθ4) for Angle Coupling Rigidity
  24
  25- **Aθ1 (d'Alembert)**: H(t+u) + H(t-u) = 2·H(t)·H(u)
  26- **Aθ2 (Regularity)**: H is continuous (implies smooth by Aczél theory)
  27- **Aθ3 (Normalization)**: H(0) = 1 (and H is even, derived from d'Alembert)
  28- **Aθ4 (Calibration)**: H''(0) = -1 (negative curvature selects cos)
  29
  30## Main Results
  31
  32- `ode_cos_uniqueness`: The unique solution to f'' = -f with f(0) = 1, f'(0) = 0 is cos.
  33- `dAlembert_cos_solution`: d'Alembert + calibration H''(0) = -1 ⟹ H = cos.
  34- `THEOREM_angle_coupling_rigidity`: Master theorem packaging Aθ1–Aθ4 ⟹ H = cos.
  35
  36## References
  37
  38- Aczél, J. "Lectures on Functional Equations and Their Applications" (1966), Chapter 3
  39- Recognition Science: Geometric Necessity of Recognition Angle
  40-/
  41
  42noncomputable section
  43
  44namespace IndisputableMonolith
  45namespace Measurement
  46namespace RecognitionAngle
  47namespace AngleFunctionalEquation
  48
  49open Real
  50
  51/-! ## Part 1: ODE Uniqueness Infrastructure for f'' = -f
  52
  53The cosine branch requires solving the ODE f'' = -f instead of f'' = f.
  54We develop the parallel infrastructure here.
  55-/
  56
  57/-- Diagonalization of the ODE f'' = -f into complex exponential components.
  58
  59For f'' = -f, the characteristic equation is r² = -1, giving r = ±i.
  60The real-valued approach uses: if f'' = -f, then (f' - i·f)' = -i(f' - i·f).
  61In real terms, we use the energy method: E = f² + (f')² is constant. -/
  62theorem ode_neg_energy_constant (f : ℝ → ℝ)
  63    (h_diff2 : ContDiff ℝ 2 f)
  64    (h_ode : ∀ t, deriv (deriv f) t = -f t) :
  65    ∀ t, f t ^ 2 + (deriv f t) ^ 2 = f 0 ^ 2 + (deriv f 0) ^ 2 := by
  66  let E : ℝ → ℝ := fun s => f s * f s + deriv f s * deriv f s
  67  have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  68  have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
  69    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
  70    rw [contDiff_succ_iff_deriv] at h_diff2
  71    exact h_diff2.2.2
  72  have h_diff_deriv : Differentiable ℝ (deriv f) :=
  73    h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  74  have h_const : ∀ t, deriv E t = 0 := by
  75    intro t
  76    have hE :
  77        deriv E t =
  78          deriv (fun s => f s * f s) t + deriv (fun s => deriv f s * deriv f s) t := by
  79      unfold E
  80      apply deriv_add
  81      · exact (h_diff1.mul h_diff1).differentiableAt
  82      · exact (h_diff_deriv.mul h_diff_deriv).differentiableAt
  83    have hprod1 :
  84        deriv (fun s => f s * f s) t = deriv f t * f t + f t * deriv f t := by
  85      apply deriv_mul h_diff1.differentiableAt h_diff1.differentiableAt
  86    have hprod2 :
  87        deriv (fun s => deriv f s * deriv f s) t =
  88          deriv (deriv f) t * deriv f t + deriv f t * deriv (deriv f) t := by
  89      apply deriv_mul h_diff_deriv.differentiableAt h_diff_deriv.differentiableAt
  90    rw [hE, hprod1, hprod2, h_ode t]
  91    ring
  92  have hE_diff : Differentiable ℝ E := by
  93    unfold E
  94    exact (h_diff1.mul h_diff1).add (h_diff_deriv.mul h_diff_deriv)
  95  have h_is_const := is_const_of_deriv_eq_zero hE_diff h_const
  96  intro t
  97  specialize h_is_const t 0
  98  simpa [E, pow_two] using h_is_const
  99
 100/-- **Theorem (ODE Zero Uniqueness for f'' = -f)**:
 101The unique solution to f'' = -f with f(0) = 0 and f'(0) = 0 is f = 0. -/
 102theorem ode_zero_uniqueness_neg (f : ℝ → ℝ)
 103    (h_diff2 : ContDiff ℝ 2 f)
 104    (h_ode : ∀ t, deriv (deriv f) t = -f t)
 105    (h_f0 : f 0 = 0)
 106    (h_f'0 : deriv f 0 = 0) :
 107    ∀ t, f t = 0 := by
 108  intro t
 109  have hE := ode_neg_energy_constant f h_diff2 h_ode t
 110  have hzero : f t ^ 2 + (deriv f t) ^ 2 = 0 := by
 111    simpa [h_f0, h_f'0] using hE
 112  have hsq_nonneg : 0 ≤ f t ^ 2 := sq_nonneg (f t)
 113  have hderivsq_nonneg : 0 ≤ (deriv f t) ^ 2 := sq_nonneg (deriv f t)
 114  have hsq_zero : f t ^ 2 = 0 := by linarith
 115  nlinarith [hsq_zero]
 116
 117/-- cos satisfies the ODE cos'' = -cos. -/
 118theorem cos_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cos x)) t = -Real.cos t := by
 119  intro t
 120  have h1 : deriv (fun x => Real.cos x) = (fun x => -Real.sin x) := by
 121    funext x
 122    simpa using (Real.deriv_cos x)
 123  rw [h1]
 124  have hneg : deriv (fun x => -Real.sin x) t = -(deriv Real.sin t) := by
 125    simpa using (deriv_neg (f := Real.sin) (x := t))
 126  rw [hneg]
 127  simp [Real.deriv_sin]
 128
 129/-- cos has the correct initial conditions: cos(0) = 1, cos'(0) = 0. -/
 130theorem cos_initials : Real.cos 0 = 1 ∧ deriv (fun x => Real.cos x) 0 = 0 := by
 131  constructor
 132  · exact Real.cos_zero
 133  · rw [Real.deriv_cos]
 134    simp [Real.sin_zero]
 135
 136/-- **Theorem (ODE Cos Uniqueness)**: The unique solution to H'' = -H with H(0) = 1, H'(0) = 0 is cos. -/
 137theorem ode_cos_uniqueness_contdiff (H : ℝ → ℝ)
 138    (h_diff : ContDiff ℝ 2 H)
 139    (h_ode : ∀ t, deriv (deriv H) t = -H t)
 140    (h_H0 : H 0 = 1)
 141    (h_H'0 : deriv H 0 = 0) :
 142    ∀ t, H t = Real.cos t := by
 143  let g := fun t => H t - Real.cos t
 144  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
 145  have hg_ode : ∀ t, deriv (deriv g) t = -g t := by
 146    intro t
 147    have h1 : deriv g = fun s => deriv H s - deriv (fun x => Real.cos x) s := by
 148      ext s
 149      apply deriv_sub
 150      · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
 151      · exact Real.differentiable_cos.differentiableAt
 152    have h2 : deriv (deriv g) t = deriv (deriv H) t - deriv (deriv (fun x => Real.cos x)) t := by
 153      have hH_diff1 : ContDiff ℝ 1 (deriv H) := by
 154        rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
 155        rw [contDiff_succ_iff_deriv] at h_diff
 156        exact h_diff.2.2
 157      have hcos_diff1 : ContDiff ℝ 1 (deriv (fun x => Real.cos x)) := by
 158        simpa [Real.deriv_cos] using (Real.contDiff_sin.neg)
 159      rw [h1]
 160      apply deriv_sub
 161      · exact hH_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 162      · exact hcos_diff1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 163    rw [h2, h_ode t, cos_second_deriv_eq t]
 164    ring
 165  have hg0 : g 0 = 0 := by
 166    simp [g, h_H0, Real.cos_zero]
 167  have hg'0 : deriv g 0 = 0 := by
 168    have h1 : deriv g 0 = deriv H 0 - deriv (fun x => Real.cos x) 0 := by
 169      apply deriv_sub
 170      · exact (h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)).differentiableAt
 171      · exact Real.differentiable_cos.differentiableAt
 172    rw [h1, h_H'0, Real.deriv_cos]
 173    simp [Real.sin_zero]
 174  have hg_zero := ode_zero_uniqueness_neg g hg_diff hg_ode hg0 hg'0
 175  intro t
 176  have hgt := hg_zero t
 177  simp [g] at hgt
 178  linarith
 179
 180/-! ## Part 2: Regularity Hypotheses for Cosine Branch
 181
 182Mirror the structure from Cost.FunctionalEquation but for H'' = -H.
 183-/
 184
 185/-- **Regularity bootstrap for linear ODE f'' = -f.**
 186
 187For the linear ODE f'' = -f, if f is twice differentiable (in the sense that
 188deriv (deriv f) t = -f t holds pointwise), then f is automatically C².
 189
 190This is a standard result: linear ODEs with smooth coefficients have smooth solutions. -/
 191def ode_linear_regularity_bootstrap_hypothesis_neg (H : ℝ → ℝ) : Prop :=
 192  (∀ t, deriv (deriv H) t = -H t) → Continuous H → Differentiable ℝ H → ContDiff ℝ 2 H
 193
 194/-- **ODE regularity: continuous solutions.** -/
 195def ode_regularity_continuous_hypothesis_neg (H : ℝ → ℝ) : Prop :=
 196  (∀ t, deriv (deriv H) t = -H t) → Continuous H
 197
 198/-- **ODE regularity: differentiable solutions.** -/
 199def ode_regularity_differentiable_hypothesis_neg (H : ℝ → ℝ) : Prop :=
 200  (∀ t, deriv (deriv H) t = -H t) → Continuous H → Differentiable ℝ H
 201
 202/-- cos satisfies the ODE regularity bootstrap. -/
 203theorem cos_satisfies_bootstrap_neg : ode_linear_regularity_bootstrap_hypothesis_neg Real.cos := by
 204  intro _ _ _
 205  exact Real.contDiff_cos
 206
 207/-- cos is continuous. -/
 208theorem cos_satisfies_continuous_neg : ode_regularity_continuous_hypothesis_neg Real.cos := by
 209  intro _
 210  exact Real.continuous_cos
 211
 212/-- cos is differentiable. -/
 213theorem cos_satisfies_differentiable_neg : ode_regularity_differentiable_hypothesis_neg Real.cos := by
 214  intro _ _
 215  exact Real.differentiable_cos
 216
 217/-- ODE cosine uniqueness with regularity hypotheses. -/
 218theorem ode_cos_uniqueness (H : ℝ → ℝ)
 219    (h_ODE : ∀ t, deriv (deriv H) t = -H t)
 220    (h_H0 : H 0 = 1)
 221    (h_H'0 : deriv H 0 = 0)
 222    (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
 223    (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
 224    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
 225    ∀ t, H t = Real.cos t := by
 226  have h_cont : Continuous H := h_cont_hyp h_ODE
 227  have h_diff : Differentiable ℝ H := h_diff_hyp h_ODE h_cont
 228  have h_C2 : ContDiff ℝ 2 H := h_bootstrap_hyp h_ODE h_cont h_diff
 229  exact ode_cos_uniqueness_contdiff H h_C2 h_ODE h_H0 h_H'0
 230
 231/-! ## Part 3: d'Alembert Functional Equation → Cosine
 232
 233The d'Alembert equation H(t+u) + H(t-u) = 2H(t)H(u) with H(0) = 1 has two branches:
 234- H''(0) = +1 → H'' = H → H = cosh (used for cost functional)
 235- H''(0) = -1 → H'' = -H → H = cos (used for angle coupling)
 236-/
 237
 238/-- **Aczél's Theorem for cosine branch.**
 239
 240Continuous solutions to f(x+y) + f(x-y) = 2f(x)f(y) with f(0) = 1
 241are analytic. The calibration H''(0) = -1 selects cos(λx) with λ = 1. -/
 242def dAlembert_continuous_implies_smooth_hypothesis_neg (H : ℝ → ℝ) : Prop :=
 243  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) → ContDiff ℝ ⊤ H
 244
 245/-- **d'Alembert to ODE derivation (negative branch).**
 246
 247If H satisfies the d'Alembert equation and is smooth, then H'' = H''(0) · H.
 248With calibration H''(0) = -1, this gives H'' = -H. -/
 249def dAlembert_to_ODE_hypothesis_neg (H : ℝ → ℝ) : Prop :=
 250  H 0 = 1 → Continuous H → (∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) →
 251    deriv (deriv H) 0 = -1 → ∀ t, deriv (deriv H) t = -H t
 252
 253/-- cos satisfies the d'Alembert smoothness hypothesis. -/
 254theorem cos_dAlembert_smooth : dAlembert_continuous_implies_smooth_hypothesis_neg Real.cos := by
 255  intro _ _ _
 256  exact Real.contDiff_cos
 257
 258/-- cos satisfies the d'Alembert to ODE hypothesis. -/
 259theorem cos_dAlembert_to_ODE : dAlembert_to_ODE_hypothesis_neg Real.cos := by
 260  intro _ _ _ _
 261  exact cos_second_deriv_eq
 262
 263/-- cos satisfies the d'Alembert equation. -/
 264theorem cos_dAlembert : ∀ t u, Real.cos (t+u) + Real.cos (t-u) = 2 * Real.cos t * Real.cos u := by
 265  intro t u
 266  rw [Real.cos_add, Real.cos_sub]
 267  ring
 268
 269/-- **Main Theorem (d'Alembert Cosine Solution)**:
 270
 271d'Alembert equation + calibration H''(0) = -1 ⟹ H = cos.
 272
 273This is the "Angle T5" theorem, parallel to the "Cost T5" theorem
 274`dAlembert_cosh_solution` in `Cost.FunctionalEquation`. -/
 275theorem dAlembert_cos_solution
 276    (H : ℝ → ℝ)
 277    (h_one : H 0 = 1)
 278    (h_cont : Continuous H)
 279    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 280    (h_deriv2_zero : deriv (deriv H) 0 = -1)
 281    (h_smooth_hyp : dAlembert_continuous_implies_smooth_hypothesis_neg H)
 282    (h_ode_hyp : dAlembert_to_ODE_hypothesis_neg H)
 283    (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
 284    (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
 285    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
 286    ∀ t, H t = Real.cos t := by
 287  -- d'Alembert + calibration → ODE H'' = -H
 288  have h_ode : ∀ t, deriv (deriv H) t = -H t := h_ode_hyp h_one h_cont h_dAlembert h_deriv2_zero
 289  -- d'Alembert → H is even
 290  have h_even : Function.Even H := Cost.FunctionalEquation.dAlembert_even H h_one h_dAlembert
 291  -- Even + differentiable → H'(0) = 0
 292  have h_deriv_zero : deriv H 0 = 0 := by
 293    have h_smooth := h_smooth_hyp h_one h_cont h_dAlembert
 294    have h_diff : DifferentiableAt ℝ H 0 := h_smooth.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) |>.differentiableAt
 295    exact Cost.FunctionalEquation.even_deriv_at_zero H h_even h_diff
 296  -- Apply ODE uniqueness
 297  exact ode_cos_uniqueness H h_ode h_one h_deriv_zero h_cont_hyp h_diff_hyp h_bootstrap_hyp
 298
 299/-! ## Part 4: Master Theorem — Angle Coupling Rigidity (Aθ1–Aθ4)
 300
 301This packages the complete forcing chain for angle coupling.
 302-/
 303
 304/-- **Structure: Angle Coupling Axioms (Aθ1–Aθ4)**
 305
 306A function H : ℝ → ℝ is a valid angle coupling if it satisfies:
 307- Aθ1: d'Alembert functional equation
 308- Aθ2: Continuity (regularity)
 309- Aθ3: Normalization H(0) = 1
 310- Aθ4: Calibration H''(0) = -1 (selects cos branch)
 311-/
 312structure AngleCouplingAxioms (H : ℝ → ℝ) : Prop where
 313  /-- Aθ1: d'Alembert functional equation -/
 314  dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u
 315  /-- Aθ2: Continuity -/
 316  continuous : Continuous H
 317  /-- Aθ3: Normalization -/
 318  normalized : H 0 = 1
 319  /-- Aθ4: Calibration (selects cosine branch) -/
 320  calibrated : deriv (deriv H) 0 = -1
 321
 322/-- **Standard Regularity Bundle for Angle Coupling**
 323
 324Packages the Aczél theory hypotheses. -/
 325structure AngleStandardRegularity (H : ℝ → ℝ) : Prop where
 326  smooth : dAlembert_continuous_implies_smooth_hypothesis_neg H
 327  ode : dAlembert_to_ODE_hypothesis_neg H
 328  cont : ode_regularity_continuous_hypothesis_neg H
 329  diff : ode_regularity_differentiable_hypothesis_neg H
 330  boot : ode_linear_regularity_bootstrap_hypothesis_neg H
 331
 332/-- **THEOREM (Angle Coupling Rigidity / Angle T5)**:
 333
 334Any function satisfying axioms Aθ1–Aθ4 with standard regularity equals cos.
 335
 336This is the master theorem that makes the angle coupling "forced":
 337there is no freedom in the choice of H once the axioms are specified. -/
 338theorem THEOREM_angle_coupling_rigidity
 339    (H : ℝ → ℝ)
 340    (hAxioms : AngleCouplingAxioms H)
 341    (hReg : AngleStandardRegularity H) :
 342    ∀ t, H t = Real.cos t :=
 343  dAlembert_cos_solution H
 344    hAxioms.normalized
 345    hAxioms.continuous
 346    hAxioms.dAlembert
 347    hAxioms.calibrated
 348    hReg.smooth
 349    hReg.ode
 350    hReg.cont
 351    hReg.diff
 352    hReg.boot
 353
 354/-- cos satisfies all angle coupling axioms. -/
 355theorem cos_satisfies_axioms : AngleCouplingAxioms Real.cos where
 356  dAlembert := cos_dAlembert
 357  continuous := Real.continuous_cos
 358  normalized := Real.cos_zero
 359  calibrated := by
 360    have h : deriv (deriv (fun x => Real.cos x)) 0 = -Real.cos 0 := cos_second_deriv_eq 0
 361    rw [h]
 362    simp [Real.cos_zero]
 363
 364/-- cos satisfies standard regularity. -/
 365theorem cos_satisfies_regularity : AngleStandardRegularity Real.cos where
 366  smooth := cos_dAlembert_smooth
 367  ode := cos_dAlembert_to_ODE
 368  cont := cos_satisfies_continuous_neg
 369  diff := cos_satisfies_differentiable_neg
 370  boot := cos_satisfies_bootstrap_neg
 371
 372end AngleFunctionalEquation
 373end RecognitionAngle
 374end Measurement
 375end IndisputableMonolith
 376