Gspher_satisfies_spherical
plain-language theorem explainer
Gspher(t) = cos(t) - 1 obeys the spherical curvature ODE G''(t) = -(G(t) + 1). Workers on the curvature gate in Recognition Science cite this to classify candidate metrics before non-negativity constraints eliminate the spherical case. The proof is a direct verification that computes the first and second derivatives of cosine and substitutes into the target equation.
Claim. Let $G(t) := cos(t) - 1$. Then $d^2G/dt^2(t) = -(G(t) + 1)$ holds for every real $t$.
background
The Curvature Gate module requires that the cost metric, reparametrized as G(t) = F(exp t), has constant nonzero curvature. This yields three cases: flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1 from the Recognition Composition Law), and spherical (G(t) = cos(t) - 1). The spherical case produces periodic comparisons that violate non-negativity of the cost function F. SatisfiesSphericalODE is the predicate requiring that the second derivative satisfies G''(t) = -(G(t) + 1) for all t. Gspher is the explicit spherical candidate defined in the same module. This lemma depends on the reparametrization G from Cost.FunctionalEquation.
proof idea
The proof introduces the time variable t and establishes the first derivative of Gspher as -sin(t) by unfolding the definition and applying the derivative of cosine. It then differentiates again using the derivative of sine to obtain -cos(t) at the second order. Substitution into the unfolded Gspher and algebraic simplification via ring closes the equality.
why it matters
This result populates the curvature gate summary theorem, which contrasts the three geometries and shows that spherical geometry fails calibration at t=0. Within the Recognition framework it confirms that only the hyperbolic solution from the RCL survives the non-negativity requirement, forcing D=3 and the eight-tick structure downstream. The parent theorem curvature_gate_summary uses it to rule out periodic metrics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.