AngleStandardRegularity
AngleStandardRegularity bundles the five regularity hypotheses required by Aczél theory for the negative-curvature branch of the d'Alembert equation. It collects smoothness from continuity, the ODE reduction, plus continuity, differentiability and bootstrap conditions so that any H obeying the angle axioms is forced to cosine. Recognition Science researchers cite the bundle inside the master uniqueness theorem for angle coupling. The declaration is a pure structure definition with no internal proof steps.
claimLet $H : ℝ → ℝ$. Then $H$ satisfies AngleStandardRegularity when the continuous-to-smooth implication holds for the negative d'Alembert equation, the d'Alembert equation reduces to the second-order ODE $H'' = -H$, and the ODE regularity conditions for continuity, differentiability and linear bootstrap are satisfied.
background
The module develops the cosine branch of d'Alembert uniqueness to complement the cosh branch used for the cost functional. In Recognition Science the equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ admits two calibrated solutions: the hyperbolic branch with $H''(0) = +1$ that recovers $J(x) = ½(x + x^{-1}) - 1$, and the trigonometric branch with $H''(0) = -1$ that recovers $H(θ) = cos(θ)$. AngleStandardRegularity packages the five Aczél hypotheses needed on the negative side, mirroring the positive-side bundle in Cost.FunctionalEquation.
proof idea
The declaration is a structure definition that simply assembles the five component hypotheses: dAlembert_continuous_implies_smooth_hypothesis_neg, dAlembert_to_ODE_hypothesis_neg, ode_regularity_continuous_hypothesis_neg, ode_regularity_differentiable_hypothesis_neg and ode_linear_regularity_bootstrap_hypothesis_neg. No lemmas or tactics are applied inside the structure itself.
why it matters in Recognition Science
AngleStandardRegularity supplies the regularity input to THEOREM_angle_coupling_rigidity, the master result that any $H$ obeying Aθ1–Aθ4 equals cos. This completes the Angle T5 step parallel to J-uniqueness on the cost side, closing the uniqueness argument for the angle coupling function once negative curvature is imposed. It is invoked directly by cos_satisfies_regularity to verify that the concrete cosine function meets the bundled conditions.
scope and limits
- Does not prove that any concrete function satisfies the five bundled hypotheses.
- Does not treat the positive-curvature d'Alembert branch or the cost functional J.
- Does not derive the d'Alembert equation or the calibration $H''(0) = -1$.
- Does not address existence of solutions beyond the uniqueness statement.
formal statement (Lean)
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. -/