SatisfiesFlatODE
plain-language theorem explainer
SatisfiesFlatODE encodes the flat curvature condition that a function G obeys the ODE G''(t) = 1 for every real t. Analysts of the curvature gate in Recognition Science cite this predicate when isolating the quadratic solution G(t) = t²/2 as the counterexample lacking interaction. The definition is introduced directly as a universal quantification on the second derivative.
Claim. A function $G : ℝ → ℝ$ satisfies the flat ODE when its second derivative equals one everywhere: $G''(t) = 1$ for all $t ∈ ℝ$.
background
The module formalizes the curvature gate: the cost metric must have constant nonzero curvature. In log coordinates the reparametrization G(t) = F(e^t) induces the line element ds² = G''(t) dt². Flat curvature (κ = 0) is defined by G'' = 1, producing the quadratic solution that the module contrasts with the hyperbolic case G(t) = cosh(t) − 1 from the recognition composition law and the spherical case ruled out by non-negativity.
proof idea
This is a direct definition of the predicate via universal quantification on the second derivative; no lemmas or tactics are applied.
why it matters
The definition supplies the flat case for the curvature gate theorems. It is used by curvature_gate_dichotomy to reduce the trichotomy to flat or hyperbolic, and by curvature_gate_main to conclude that non-negativity plus interaction forces the hyperbolic solution G(t) = cosh(t) − 1. In the Recognition framework it isolates the flat (κ = 0) counterexample that lacks holistic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.