same_fixed_point
plain-language theorem explainer
g and h, defined as the J-cost and its log-ratio approximation in logarithmic coordinates, both vanish at the origin. Researchers establishing the shared fixed point for J-cost convexity in the ALEXIS closed-loop control setting would cite this identity. The proof is a direct term-mode conjunction of the separate zero evaluations for g and h.
Claim. Let $g(t) := J(e^t)$ where $J$ is the J-cost function, and let $h(t)$ be the log-ratio cost. Then $g(0) = 0$ and $h(0) = 0$.
background
The module proves structural properties of the J-cost in log space as described in the ALEXIS internal note. Here g is the composition g(t) = J(e^t) and h is the quadratic log-ratio approximation, both required to share the fixed point at t = 0 corresponding to x = 1. Upstream g_at_zero states that g(0) = J(e^0) = J(1) = 0, while h_at_zero follows by direct simplification of the definition of h.
proof idea
Term-mode proof that directly pairs the two zero theorems via the constructor for conjunction.
why it matters
This theorem supplies the shared zero property required by the downstream definition jCostLogSpaceCert, which bundles the zero, evenness, and positivity facts for both g and h. It completes one step of the structural identity showing that J-cost and the log-ratio (1/2)(ln x)^2 share the fixed point at x = 1, the same symmetry J(x) = J(x^{-1}), and the same sign pattern, as stated in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.