jCostLogSpaceCert
plain-language theorem explainer
The definition assembles a certificate that g(t) = J(exp t) and h(t) = t²/2 share a fixed point at t = 0, are even, and obey the sign conditions g(t) > 0 and h(t) ≥ 0 for t ≠ 0. Recognition Science researchers working on ALEXIS closed-loop control would cite it when invoking log-space convexity of the cost. It is constructed as a direct structure instance that references the individual lemmas g_at_zero, g_even, g_pos_off_zero, h_at_zero, h_even, h_nonneg, same_fixed_point, and same_symmetry.
Claim. Let $g(t) := J(e^{t})$ and $h(t) := t^{2}/2$. Then $g(0) = 0$, $g(t) = g(-t)$ for all real $t$, $g(t) > 0$ whenever $t ≠ 0$, $h(0) = 0$, $h(t) = h(-t)$ for all real $t$, $h(t) ≥ 0$ for all real $t$, and both functions share the fixed point at zero together with even symmetry.
background
This module establishes the log-space properties of the J-cost underlying the ALEXIS closed-loop control result. The function g is defined by g(t) := J(exp(t)), where J denotes the J-cost J(x) = (x + x^{-1})/2 - 1 with unique minimum J(1) = 0. The auxiliary function h(t) := t²/2 serves as the local quadratic approximation in log coordinates. From the module documentation: '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.' The certificate JCostLogSpaceCert collects the zero, evenness, positivity, and shared symmetry properties for both g and h. It relies on upstream results such as g_at_zero which states g(0) = J(1) = 0, g_even which follows from Jcost_symm, and g_pos_off_zero which uses Jcost_pos_of_ne_one.
proof idea
The definition is a direct structure constructor for JCostLogSpaceCert. It populates each field by referencing the corresponding pre-established lemma: g_zero from g_at_zero, g_even from g_even, g_positive from g_pos_off_zero, h_zero from h_at_zero, h_even from h_even, h_nonneg from h_nonneg, same_fixed_pt from same_fixed_point, and same_sym from same_symmetry. No additional reasoning is required beyond these references.
why it matters
This certificate supplies the structural properties required to invoke log-space convexity in the ALEXIS closed-loop control arguments. It directly supports the claim in the module documentation that J-cost and the log-ratio share the same fixed point, symmetry, and sign pattern. Within the Recognition Science framework it connects to the J-uniqueness property (T5) and the self-similar fixed point (T6) by confirming that the cost remains convex under the logarithmic change of variables. No downstream uses are recorded in the current module graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.