ContinuousCombinerMollifierFiniteSmoothness
plain-language theorem explainer
ContinuousCombinerMollifierFiniteSmoothness packages the finite-order differentiability of the log-cost G(t) = derivedCost(C, exp t) for any comparison operator C obeying the continuous laws of logic. Analysts completing the mollifier bootstrap to full C^∞ smoothness cite it as the named residual input 1a that supplies derivative control on compact intervals. The declaration is a direct definition that quantifies the ContDiff predicate over every natural number order.
Claim. Let $C : ℝ → ℝ → ℝ$ satisfy the continuous laws of logic. Then the function $t ↦$ derivedCost$(C, e^t)$ belongs to $C^n(ℝ)$ for every $n ∈ ℕ$.
background
The module develops the continuous-combiner version of the laws of logic to relax the polynomial route-independence hypothesis in the Translation Theorem. A ComparisonOperator is a map ℝ → ℝ → ℝ that returns the cost of comparing two positive quantities. derivedCost extracts the scale-invariant cost by fixing the second argument at 1, yielding a function on positive ratios. SatisfiesLawsOfLogicContinuous augments the standard identity, non-contradiction, excluded-middle and scale-invariance axioms with ContinuousRouteIndependence, which replaces the earlier polynomial condition.
proof idea
This is a definition that directly states the universal quantification over n of the ContDiff predicate applied to the log-cost function. No lemmas or tactics are invoked; the body is the literal statement of finite-order smoothness.
why it matters
It supplies the finite_smoothness field of ContinuousCombinerAnalysisInputs and is consumed by continuous_combiner_log_smoothness_bootstrap to obtain the full ContDiff statement at infinity. The declaration therefore closes the analytic gap left after the mollifier construction, allowing the Aczél–Kannappan classification (continuous solutions are constant, cosh or cos) to replace the polynomial restriction in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.