continuous_combiner_log_smoothness_bootstrap
continuous_combiner_log_smoothness_bootstrap upgrades finite differentiability of the log-derived cost under continuous laws of logic to C^∞ smoothness. Researchers replacing the polynomial hypothesis in the d'Alembert translation theorem cite it to complete the bootstrap. The proof applies the finite-to-top promotion lemma in one step.
claimLet $C$ be a comparison operator. If $C$ satisfies the continuous laws of logic and the mollifier construction yields $C^n$ regularity for every finite $n$ on the map $tmapsto$ derivedCost$(C, e^t)$, then this map is $C^infty$ on $mathbb{R}$.
background
The GeneralizedDAlembert module replaces the polynomial route-independence hypothesis in the Translation Theorem with continuity alone. It invokes the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation to discharge the stronger polynomial-degree-≤-2 requirement. SatisfiesLawsOfLogicContinuous encodes the logic laws together with continuous route independence in place of the polynomial version. ContinuousCombinerMollifierFiniteSmoothness packages the statement that the mollifier route supplies ContDiff ℝ n for every finite n on the log-coordinate derived cost.
proof idea
The proof is a term-mode one-liner that invokes continuous_combiner_finite_smoothness_to_top on the inputs C, h, and hFinite.
why it matters in Recognition Science
This result supplies the top-level smoothness required by ContinuousCombinerAnalysisInputs, which then feeds continuous_combiner_bilinear_classification. It closes the smoothness bootstrap for log Aczel data extracted from continuous laws of logic, advancing the replacement of the polynomial axiom by continuity in the Recognition framework. The quartic-log counterexample shows that the second-derivative input in the analysis package remains a separate hypothesis.
scope and limits
- Does not derive the finite smoothness certificates from the laws alone.
- Does not guarantee bilinearity without the second-derivative input.
- Applies only when route independence is continuous.
- Does not classify solutions for non-smooth combiners.
formal statement (Lean)
517theorem continuous_combiner_log_smoothness_bootstrap
518 (C : ComparisonOperator)
519 (h : SatisfiesLawsOfLogicContinuous C)
520 (hFinite : ContinuousCombinerMollifierFiniteSmoothness C h) :
521 ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
522 (fun t : ℝ => derivedCost C (Real.exp t)) := by
proof body
Term-mode proof.
523 exact continuous_combiner_finite_smoothness_to_top C h hFinite
524
525/-- The second-derivative identity extracted from the smooth Aczél equation.
526The function `ψ` is morally `∂₂ P(u, 0)`. -/