hyperbolic_not_flat
plain-language theorem explainer
The log-lift Gcosh of the hyperbolic cosine branch fails the flat ODE. Researchers tracing the Recognition Science forcing chain cite this result to exclude the flat solution once interaction is present. The proof is a direct one-line application of the Gcosh_not_flat lemma established in the CurvatureGate module.
Claim. Let $G(t) = G_F(t)$ denote the log-coordinate reparametrization $G_F(t) = F(e^t)$ of the functional $F$. Then $G(t) = 2^{-1}(e^t + e^{-t}) - 1$ does not satisfy the flat ODE condition $G'' = 0$.
background
The TriangulatedProof module assembles four gates that together force the Recognition functional equation. The Curvature Gate states that the log-lift $G$ obeys the hyperbolic ODE $G'' = G + 1$ precisely when the solution branch is hyperbolic. Gcosh is the concrete instance arising from the cosh branch, $G(t) = 2^{-1}(e^t + e^{-t}) - 1$, which satisfies $G'' = G + 1$ by direct differentiation. The module imports CurvatureGate, NecessityGates, EntanglementGate and FourthGate; the local setting is the quadrilateral diagram that routes interaction through entanglement to curvature and finally to the d'Alembert identity.
proof idea
The declaration is a one-line term proof that directly invokes the lemma Gcosh_not_flat from the CurvatureGate module.
why it matters
This result excludes the flat ODE branch inside the triangulated inevitability argument. It feeds the parent theorem full_inevitability_triangulated listed among the module siblings. In the Recognition Science framework it corresponds to the T5 J-uniqueness step and the T0-T8 forcing chain that selects the hyperbolic solution once interaction is enforced by the RCL. The declaration closes one side of the quadrilateral structure described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.