curvature_gate_main
plain-language theorem explainer
Curvature gate theorem establishes that any non-negative even twice-differentiable G with G(0)=0 and G''(0)=1 satisfying a constant-curvature ODE must obey either the flat ODE G''=1 or the hyperbolic ODE G''=G+1. Recognition Science researchers cite it when selecting the geometry that yields the Recognition Composition Law from the cost functional. The proof uses case analysis on the three possible ODEs and obtains an immediate contradiction for the spherical case from the sign of G''(0).
Claim. Let $G : ℝ → ℝ$ be twice continuously differentiable and even, satisfying $G(0)=0$, $G''(0)=1$, $G(t) ≥ 0$ for all $t$, and one of the constant-curvature conditions $G''(t)=1$, $G''(t)=G(t)+1$, or $G''(t)=-(G(t)+1)$. Then $G$ satisfies either $G''(t)=1$ or $G''(t)=G(t)+1$.
background
The module introduces the curvature gate for the cost metric in log-coordinates, where $G(t)=F(e^t)$ and the metric is $ds^2 = G''(t) dt^2$. This distinguishes three constant-curvature geometries: flat ($κ=0$), hyperbolic ($κ=-1$), and spherical ($κ=+1$).
proof idea
The proof performs case analysis on the hypothesis that G satisfies one of the three ODEs. For the flat and hyperbolic cases the conclusion follows immediately by disjunction introduction. For the spherical case, evaluation of the ODE at t=0 together with G(0)=0 yields G''(0)=-1, which contradicts the calibration condition G''(0)=1; the proof closes with exfalso after rewriting the contradictory equalities.
why it matters
This declaration closes the curvature gate argument in the Foundation.DAlembert module, selecting the hyperbolic geometry that realizes the Recognition Composition Law from the cost functional. It directly supports the claim that non-negativity plus interaction forces the RCL solution G(t)=cosh(t)-1. In the broader framework it aligns with the forcing chain from T5 J-uniqueness through T6 phi fixed point, ruling out periodic spherical geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.