Gcosh
plain-language theorem explainer
Gcosh supplies the explicit hyperbolic form of the cost function in log coordinates. Analysts deriving the d'Alembert equation or applying the curvature gate cite this definition to isolate the RCL solution from flat and spherical cases. The definition follows at once from the identity J(x) = cosh(log x) - 1.
Claim. Define the hyperbolic cost function by $G(t) := cosh(t) - 1$.
background
The CurvatureGate module requires the cost metric to have constant nonzero curvature. In log coordinates the reparametrization G(t) = F(exp t) yields the metric ds² = G''(t) dt², which distinguishes flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1), and spherical (G(t) = 1 - cos(t)) geometries. The upstream JCostInflaton result states that G(t) = J(e^t) = cosh(t) - 1 exactly, because J(x) = (x + x^{-1})/2 - 1 and ½(e^t + e^{-t}) = cosh(t).
proof idea
Direct definition that sets Gcosh(t) to Real.cosh t minus one, matching the closed-form expression for the J-cost in log coordinates.
why it matters
This definition anchors the hyperbolic branch inside curvature_gate_summary, which contrasts it with the flat counterexample and the ruled-out spherical case. It is invoked by analytic_bridge_full and gates_connected to close the chain from interaction to the recognition composition law and d'Alembert. In the framework it realizes the T5 J-uniqueness step and the forced hyperbolic curvature of the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.