pith. sign in
theorem

dAlembert_cosh_solution_aczel

proved
show as:

Why this theorem is linked from Deterministic Ground State Preparation via Power-Cosine Filtering of Time Evolution Operators echoes

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

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)

ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

module
IndisputableMonolith.Cost.FunctionalEquation
domain
Cost
line
1053 · github
papers citing
43 papers (below)

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)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.