h_nonneg
plain-language theorem explainer
The quadratic log-ratio function h(t) = t²/2 is non-negative for every real t. Workers on the ALEXIS closed-loop control and on the shared fixed-point properties between J-cost and log-ratio costs cite this result when bounding costs in log coordinates. The proof is a direct unfolding of h followed by an automated positivity check on the squared term.
Claim. For all real numbers $t$, $h(t) = t^2/2$ satisfies $h(t) >= 0$.
background
The module establishes the key structural identity for the ALEXIS closed-loop control result. As stated in 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 function g(t) = J(e^t) captures the transformed J-cost, while h(t) = t²/2 supplies the quadratic approximation. Both share the fixed point at t = 0, even symmetry, and positivity away from zero. The module has no upstream dependencies.
proof idea
The proof is a one-line wrapper. It unfolds the definition of h to expose the squared term and applies the positivity tactic, which automatically recognizes that t²/2 is nonnegative for all real t.
why it matters
This non-negativity lemma supports the JCostLogSpaceCert structure that packages the zero, even, and positive properties for both g and h. It is referenced in the construction of dimensionless identities such as lambda_rec_dimensionless_id and in chemical approximations like lj_minimum_approx. The result closes a basic step in the ALEXIS closed-loop control argument by confirming the sign pattern of the quadratic approximation, consistent with the Recognition Science landmarks of unique fixed point at x=1 and convexity in log space. It touches no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.