Gcosh_satisfies_hyperbolic
plain-language theorem explainer
The declaration verifies that Gcosh(t) := cosh(t) - 1 obeys the second-order ODE G''(t) = G(t) + 1 for all real t. Researchers tracing the curvature gate in Recognition Science cite it when showing that the recognition composition law selects hyperbolic geometry. The proof is a short tactic script that differentiates twice using the known rules for cosh and sinh, then closes with algebraic simplification.
Claim. Let $G(t) := {cosh}(t) - 1$. Then $G''(t) = G(t) + 1$ for every real number $t$.
background
The Curvature Gate module requires that the cost metric have constant nonzero curvature. In log coordinates the induced line element is $ds^2 = G''(t) dt^2$ where $G(t) = F(e^t)$. The hyperbolic case is defined by the ODE $G''(t) = G(t) + 1$, which is captured exactly by the predicate SatisfiesHyperbolicODE. The explicit function Gcosh is given by $Gcosh(t) = {cosh}(t) - 1$ and arises as the self-similar solution of the recognition composition law.
proof idea
The tactic proof begins by introducing an arbitrary real $t$. It proves that the first derivative of Gcosh equals sinh by unfolding the definition and invoking the derivative of cosh. The second derivative is obtained by differentiating sinh, producing cosh($t$). Unfolding Gcosh and applying the ring tactic then shows equality to Gcosh($t$) + 1.
why it matters
This result supplies the hyperbolic case required by curvature_gate_summary and is invoked verbatim in Jcost_hyperbolic_ODE and gates_consistent. It thereby closes the link from the recognition composition law to hyperbolic curvature, which the interaction gate then selects over the flat counterexample. In the larger framework the step supports the forcing chain that produces the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.