structure
definition
AngleCouplingAxioms
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation on GitHub at line 312.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 :=