same_symmetry
plain-language theorem explainer
Both g(t) = J(exp(t)) and h(t) = (1/2)t^2 are even functions of the logarithmic coordinate t. Researchers citing the ALEXIS closed-loop control note would invoke this to confirm that the J-cost symmetry J(x) = J(x^{-1}) survives the change to log space. The proof is a one-line term that pairs the separate evenness results already established for g and for h.
Claim. $forall t in mathbb{R}, g(t) = g(-t) land h(t) = h(-t)$, where $g(t) := J(e^t)$ and $h(t) := frac12 t^2$.
background
The module develops the structural properties of the J-cost after the change of variable t = ln(x). The function g is defined by g(t) = J(exp(t)) and therefore inherits the fixed point g(0) = 0 together with the symmetry J(x) = J(x^{-1}). The companion function h is the quadratic log-ratio (1/2)t^2 that shares the same fixed point and sign pattern near the origin. The upstream lemma g_even obtains evenness of g by substituting exp(t) and exp(-t) into the known symmetry of J. The companion lemma h_even follows at once from the algebraic definition of h.
proof idea
The proof is a one-line term-mode wrapper. It abstracts over t and returns the ordered pair whose first component is the evenness statement for g at t and whose second component is the evenness statement for h at t.
why it matters
The result populates the JCostLogSpaceCert certificate that collects the zero, evenness and positivity properties for both g and h. That certificate in turn underwrites the claim in the ALEXIS note that the J-cost and the log-ratio share the same fixed point, the same symmetry J(x) = J(x^{-1}), and the same sign pattern. Within the Recognition framework the symmetry is the direct image of the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.