h_at_zero
plain-language theorem explainer
The quadratic log-ratio approximation h to the J-cost satisfies h(0) = 0 in log coordinates. Researchers verifying the ALEXIS closed-loop control identities would cite this to confirm the shared fixed point between the exact J-cost and its approximation. The result supports the structural match noted in the module documentation for convexity in log space. The proof is a one-line simplification that evaluates the definition of h at zero.
Claim. Let $h(t) := t^2/2$. Then $h(0) = 0$.
background
The JCostConvexityInLogSpace module works in log coordinates t = ln(x) to compare the exact J-cost with its quadratic approximation. The function g(t) is defined as J(e^t), inheriting the unique minimum at t = 0 from J. The companion h(t) = t^2/2 is the log-ratio form that the module documentation identifies as belonging to the same cost family, convex in log space with the same fixed point at x = 1. This local setting is used to prove that both functions vanish at the origin, are even, and are positive off zero.
proof idea
The proof is a one-line wrapper that applies the definition of h and reduces the expression at zero by simplification.
why it matters
This theorem supplies the h_zero field for the jCostLogSpaceCert definition that bundles the zero, even, and positive properties of both g and h. It is also invoked in the same_fixed_point theorem to establish that g and h share the fixed point at t = 0. The result fills the structural identity required for the ALEXIS closed-loop control claim that J-cost and the log-ratio share the same minimum and symmetry, consistent with T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.