g
The definition recasts the J-cost as g(t) := J(exp(t)) to enable analysis in logarithmic coordinates. Researchers working on the ALEXIS closed-loop control result cite it to transfer fixed-point and symmetry properties from the original J-cost into log space. The declaration is a direct one-line composition with the exponential map and requires no lemmas.
claimDefine the function $g : ℝ → ℝ$ by $g(t) := J(e^t)$, where $J$ is the J-cost function with unique global minimum $J(1) = 0$.
background
The module studies the J-cost in log space following the ALEXIS internal note. The J-cost satisfies J(1) = 0, J(x) = J(x^{-1}), and is strictly positive for x ≠ 1. Changing variables to t = ln(x) produces the auxiliary function g(t) = J(e^t), which inherits the fixed point g(0) = 0 together with even symmetry and the same sign pattern. The note further records that near t = 0 the function behaves as g(t) ≈ t²/2, placing it in the same convex cost family as the log-ratio (1/2)(ln x)².
proof idea
The declaration is a one-line wrapper that composes the Jcost function with the real exponential.
why it matters in Recognition Science
The definition supplies the change-of-variables step required for the convexity and fixed-point analysis that supports the ALEXIS closed-loop control result. It directly implements the log-space translation of the J-uniqueness property (T5) and the shared fixed point at unity. Subsequent declarations in the same module (g_at_zero, g_even, g_pos_off_zero) rely on this coordinate shift to establish the evenness, positivity, and quadratic approximation properties.
scope and limits
- Does not prove convexity of g.
- Does not derive the quadratic approximation g(t) ≈ t²/2.
- Does not connect g to physical constants or spatial dimensions.
- Does not establish uniqueness of the minimum in log coordinates.
formal statement (Lean)
34noncomputable def g (t : ℝ) : ℝ := Jcost (Real.exp t)
proof body
Definition body.
35
36/-- g(0) = J(e⁰) = J(1) = 0. -/