flat_not_hyperbolic
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.