IndisputableMonolith.Foundation.GeneralizedDAlembert
Module housing the continuous Aczél–Kannappan classification of d'Alembert solutions: any continuous H with H(x+y)+H(x-y)=2H(x)H(y) and H(0)=1 is 1, cosh, or cos. Recognition theorists cite it when discharging the continuous-combiner route for the cost functional. The argument bootstraps continuity to analyticity, derives a universal-coefficient ODE, and applies uniqueness.
claimEvery continuous $H:\mathbb{R}\to\mathbb{R}$ satisfying the d'Alembert equation $H(x+y)+H(x-y)=2H(x)H(y)$ with $H(0)=1$ is identically $1$, or of the form $\cosh(ax)$, or of the form $\cos(ax)$ for some $a\in\mathbb{R}$. The module also packages continuous-route independence, log-cost Aczél data, and mollifier $C^k$ approximation tools used on that route.
background
Recognition Science forces the cost functional through multiplicative consistency. Upstream, D'Alembert Inevitability shows that any cost $F:\mathbb{R}_+\to\mathbb{R}$ with the right composition law must obey the d'Alembert equation on a logarithmic change of variables; the equation is not an arbitrary modeling choice.
Aczél's smoothness theorem (Cost.AczelProof) upgrades any continuous solution $H$ of $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ to real-analyticity via an integration bootstrap (continuous to $C^\infty$ by an antiderivative representation). SmoothnessTop isolates the Mathlib step identifying $\mathrm{ContDiff},\top$ with $C^n$ for every finite $n$, so the main file does not treat that API fact as an axiom.
Within this module the continuous route is organized around log-cost Aczél data, continuous satisfaction of the laws of logic, mollified approximations (convolution with bump functions), and a polynomial-continuous side path. These feed the named classification theorem rather than standing as free axioms.
proof idea
The spine is the proved Aczél–Kannappan theorem for continuous solutions. Continuity is lifted to analyticity by the Aczél smoothness bootstrap. From analyticity one derives a universal-coefficient second-order ODE for $H$, then invokes ODE uniqueness to obtain the classical trichotomy: constant 1, hyperbolic cosine, or trigonometric cosine.
Supporting material builds the continuous-route infrastructure: log-cost data extracted from continuous positive costs, mollifier $C^k$ routes via convolution (existence and pointwise convergence), and continuous-route independence lemmas that keep the classification independent of auxiliary choices. The classification itself is assembled by reducing to the Cost-layer d'Alembert classification that packages integration bootstrap, ODE derivation, and uniqueness.
why it matters in Recognition Science
This module is the continuous half of the foundation that turns the Recognition Composition Law into a rigid cost shape. Downstream, AxiomDischargePlan treats the named continuous classification as a classical input to be reduced: the cosh case is already fully discharged by a dedicated continuous d'Alembert–cosh solution theorem, and the plan tracks what remains for the constant and cosine branches.
SecondDerivative records an obstruction on the continuous-combiner route: the residual second-derivative identity cannot follow from present hypotheses alone (the quartic log-cost $G(t)=t^4$ has $G''(0)=0$ but $G''(1)=12$). That obstruction explains why the classification and its smoothness ladder sit here rather than being collapsed into a single one-line axiom.
In the broader forcing chain, once continuous d'Alembert solutions are classified, the J-cost uniqueness step (T5: $J(x)=(x+x^{-1})/2-1$) and the self-similar fixed point $\varphi$ (T6) rest on a proved functional-equation disjunction instead of an imported special-function catalogue.
scope and limits
- Does not classify discontinuous or non-measurable d'Alembert solutions.
- Does not by itself force the physical J-cost; only the continuous trichotomy.
- Does not discharge the residual continuous-combiner second-derivative identity.
- Does not prove inevitability of d'Alembert; that lives in the Inevitability import.
- Does not select among cosh, cos, and constant 1 on physical grounds alone.
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