Gquad_satisfies_flat
plain-language theorem explainer
The quadratic reparametrization G(t) = t²/2 satisfies the second-order ODE G''(t) = 1 for all real t. Workers on the curvature gate in the Recognition Science foundation would cite this result to classify the additive counterexample as flat. The proof computes the derivatives explicitly using the power rule and confirms the second derivative equals the constant 1.
Claim. The function $G(t) := t^2/2$ satisfies $G''(t) = 1$ for every real $t$.
background
The Curvature Gate module requires the cost metric to have constant nonzero curvature, expressed in log coordinates via the second derivative of G(t) = F(e^t). Flat curvature corresponds to the ODE G''(t)=1, realized by the quadratic Gquad(t)=t²/2 from the counterexample. This contrasts with the hyperbolic case G''(t)=G(t)+1 from the Recognition Composition Law, and the spherical case ruled out by non-negativity of F.
proof idea
The proof introduces an arbitrary t, shows that the first derivative of Gquad equals the identity by applying hasDerivAt_pow to the squared term, dividing by the constant 2, and converting the result. It then rewrites the second derivative using this identity and applies the derivative of the identity function to obtain the constant 1.
why it matters
This result supplies the flat case for the curvature gate summary theorem, which contrasts Gquad (flat, additive) against Gcosh (hyperbolic, from RCL). It is invoked directly in Gquad_not_hyperbolic to separate the ODEs and in the triangulated proof to establish that Fquad fails the hyperbolic gate while J passes all four gates. Within the framework it marks the boundary between additive and interacting cost functions, consistent with the requirement that recognition geometry be non-trivially curved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.