IndisputableMonolith.Foundation.GeneralizedDAlembert
GeneralizedDAlembert assembles the Aczél–Kannappan classification for continuous solutions of the d'Alembert equation. Researchers deriving cost functionals from multiplicative consistency cite the module to obtain the constant-1, cosh, or cos cases. The structure reduces the classification to the integration bootstrap and ODE uniqueness lemmas imported from AczelProof and sibling modules.
claimEvery continuous solution $H:\mathbb{R}\to\mathbb{R}$ of $H(x+y)+H(x-y)=2H(x)H(y)$ with $H(0)=1$ equals the constant function 1, $\cosh(kx)$ for some $k$, or $\cos(kx)$ for some $k$.
background
The module sits inside the Foundation layer and imports DAlembert.Inevitability, which shows the d'Alembert equation is the unique form required by multiplicative consistency of any cost functional $F:\mathbb{R}_+\to\mathbb{R}$. It also imports AczelProof, whose integration bootstrap converts continuity into real-analyticity (ContDiff $\mathbb{R}$ $\top$), and SmoothnessTop, which isolates the Mathlib ContDiff API for the top smoothness level.
LogicAsFunctionalEquation supplies the surrounding context that cost functionals must obey the Recognition Composition Law. The module therefore treats the classification as a proved theorem rather than an axiom, wiring the imported smoothness and inevitability results into the disjunction of constant, hyperbolic, and trigonometric solutions.
proof idea
The module is an assembly layer rather than a self-contained proof. It reduces aczel_kannappan_continuous_dAlembert directly to the classification theorem in Cost.FunctionalEquation.dAlembert_classification. Helper definitions (mollified, polynomial_continuous, MollifierCkRoute) support the continuous-combiner route while SmoothnessTop supplies the finite-to-top smoothness step.
why it matters in Recognition Science
The module supplies the named theorem aczel_kannappan_continuous_dAlembert that AxiomDischargePlan uses to discharge classical inputs. It also feeds the second-derivative obstruction analysis in GeneralizedDAlembert.SecondDerivative. In the chain it closes the classification step that begins in LogicAsFunctionalEquation and leads to the cosh case already discharged by dAlembert_cosh_solution_aczel.
scope and limits
- Does not derive the d'Alembert equation without the inevitability module.
- Does not treat discontinuous solutions.
- Does not fix the constant $k$ from Recognition Science parameters.
- Does not address the quartic counterexample used in the second-derivative obstruction.
used by (2)
depends on (4)
declarations in this module (38)
-
theorem
aczel_kannappan_continuous_dAlembert -
def
ContinuousRouteIndependence -
structure
SatisfiesLawsOfLogicContinuous -
structure
LogAczelData -
theorem
continuous_log_cost_of_continuousOn_positive -
theorem
log_aczel_data_of_laws -
def
mollified -
theorem
mollified_continuous -
theorem
mollified_pointwise_tendsto -
def
MollifierCkRoute -
theorem
mollifierCkRoute_exists -
theorem
polynomial_continuous -
theorem
polynomial_implies_continuous -
theorem
laws_polynomial_implies_continuous -
def
LogBilinearIdentity -
def
ClassifiedLogCost -
theorem
log_zero_bilinear_identity -
theorem
log_parabolic_bilinear_identity -
theorem
log_cosh_sub_one_bilinear_identity -
theorem
log_one_sub_cos_bilinear_identity -
theorem
classified_log_cost_bilinear -
theorem
classified_positive_cost_bilinear -
theorem
log_bilinear_affine_lift_dAlembert -
theorem
log_bilinear_affine_lift_classification -
theorem
log_bilinear_positive_cost_bilinear -
def
ContinuousCombinerMollifierFiniteSmoothness -
theorem
continuous_combiner_finite_smoothness_to_top -
theorem
continuous_combiner_log_smoothness_bootstrap -
def
AczelSecondDerivativeIdentity -
def
PsiAffineOnImage -
def
ContinuousCombinerSecondDerivativeInput -
def
ContinuousCombinerPsiAffineCompletion -
structure
ContinuousCombinerAnalysisInputs -
theorem
continuous_combiner_psi_affine_forcing -
theorem
continuous_combiner_bilinear_classification -
theorem
continuous_combiner_bilinear -
theorem
RCL_is_unique_functional_form_of_logic_continuous -
theorem
laws_continuous_subsumes_polynomial