curvature_gate_summary
plain-language theorem explainer
Curvature gate summary establishes that Gquad satisfies the flat ODE with G(0)=0 and G''(0)=1, Gcosh satisfies the hyperbolic ODE with matching initials, and Gspher satisfies its ODE but has G''(0)=-1. Recognition geometry researchers cite this to exclude spherical curvature and separate the additive counterexample from the RCL-derived hyperbolic case. The proof is a term-mode wrapper applying the individual ODE satisfaction lemmas and initial condition evaluations via simp.
Claim. Let $G_0(t) = t^2/2$, $G_+(t) = {cosh}(t) - 1$, $G_-(t) = {cos}(t) - 1$. Then SatisfiesFlatODE$(G_0) {wedge} G_0(0)=0 {wedge} G_0''(0)=1$, SatisfiesHyperbolicODE$(G_+) {wedge} G_+(0)=0 {wedge} G_+''(0)=1$, and SatisfiesSphericalODE$(G_-) {wedge} G_-(0)=0 {wedge} G_-''(0)=-1$.
background
The curvature gate requires the cost metric in log-coordinates to have constant nonzero curvature. Define $G(t) = F(e^t)$ so that the metric is $ds^2 = G''(t) dt^2$. Flat space uses $G_0(t) = t^2/2$ with $G''=1$ (independent comparisons, no interaction). Hyperbolic space uses $G_+(t) = {cosh}(t)-1$ with $G''=G+1$ (entangled comparisons, matching the Recognition Composition Law). Spherical space uses $G_-(t)={cos}(t)-1$ with $G''=-(G+1)$ (periodic but eventually negative, violating non-negativity).
proof idea
The proof is a term-mode wrapper. It refines the top-level conjunction into three blocks. The first block applies Gquad_satisfies_flat together with direct simp on the initial conditions. The second block applies Gcosh_satisfies_hyperbolic and rewrites using cosh(0)=1. The third block applies Gspher_satisfies_spherical and rewrites using cos(0)=1.
why it matters
This theorem summarizes the curvature distinctions that rule out spherical geometry by calibration mismatch at t=0 while linking the hyperbolic solution to the RCL and the flat solution to the additive counterexample. It supplies the geometric input to the interaction gate that selects hyperbolic over flat, advancing the forcing chain toward J-uniqueness. The module doc states that recognition geometry is non-trivially curved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.