H_of_F
plain-language theorem explainer
H_of_F supplies the shifted log-lift of any cost function F by adding one to its log-coordinate representation G_of_F. Workers on the curvature gate cite it when moving from the metric ds² = G''(t) dt² to the d'Alembert form. The definition is a direct one-line algebraic shift that matches the convenience reparametrization already noted in the functional equation module.
Claim. Let $H(F,t) := G(F,t) + 1$, where $G(F,t) := F(e^t)$ denotes the log-coordinate reparametrization of the cost function $F$.
background
The Curvature Gate module requires the cost metric to possess constant nonzero curvature. In log coordinates the metric takes the form ds² = G''(t) dt² with G(t) = F(exp t). This distinguishes three cases: flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1, from the Recognition Composition Law), and spherical (G(t) = 1 - cos(t), excluded by non-negativity of F).
proof idea
One-line definition that applies the sibling G_of_F log-lift and adds the constant 1, reproducing the convenience reparametrization already recorded in Cost.FunctionalEquation.G.
why it matters
The definition supplies the shifted form required for d'Alembert analysis inside the curvature gate. It directly supports the hyperbolic case G(t) = cosh(t) - 1 that arises from the J-cost and the Recognition Composition Law, while the module as a whole rules out spherical curvature. This step reinforces the non-trivial curvature demanded by the forcing chain (T5-T8) and the requirement that recognition geometry be entangled rather than flat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.