cosh_initials
plain-language theorem explainer
cosh_initials establishes that the hyperbolic cosine satisfies cosh(0) = 1 and its derivative vanishes at zero. Researchers proving T5 cost uniqueness cite it to fix the boundary conditions for the ODE H'' = H. The proof is a direct term-mode reduction that splits the conjunction and applies library facts on cosh and sinh at zero.
Claim. $cosh(0) = 1$ and $frac{d}{dx} cosh(x) big|_{x=0} = 0$
background
The module supplies lemmas for the T5 cost uniqueness proof. The shifted cost is defined by H(x) = J(x) + 1 = ½(x + x^{-1}), converting the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Upstream, CostAlgebra records that under this H the RCL becomes the standard d'Alembert equation.
proof idea
The term proof opens with constructor to split the conjunction. The first conjunct is discharged by simp using Real.cosh_zero. The second applies the known derivative formula Real.deriv_cosh and simplifies with Real.sinh_zero.
why it matters
This supplies the initial conditions H(0) = 1, H'(0) = 0 required to identify the unique solution of H'' = H as cosh, which identifies J(x) = cosh(log x) - 1 in the T5 step of the forcing chain. It directly supports the ODE Cosh Uniqueness claim referenced in the module and anchors the transition from the functional equation to the explicit cosh form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.