cosh_satisfies_bootstrap
plain-language theorem explainer
The hyperbolic cosine satisfies the regularity bootstrap hypothesis for the linear ODE f'' = f. Workers on the T5 J-uniqueness step in Recognition Science cite this to confirm that cosh meets the smoothness requirements inside the cost functional equation. The proof is a one-line term wrapper that assumes the pointwise second-derivative condition, continuity, and differentiability, then invokes the known C² property of cosh.
Claim. If ∀t ∈ ℝ, (d²/dt²) cosh(t) = cosh(t), then continuity and differentiability of cosh imply that cosh is twice continuously differentiable.
background
The module supplies helper lemmas for the T5 cost-uniqueness argument. The key upstream definition states: for the linear ODE f'' = f, if the second-derivative identity holds pointwise then continuity and differentiability of f automatically yield that f is C². This is presented as a standard consequence of linear ODEs with smooth coefficients having smooth solutions. The local setting is the functional-equation layer that precedes the explicit construction of J(x) = (x + x⁻¹)/2 − 1.
proof idea
Term-mode proof. The three antecedents of the bootstrap implication (pointwise second-derivative equation, continuity, differentiability) are introduced and the goal is discharged at once by the Mathlib fact Real.contDiff_cosh.
why it matters
The lemma supplies the required regularity check for the T5 J-uniqueness proof inside the cost functional equation. It guarantees that the candidate solution cosh satisfies the smoothness conditions needed to close the bootstrap step. In the Recognition Science chain this supports the transition from the functional equation to the self-similar fixed point phi and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.