curvature_gate_dichotomy
plain-language theorem explainer
The theorem establishes that any twice-differentiable G satisfying G(0)=0, G''(0)=1, and one of the three constant-curvature ODEs must obey either the flat ODE G''=1 or the hyperbolic ODE G''=G+1. Researchers formalizing the Recognition Science curvature gate cite it to exclude spherical geometry at the outset. The proof uses case analysis on the disjunction, returning the first two cases directly and deriving a numerical contradiction for the spherical case via substitution at t=0.
Claim. Let $G : ℝ → ℝ$ be twice differentiable with $G(0) = 0$ and $G''(0) = 1$. If $G$ satisfies the flat ODE $G''(t) = 1$ for all $t$, or the hyperbolic ODE $G''(t) = G(t) + 1$ for all $t$, or the spherical ODE $G''(t) = -(G(t) + 1)$ for all $t$, then $G$ satisfies either the flat or the hyperbolic ODE.
background
The module formalizes the curvature gate: the cost metric must have constant nonzero curvature. In log-coordinates $G(t) = F(e^t)$ the line element is $ds^2 = G''(t) dt^2$, yielding three constant-curvature solutions: flat ($G'' = 1$), hyperbolic ($G'' = G + 1$), and spherical ($G'' = -(G + 1)$). The spherical solution is ruled out by non-negativity of the underlying cost function $F$.
proof idea
The term proof performs case analysis on the disjunction that G satisfies one of the three ODEs. The flat and hyperbolic cases are returned immediately. For the spherical case, the assumption is instantiated at t=0; rewriting with G(0)=0 and G''(0)=1 produces the equation 1 = -1 after simplification, yielding exfalso.
why it matters
The result completes the curvature-gate step in the foundation layer: spherical geometry is eliminated by calibration, leaving only flat (additive counterexample) or hyperbolic (RCL-compatible) possibilities. The interaction gate is then invoked downstream to select the hyperbolic branch. It directly implements the module summary that constant nonzero curvature forces the Recognition Composition Law geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.