ContinuousCombinerMollifierFiniteSmoothness
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert that finite smoothness follows from continuity alone.
- Does not construct the mollifier family or prove pointwise convergence.
- Does not supply the second-derivative identity needed for bilinearity.
- Does not apply when route independence fails to be continuous.
formal statement (Lean)
493def ContinuousCombinerMollifierFiniteSmoothness
494 (C : ComparisonOperator)
495 (_h : SatisfiesLawsOfLogicContinuous C) : Prop :=
proof body
Definition body.
496 ∀ n : ℕ, ContDiff ℝ n (fun t : ℝ => derivedCost C (Real.exp t))
497
498/-- **Residual input 1b: finite-order smoothness promotes to full top-level
499smoothness for this log-cost.**
500
501Lean's `ContDiff` index used by Mathlib distinguishes the imported `⊤ : ℕ∞`
502from the outer `⊤ : WithTop ℕ∞` expected by downstream APIs. This input is the
503formal promotion step from the finite-order certificates produced by the
504mollifier route to the top-level smoothness statement consumed below. -/