dAlembert_cosh_solution_aczel
plain-language theorem explainer
Continuous solutions of d'Alembert's functional equation with H(0)=1 and H''(0)=1 coincide with the hyperbolic cosine. Recognition Science researchers cite this to establish the explicit form of the shifted cost under the composition law. The argument first invokes Aczél smoothness to reach infinite differentiability, derives the ODE H''=H, and concludes via ODE uniqueness.
Claim. Let $H:ℝ→ℝ$ be continuous and satisfy $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, with $H(0)=1$ and $H''(0)=1$. Then $H(t)=cosh(t)$ for all real $t$.
background
In Recognition Science the shifted cost is $H(x)=J(x)+1$, where $J$ satisfies the Recognition Composition Law. Under this change of variable the RCL becomes d'Alembert's equation $H(t+u)+H(t-u)=2H(t)H(u)$. The module supplies supporting lemmas for the T5 uniqueness argument. The AczelSmoothnessPackage states that every continuous solution with $H(0)=1$ is $C^∞$. Upstream, dAlembert_to_ODE_theorem shows that the functional equation plus $H''(0)=1$ forces the ODE $H''=H$ everywhere.
proof idea
The term proof first applies aczel_dAlembert_smooth to obtain ContDiff ℝ ⊤ H, then uses dAlembert_even to establish evenness and even_deriv_at_zero to obtain H'(0)=0. It invokes dAlembert_to_ODE_theorem to derive the ODE H''=H, reduces to ContDiff ℝ 2 H, and finishes by applying ode_cosh_uniqueness_contdiff.
why it matters
This supplies the cosh identification required by washburn_uniqueness_aczel, which proves that the J-cost is the unique reciprocal cost obeying the composition law, normalization, calibration, and continuity. It fills the explicit-solution step in the T5 J-uniqueness forcing chain. The result also supports the downstream discharge lemmas aczel_kannappan_via_cases and cosh_rescaling_lemma in the AxiomDischargePlan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 43)
-
Perturbation around Koebe function closes Li-Keiper equations
"perturbation around Koebe function K(z)=z/(1-z)^2 yielding an = λ_tiny(n)/(n γ) < 1; recurrence λ_tiny(n) = 2 λ_tiny(n-1) - λ_tiny(n-2) (Eq. 9, Approximation A)"
-
200 ms sampling leaves legged balance error unchanged
"A = [cosh(ωτ) ω^{-1} sinh(ωτ); ω sinh(ωτ) cosh(ωτ)], r = 1/(k-1)+2 independent of λ,ω,τ inside gray area"
-
Cosine-sine functional equation gets new extensions
"We relate the solutions of (1.1),(1.5),(1.2),(1.6),(1.4),(1.8) to ... f(xy)=f(x)χ1(y)+χ2(x)f(y) ... solved by Stetkær [11]. ... solutions of the sine addition law f(xy)=f(x)g(y)+g(x)f(y)"
-
Classical granules show multiple Berry phases under nonlinear drive
"Eq. (3) ... regular perturbation technique ... u1 = u1,0 + ε u1,1 + ... amplitudes A1,n-1 expressed via γ1,γ2,γ3 and σi"
-
Finsler spacetimes split diffeomorphically under timelike completeness
"the p-d’Alembertian... is elliptic... yielding a simpler, alternative proof of the timelike splitting theorem"
-
User capacity scales as log of task SNR in HCI model
"The user’s capacity to process Bayesian surprise follows the logarithm of this SNR... C = b·log₂(S/N + 1)"
-
Moments estimator recovers edge weights in reinforced random walks
"the hyperbolic Gaussian density: p_β(φ)=…e^{−∑β_e(cosh(φ_i−φ_j)−1)}…"
-
Gradient bias creates two dynamical scaling laws in neural training
"logistic loss … Vλ(Δμ) = −1/λ (λΔμ − log 2 cosh(λΔμ))"
-
Identity equates persistence exponents at (a,H) and (a+2H-1,1-H)
"limiting correlation function ... cosh((H-1/2)t)/cosh(t/2) ... persistence exponent ... Statement 1.4"
-
Joint deblurring-segmentation model sustains Dice on degraded endoscopic views
"w_seg(t) = w_min + 1/2 (1-w_min)(1 + cos(π t / T)) ... cosine annealing-based loss scheduler (LoCoS)"
-
Cross-section detects holographic quantum critical point
"V(Ψ)=-6Cosh(Ψ), Z(Ψ)=Cosh^{γ/3}(3Ψ), Y(Ψ)=4Sinh²(Ψ) in the EMDA action"
-
Power-cosine filter prepares ground states at O(Δ^{-2} log(1/ε)) depth
"Vstep = (I + e^{-i H τ})/2 ; F(d) = [(I + e^{-i H τ})/2]^d ; |f(E_k)| = |cos(E_k τ /2)|^d with resonance E0 τ ≈ 0 (mod 2π) and gap suppression exp(-d Δ² τ² /8)"
-
Blocked local pumps reveal multipartite Bell nonclassicality
"P(A′,B′,C′)=2|g|⁶[1+cos(ϕA+ϕB+ϕC)] ... tuned to maximal destructive interference"
-
Reciprocal cost yields rank-one Hessian in log coordinates
"In logarithmic coordinates the potential depends only on the linear combination S=α·t, and the associated Hessian metric has rank one at every point... J(t)=cosh(∑α_i t_i)−1. Hence the Hessian matrix of J is ∇²J(t)=cosh(S)ααᵀ... rank(∇²J(t))=1."
-
Quantum LIF neurons cut weather forecast error 15% over classical
"The QLIF-CAST model encodes neuron excitation states as single-qubit quantum superpositions, driven by Rx rotation gates and T1 relaxation decay... αnew = sin²((ϕ+θinput)/2)"
-
von Neumann-Jordan constant extends to non-normable metrics
"Theorem 2: equivalences (midpoint convex ⇔ convex ⇔ positively homogeneous ⇔ absolutely homogeneous) for translation-invariant f; Theorem 13: metric parallelogram law and von Neumann-Jordan constant = 2^{1-σ/2}; Theorem 29: exact C_NJ for p-metrics under Clarkson inequality."
-
Exponential cutoff emerges in gravitational wave spectrum for smooth transitions
"using the Born approximation... smoothing the 'effective potential' with a linear/quadratic/cubic/quintic function... infinitely differentiable 'effective potential'... exponential suppression on small scales"
-
Quantum identities give formulas for molecular charge capacity
"the spectral decomposition of the density matrix (3) is written as ρ̂(γ;q) = Σ ω_M |Φ_M⟩⟨Φ_M| with Ξ(γ;q) = e^{−γN}[1 + 2 cosh(γq)]"
-
Skew-adaptive conformal prediction keeps validity with tilted intervals
"Cr(x)=[μ̂−rσ̂e−γ̂,μ̂+rσ̂eγ̂]; s(x,y)=max{(μ̂−y)+/(σ̂e−γ̂),(y−μ̂)+/(σ̂eγ̂)}; τ=arcsinh(z/2); width ratio (r*/r)cosh(γ̂(x))"
-
Hyperbolic space cuts volume distortion in 3D pose estimates
"Lorentzian-proximity logit: s_prox_ij = 1 + <q_i, k_j>_L / τ_h ... monotone-equivalent to geodesic distance d_L = arccosh(-<x,y>_L)"
-
Homotopy training lifts unrolled imaging PSNR by 2.5 dB
"We define a continuation path strategy to transition smoothly from the synthetic fidelity to the desired ill-posed problem... Theorem 1 (Smooth path of unrolled solutions). Under A1–A2 the fixed-point equation x=T_α(x) admits a unique solution x̂_α=fix(T_α) for every α∈[0,1]. The mapping α↦x̂_α lies in C^1[0,1] and obeys ∥x̂_α1−x̂_α2∥2≤τL/(1−β(1−τL))|α1−α2|."
-
Chaotic systems acquire linear phase winding in operator wavefunctions
"Krylov wavefunction φ_n(t_β) = sqrt[...] tanh[α(t_β)]^n / cosh[α(t_β)]^{2Δ} with phase θ_K(t) = Arg[tanh(α t_β)] and exponential decay exp(−2 n e^{-2α t} cos(α β/2))"
-
Weak long-range couplings trigger topological transitions
"h(k) = J1 + (J2 - J e^{-λ})e^{-ik} + J (cosh λ - cos k)^{-1} ..."
-
Randomized algorithm cuts oracle calls for ordered-norm load balancing
"We need and show that these have non-trivial stability properties... bounded gradient increase... ∇Ψ(x+y)≤exp(η∥y∥∞)·∇Ψ(x)"
-
Nested radicals of 2 prove pi is irrational
"by induction it follows that cos(π/2^{k+1}) = (1/2) c_k"
-
Pb-Pb v2 data reveal multiple particle sources
"¯ρ2(yt,φr)∝ exp{−m[cosh(yt− Δyt(φr))− 1]/T2} ... factored as ¯ρ2(yt, Δyt0)×F1×F2 with monopole and quadrupole boost components (Eqs. 3–4)"
-
Explicit Koenigs functions derived for Poisson branching
"The obtained explicit solutions contain the exponential Bell polynomials and the modified exponential-integral function Ein(z). ... Abel’s equation A(F(t,s))=f'(1)t+A(s) with integral ∫(λ−1)dx/(e^{−λ}e^{λx}−x)"
-
Tether aerodynamics solved in milliseconds for UAVs
"analytical method based on catenary theory with a uniform drag assumption... y = a*cosh((x-x0)/a) + y0"
-
Polar flow matching adapts graphs while preserving topology
"Hyperbolic (H, c <0 ):The volume expands exponentially, satisfying: lim R→∞ Vol(BH(R))/exp((d−1)√|c|R) =const>0. ... Theorem 4.2 ... gradient flows for structural preservation (∇rL) and semantic alignment (∇θL) are orthogonal under the Riemannian metric: ⟨∇rL,∇θL⟩g=0."
-
Local Bernstein bounds extend Erdős lower bounds to short intervals
"Theorem 1.6 (Local Bernstein theory) … |f(x+iy)| ≤ A (1+O(e^{-πL/4y0})) cosh((1+O(1/(λ min(y0,L)))) λ y)"