`AngleStandardRegularity`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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

papers checked against this theorem

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