continuous_log_cost_of_continuousOn_positive
plain-language theorem explainer
If a function F is continuous on the positive reals, then the reparametrized map t maps to F(exp t) is continuous on all reals. Analysts preparing continuous inputs for the Aczel equation in Recognition Science cite this lifting step when moving from positive-ratio costs to log-coordinates. The proof verifies that the exponential maps the reals into the positive domain and applies the standard composition rule for continuous functions on open sets.
Claim. If $F : (0,∞) → ℝ$ is continuous, then the function $t ↦ F(e^t)$ is continuous on $ℝ$.
background
The GeneralizedDAlembert module replaces the polynomial-degree-≤2 restriction in the Translation Theorem with mere continuity of the combiner. The Aczél–Kannappan classification states that a continuous H : ℝ → ℝ with H(0)=1 satisfying H(x+y)+H(x-y)=2H(x)H(y) must be constant 1, a hyperbolic cosine, or a trigonometric cosine. This theorem supplies the continuity lift from positive ratios to the log-coordinate cost G(t)=F(exp t) required for the continuous-combiner version of SatisfiesLawsOfLogicContinuous.
proof idea
The tactic proof first records that the exponential is continuous on the whole real line and maps into the positive reals. It then composes the given ContinuousOn F with this exponential via the composition lemma for continuous functions on open sets, converts the resulting ContinuousOn on the universe to a global Continuous, and simplifies the composition definition.
why it matters
The result is invoked by log_aczel_data_of_laws to produce the continuous log-coordinate Aczel data that feeds the smoothness bootstrap. It advances the module's Move 3 goal of discharging the polynomial hypothesis via the Aczél–Kannappan classification, allowing the continuous-combiner Law of Logic to replace the stricter polynomial case. It touches the open question whether continuity alone closes the full Law of Logic without finite pairwise polynomial closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.