H_CauchyToExponential
plain-language theorem explainer
The continuous Cauchy functional equation asserts that any continuous positive f from reals to positives with f(0)=1 and f(t+u)=f(t)f(u) equals exp(λt) for some real λ. Recognition Science invokes this to classify d'Alembert solutions H in the unbounded cosh branch of the Aczél theorem. The declaration packages the textbook result as a Prop hypothesis whose intended reduction takes the logarithm to reach the additive Cauchy equation.
Claim. Suppose $f : ℝ → ℝ$ is continuous, satisfies $f(t) > 0$ for every real $t$, $f(0) = 1$, and $f(t + u) = f(t) · f(u)$ for all real $t, u$. Then there exists λ ∈ ℝ such that $f(t) = exp(λ t)$ for all $t$.
background
The module develops auxiliary functions for classifying continuous solutions to d'Alembert's equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1. Branch 1 applies when H exceeds 1 at some point: the auxiliary φ(t) = H(t) + √(H(t)² - 1) is then positive, equals 1 at 0, and multiplicative. The declaration states the consequence that φ must be exponential. From the module: 'Given a continuous d'Alembert solution H with H(0) = 1, the classification proceeds in two branches depending on whether H achieves values > 1: Branch 1 (cosh): If H(t₀) > 1 for some t₀, define φ(t) = H(t) + √(H(t)² - 1) Then φ satisfies Cauchy's multiplicative equation... which for continuous positive functions forces φ(t) = e^(λt), giving H(t) = cosh(λt).'
proof idea
Encodes the hypothesis as a universal statement over continuous positive multiplicative functions. The roadmap sets g(t) = log(f(t)), deduces additivity g(t+u) = g(t) + g(u) from multiplicativity, transfers continuity via the logarithm and square root, then applies the known result that continuous additive functions on the reals are linear.
why it matters
It supplies the exponential form needed for the cosh branch inside aczel_classification_conditional. The module selects this branch because the J-cost grows unboundedly so that H = 1 + J exceeds 1. It aligns with the forcing chain at T5 J-uniqueness and T6 phi as self-similar fixed point. The open question is whether Mathlib supplies a continuous exponential form lemma or a custom log reduction must be added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.