g_at_zero
plain-language theorem explainer
The auxiliary function g, obtained by composing the J-cost with the exponential map, evaluates to zero at the origin. Researchers establishing shared fixed-point properties between the J-cost and its log-ratio approximation cite this base case. The proof is a direct unfolding of the definition of g followed by simplification with the unit lemma for the J-cost.
Claim. $g(0)=0$ where $g(t):=J(e^t)$ and $J(x)=(x-1)^2/(2x)$ satisfies $J(1)=0$.
background
The module proves structural identities for the J-cost in logarithmic coordinates, as motivated by the ALEXIS internal note on closed-loop control. The J-cost is given by $J(x)=(x-1)^2/(2x)$, which vanishes at the unit point by the upstream lemma Jcost_unit0. The auxiliary function g is defined by composition as $g(t)=J(e^t)$, mapping the fixed point $x=1$ to the origin $t=0$ in log space. This construction allows direct comparison with the quadratic log-ratio cost $h(t)=t^2/2$, which shares the same fixed point, symmetry, and sign pattern.
proof idea
The proof is a one-line wrapper that unfolds the definition of g and applies the lemma Jcost_unit0 stating Jcost 1 = 0.
why it matters
This theorem supplies the zero value required to build the JCostLogSpaceCert record, which bundles the fixed-point, evenness, and positivity properties for both g and h. It is also invoked directly by the same_fixed_point theorem. The result fills the base case of the structural identity between the J-cost and the log-ratio form that underlies the ALEXIS closed-loop control argument described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.