AngleStandardRegularity
plain-language theorem explainer
AngleStandardRegularity bundles the five Aczél-derived regularity conditions (continuous-to-smooth, ODE conversion, continuity, differentiability, linear bootstrap) for a map H in the cosine branch of the d'Alembert equation. Researchers working on angle coupling rigidity cite it when stating the hypotheses for the master uniqueness result. The declaration is a structure definition that simply collects these named properties.
Claim. A function $H : ℝ → ℝ$ satisfies the standard regularity bundle when it meets the d'Alembert continuous-implies-smooth hypothesis (negative branch), the d'Alembert-to-ODE hypothesis, the ODE continuous regularity hypothesis, the ODE differentiable regularity hypothesis, and the linear regularity bootstrap hypothesis.
background
The module develops the cosine branch of the d'Alembert functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$, contrasting it with the cosh branch that yields the cost functional J. Axioms Aθ1–Aθ4 are d'Alembert, continuity (which upgrades to smoothness), normalization $H(0)=1$, and calibration $H''(0)=-1$ that selects the cos solution. Upstream CostAlgebra.H reparametrizes the shifted cost as $H(x) = J(x) + 1$, while AczelProof.smooth and AczelTheorem.smooth supply the continuous-to-smooth bootstrap used in the negative branch.
proof idea
Structure definition that packages the five named hypotheses (dAlembert_continuous_implies_smooth_hypothesis_neg, dAlembert_to_ODE_hypothesis_neg, ode_regularity_continuous_hypothesis_neg, ode_regularity_differentiable_hypothesis_neg, ode_linear_regularity_bootstrap_hypothesis_neg) drawn from the Aczél regularity theory.
why it matters
It supplies the regularity interface required by THEOREM_angle_coupling_rigidity, the master result that forces any H obeying Aθ1–Aθ4 to equal cos. This realizes Angle T5 in the Recognition forcing chain, the negative-curvature counterpart to the J-uniqueness step T5 that selects cosh. The bundle closes the regularity scaffolding for the angle coupling and is instantiated by cos_satisfies_regularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.