SatisfiesHyperbolicODE
plain-language theorem explainer
Recognition Science classifies log-reparametrized cost functions by the curvature of the induced metric, and this definition isolates the hyperbolic case G''(t) = G(t) + 1. Analysts working on the curvature gate or the forcing chain from RCL to J-cost cite it when separating hyperbolic from flat or spherical branches. The declaration is a direct equational definition with no lemmas or tactics required.
Claim. A function $G : ℝ → ℝ$ satisfies the hyperbolic ODE when $G''(t) = G(t) + 1$ for every real $t$.
background
The CurvatureGate module encodes the geometric requirement that the cost metric has constant nonzero curvature. In log coordinates the reparametrization $G(t) = F(e^t)$ produces the line element $ds^2 = G''(t) dt^2$, so the sign of $G'' - G$ distinguishes flat ($κ=0$), hyperbolic ($κ=-1$), and spherical ($κ=+1$) geometries. The module doc states that hyperbolic curvature corresponds to the ODE $G'' = G + 1$ whose solution is $G(t) = cosh(t) - 1$, matching the J-cost from the Recognition Composition Law.
proof idea
Direct definition of the second-order ODE condition; no lemmas are invoked and the body is simply the universal quantification of the equation $deriv (deriv G) t = G t + 1$.
why it matters
The definition is invoked by hyperbolic_ode_unique to conclude that the unique $C^2$ solution with $G(0)=0$ and $G'(0)=0$ is $cosh(t)-1$, which then feeds F_forced_to_Jcost and the gates_connected summary. It supplies the hyperbolic branch of the curvature gate, linking the RCL functional equation to d'Alembert structure and the downstream emergence of the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.