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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.