Gquad_not_hyperbolic
plain-language theorem explainer
The quadratic cost function fails to obey the hyperbolic curvature equation. Workers on the curvature gate in the Recognition Science framework cite this result to rule out flat metrics from the hyperbolic class. The proof assumes the ODE holds, checks consistency at t=0, then derives a numerical contradiction at t=1 by combining the flat second-derivative property with direct evaluation of the quadratic.
Claim. The function $G(t) = t^2/2$ does not satisfy the ODE $G''(t) = G(t) + 1$ for all real $t$.
background
Gquad is the quadratic function $t^2/2$ introduced as a counterexample in the DAlembert module. SatisfiesHyperbolicODE is the predicate requiring that the second derivative of a function G equals G plus one at every real point, which characterizes hyperbolic solutions. The module formalizes the curvature gate: the cost metric must have constant nonzero curvature, distinguishing flat space (G'' = 1, comparisons independent) from hyperbolic space (G'' = G + 1, entangled comparisons) and spherical space (ruled out by non-negativity). Upstream, Gquad_satisfies_flat establishes that this quadratic obeys the flat ODE G''(t) = 1.
proof idea
The term-mode proof assumes SatisfiesHyperbolicODE Gquad. It obtains the assumption at t=0 and recalls Gquad_satisfies_flat at t=0, where both sides equal 1. It then evaluates at t=1, applies Gquad_satisfies_flat at t=1, simplifies Gquad(1) = 1/2, and uses norm_num to reach the contradiction 1 = 3/2.
why it matters
This theorem is invoked directly by flat_not_hyperbolic in the TriangulatedProof module to establish mutual exclusivity of the flat and hyperbolic ODEs. It supports the curvature gate by excluding the flat counterexample from the hyperbolic class required by the Recognition Composition Law. In the framework this reinforces that recognition geometry must be non-trivially curved, consistent with the hyperbolic solution tied to J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.