flat_not_hyperbolic
Quadratic counterexample G(t) = t²/2 violates the hyperbolic ODE G'' = G + 1. Researchers assembling the four-gate inevitability argument cite it to separate the flat branch from the hyperbolic one before applying the d'Alembert gate. The argument reduces directly to the established non-hyperbolicity result for this G.
claimThe quadratic function defined by $G(t) := t^2 / 2$ fails to satisfy the ordinary differential equation $G''(t) = G(t) + 1$ for every real number $t$.
background
Gquad is the quadratic function $t^2/2$ introduced as a counterexample in the Counterexamples module and reused in CurvatureGate. SatisfiesHyperbolicODE is the predicate requiring that the second derivative of a function equals the function value plus one at every real argument. The TriangulatedProof module assembles the interaction, entanglement, curvature, and d'Alembert gates into a unified inevitability theorem, with the module documentation noting that the two ODEs are mutually exclusive.
proof idea
The proof is a one-line wrapper that applies the theorem Gquad_not_hyperbolic from the CurvatureGate module.
why it matters in Recognition Science
This declaration records the mutual exclusivity of the flat and hyperbolic ODEs, a prerequisite step listed in the module documentation for the triangulated proof. It supports the curvature gate by excluding the quadratic branch, allowing the argument to proceed to the hyperbolic solution $G = J$ and the unconditional derivation of the RCL combiner. The result sits inside the forcing chain that derives J-uniqueness and the eight-tick octave structure.
scope and limits
- Does not establish the hyperbolic ODE for any function other than the specific quadratic counterexample.
- Does not derive or invoke the d'Alembert identity.
- Does not incorporate interaction or entanglement conditions from the other gates.
- Does not address calibration, spherical solutions, or the full inevitability theorem.
formal statement (Lean)
118theorem flat_not_hyperbolic : ¬ SatisfiesHyperbolicODE Gquad := Gquad_not_hyperbolic
proof body
119