continuous_combiner_log_smoothness_bootstrap
plain-language theorem explainer
The theorem shows that finite-order differentiability of the log-derived cost, supplied by mollifier estimates under a continuous Law of Logic, upgrades to full C^∞ smoothness. Analysts replacing the polynomial route-independence axiom with continuity in the Translation Theorem would cite it. The proof is a direct one-line application of the finite-to-top promotion lemma.
Claim. Let $C$ be a comparison operator satisfying the continuous laws of logic. Assume that for every finite $n$ the map $tmapsto$ derived cost of $C$ at $e^t$ is $C^n$. Then the same map is $C^infty$.
background
The GeneralizedDAlembert module discharges the polynomial route-independence hypothesis by continuity, invoking the Aczél–Kannappan classification of continuous d'Alembert solutions. SatisfiesLawsOfLogicContinuous is the structure that keeps the algebraic laws but replaces polynomial route independence with its continuous counterpart. ContinuousCombinerMollifierFiniteSmoothness packages the finite-order ContDiff certificates for the log-coordinate derived cost $G(t)=F(e^t)$ produced by the mollifier route.
proof idea
One-line wrapper that applies the upstream theorem continuous_combiner_finite_smoothness_to_top to the supplied finite-order hypothesis.
why it matters
The result completes the smoothness bootstrap for the continuous-combiner setting and supplies the finite-smoothness component of ContinuousCombinerAnalysisInputs. It is used by the bilinear classification theorem and by log_aczel_data_of_laws. The module doc states the intent: continuity of the combiner plus the Aczél–Kannappan trichotomy replaces the old polynomial-degree restriction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.