`THEOREM_angle_coupling_rigidity`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation
domain: Measurement
line: 338 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation on GitHub at line 338.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.