continuous_combiner_finite_smoothness_to_top
plain-language theorem explainer
Finite-order smoothness of the log-derived cost for any comparison operator obeying the continuous laws of logic upgrades to full C^∞ smoothness. Workers assembling the continuous route-independence version of the Translation Theorem cite this step to close the smoothness bootstrap. The argument is a direct invocation of the general lemma that uniform finite-order ContDiff implies ContDiff at infinity.
Claim. Let $C$ be a comparison operator satisfying the continuous laws of logic. If for every natural number $n$ the map $tmapsto C(e^t,1)$ is of class $C^n$, then this map is of class $C^infty$.
background
The GeneralizedDAlembert module replaces the polynomial route-independence hypothesis of the Translation Theorem with mere continuity of the combiner, using the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation. A comparison operator is a map from pairs of positive reals to reals that encodes comparison cost; derivedCost fixes the second argument at 1, producing a function on positive ratios that is well-defined under scale invariance. SatisfiesLawsOfLogicContinuous is the structure requiring identity, non-contradiction, excluded middle, scale invariance, non-triviality, and ContinuousRouteIndependence in place of the earlier polynomial condition.
proof idea
This is a one-line wrapper that applies contDiff_top_of_contDiff_nat directly to the hypothesis that the derived cost in exponential coordinates has ContDiff of every finite order.
why it matters
The declaration supplies the top-level smoothness statement for the continuous-combiner log-cost and is invoked by continuous_combiner_log_smoothness_bootstrap. It completes the promotion from mollifier-derived finite-order control to the C^∞ input required by the continuous version of the Translation Theorem, supporting the framework's replacement of polynomial restrictions by the Aczél–Kannappan trichotomy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.