Gcosh_not_flat
plain-language theorem explainer
G(t) = cosh(t) - 1 fails the flat ODE G''(t) = 1. Curvature-gate workers in Recognition Science cite it to exclude flat geometry. The term proof assumes the ODE, substitutes the hyperbolic identity at t=1, and contradicts cosh(1) > 1 via linear arithmetic.
Claim. The function $G(t) = cosh(t) - 1$ does not satisfy $G''(t) = 1$ for all real $t$.
background
Module CurvatureGate formalizes the requirement that the cost metric possess constant nonzero curvature. The log-coordinate representation G(t) = F(e^t) yields the metric ds² = G''(t) dt². Flat curvature is characterized by the ODE G''(t) = 1, encoded in the definition SatisfiesFlatODE as the proposition that the second derivative equals 1 everywhere. Gcosh is the explicit map t ↦ cosh(t) - 1 drawn from the Recognition Composition Law. Its companion theorem establishes that this G satisfies the hyperbolic ODE G''(t) = G(t) + 1.
proof idea
The term proof begins by introducing the assumption that Gcosh satisfies the flat ODE. It specializes this assumption at the point t = 1. The hyperbolic satisfaction theorem is then applied at the same point to obtain an expression for the second derivative equal to cosh(1). The fact that cosh(1) exceeds 1 is invoked from real analysis, and linear arithmetic produces the contradiction.
why it matters
This theorem is directly invoked by hyperbolic_not_flat in the TriangulatedProof module, which connects the curvature gates to the broader forcing chain. It supports the assertion that recognition geometry must be hyperbolic, consistent with the self-similar fixed point and the eight-tick octave. The result closes the flat case for the RCL-derived G, leaving only the hyperbolic branch viable under the non-negativity constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.