loglift_contDiff_of_cost_contDiff
plain-language theorem explainer
If a cost function from the reals to the reals is twice continuously differentiable, then the map obtained by composing it with the exponential remains twice continuously differentiable. Analysts working on regularity conditions inside cost-based recognition models cite the result to transfer smoothness across the change of variables that converts multiplicative ratios into additive logs. The argument is a direct one-line application of the composition rule for ContDiff maps together with the standard smoothness of the real exponential.
Claim. If $cost : ℝ → ℝ$ satisfies ContDiff $ℝ$ 2 $cost$, then the function $t ↦ cost(e^t)$ is also ContDiff $ℝ$ 2.
background
The module InevitabilityEquivalence bridges abstract inevitability slogans (zero-parameter, no alternatives) with concrete CPM cost conditions such as INEV_DIMLESS and INEV_ABSOLUTE. Cost functions enter as J-costs of recognition events or as derived costs of multiplicative recognizers; the log-lift replaces the positive-ratio argument by its logarithm, turning multiplicative structures into additive ones on the real line. Upstream results supply the relevant cost maps: the cost definition in ObserverForcing (Jcost of a recognition event) and the derivedCost in MultiplicativeRecognizerL4, together with the composition operation in CostAlgebra that preserves the underlying algebraic structure.
proof idea
The proof is a one-line wrapper that applies the composition lemma for ContDiff functions to the hypothesis hSmooth and the known fact that the real exponential map is ContDiff of all orders.
why it matters
The declaration supplies a technical regularity bridge required by the concrete side of the inevitability equivalence. It ensures that smoothness hypotheses placed on cost functions survive the log-lift that appears in the analysis of J-minima and the φ fixed-point. The result sits inside the module whose doc-comment states the master claim that abstract inevitability is equivalent to concrete cost/CPM conditions; it therefore supports the transfer of regularity statements into the forcing chain (T5–T8) without introducing extra parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.