g_even
plain-language theorem explainer
The function g defined by g(t) := Jcost(exp t) is even. Researchers analyzing the log-space version of J-cost convexity cite this to confirm the required symmetry around the fixed point at t=0. The proof is a one-line wrapper that unfolds the definition of g, rewrites the negative exponential, and applies the inversion symmetry of Jcost.
Claim. Let $g(t) := Jcost(e^t)$. Then $g(t) = g(-t)$ for every real number $t$.
background
The J-Cost Convexity in Log Space module works in coordinates t = ln x. It defines g(t) := Jcost(exp t) so that the fixed point x=1 of the J-cost becomes the origin t=0. The module proves three structural facts for g: g(0)=0, g is even, and g(t)>0 for t≠0. These mirror the corresponding properties of the log-ratio cost (1/2)(ln x)^2, as noted in the module header: 'The log-ratio (1/2)(ln x)^2 is the same cost family; it is convex in log space with the same fixed point at x=1.'
proof idea
The proof unfolds the definition of g, replaces exp(-t) by its reciprocal via Real.exp_neg, and invokes the lemma Jcost_symm on the positive real number exp t. Jcost_symm states that Jcost x = Jcost x^{-1} whenever x>0, which directly yields the evenness after the substitution.
why it matters
g_even supplies the evenness clause inside the JCostLogSpaceCert structure, which also records the zero and positivity properties of both g and h. The same_symmetry theorem packages g_even together with the corresponding fact for h. This completes the symmetry component of the log-space certification that underpins the ALEXIS closed-loop control identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.