hyperbolic_not_flat
plain-language theorem explainer
The theorem shows that the hyperbolic cost function Gcosh fails to satisfy the flat ordinary differential equation. A researcher closing the interaction-to-geometry path in Recognition Science would cite it to exclude the flat solution once the curvature gate is reached. The proof is a direct one-line application of the prior lemma Gcosh_not_flat.
Claim. Let $G(t) = F(e^t)$ be the log-lift of a functional $F$. Then the specific hyperbolic lift $G$ defined via $G(t) = e^t + e^{-t} - 2$ (equivalently $G(t) = 2Gcosh(t) - 2$) does not satisfy the flat ODE $G'' = 0$.
background
The TriangulatedProof module assembles four gates that together force the Recognition Composition Law. The curvature gate supplies the hyperbolic ODE $G'' = G + 1$ for the log-lift of the J-cost; the contrasting flat ODE $G'' = 0$ appears when interaction is absent. The functional reparametrization $G_F(t) := F(e^t)$ converts the original multiplicative equation into an additive ODE on the real line. Upstream, the lemma Gcosh_not_flat already records that the explicit hyperbolic solution violates the flat equation.
proof idea
The proof is a one-line wrapper that applies the lemma Gcosh_not_flat from the CurvatureGate module.
why it matters
This declaration rules out the flat branch for the hyperbolic cost function, completing one side of the quadrilateral that forces F = J and P = RCL. It directly supports the module's listed main results on J's log-lift satisfying the hyperbolic ODE while remaining non-flat. In the larger chain it helps close the path from the interaction gate through the curvature gate toward the unconditional inevitability theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.