IndisputableMonolith.Foundation.GeneralizedDAlembert
The GeneralizedDAlembert module delivers the Aczél–Kannappan classification of continuous solutions to the d'Alembert functional equation. Researchers deriving physics from cost functionals would cite it to justify analytic forms in the Recognition framework. The argument reduces the classification to the upstream result in Cost.AczelProof by combining smoothness bootstrap, inevitability, and ODE uniqueness.
claimEvery continuous function $H:ℝ→ℝ$ satisfying $H(x+y)+H(x-y)=2H(x)H(y)$ for all real $x,y$ with $H(0)=1$ is either the constant function 1, a hyperbolic cosine, or a trigonometric cosine.
background
This module sits in the Foundation layer and treats the d'Alembert equation as the unique form arising from multiplicative consistency of cost functionals. It imports AczelProof, whose doc states: Any continuous solution H : ℝ → ℝ of the d'Alembert functional equation H(t + u) + H(t - u) = 2 · H(t) · H(u) with H(0) = 1 is real analytic (ContDiff ℝ ⊤). The inevitability module supplies the derivation of the equation itself from cost axioms, while SmoothnessTop isolates the ContDiff ℝ ⊤ API and LogicAsFunctionalEquation frames the broader setting.
proof idea
The module organizes imports of analyticity from AczelProof, inevitability from DAlembert.Inevitability, and smoothness helpers. The central classification theorem reduces directly to dAlembert_classification in Cost.FunctionalEquation once continuity and the functional equation are verified via the imported lemmas.
why it matters in Recognition Science
The classification feeds the AxiomDischargePlan, which reduces the classical input aczel_kannappan_continuous_dAlembert and already discharges the cosh case via dAlembert_cosh_solution_aczel. It also supports SecondDerivative for obstruction analysis. The result closes the step from the unique cost equation to its continuous solutions, aligning with the framework's derivation of physics from the functional equation.
scope and limits
- Does not classify discontinuous solutions of the d'Alembert equation.
- Does not derive the d'Alembert equation from cost axioms.
- Does not compute explicit frequency parameters for the cosine or cosh cases.
- Does not address multi-variable or vector-valued generalizations.
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