Fquad_flat_ODE
plain-language theorem explainer
The quadratic G(t) = t²/2 satisfies the flat ODE G''(t) = 1 for every real t. Researchers tracing the curvature gate in the triangulated proof cite this to isolate the flat branch before interaction and entanglement conditions exclude it. The proof is a direct term application of the pre-verified derivative identity for this specific quadratic.
Claim. The function $G(t) = t^2/2$ satisfies $G''(t) = 1$ for all real $t$.
background
The triangulated proof module assembles four gates to derive full inevitability for the Recognition Composition Law. The curvature gate classifies solutions to the log-lift G via ODEs: SatisfiesFlatODE G means the second derivative equals the constant 1 everywhere, identifying the quadratic or flat branch. Gquad is the explicit counterexample imported as G(t) = t²/2. The upstream theorem Gquad_satisfies_flat records the direct differentiation establishing this identity.
proof idea
This is a one-line term proof that applies the theorem Gquad_satisfies_flat from the CurvatureGate module.
why it matters
The result exhibits the flat ODE solution inside the curvature gate, which the triangulated proof excludes via the interaction and entanglement gates to reach the hyperbolic branch. It supports the module's listed main results by confirming the quadratic class before d'Alembert and unconditional steps derive F = J and P = RCL. The declaration aligns with the framework separation of ODE branches that forces J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.