h_pos_off_zero
plain-language theorem explainer
The auxiliary function h in logarithmic coordinates is strictly positive for every nonzero real argument. Researchers developing the ALEXIS closed-loop control result would cite this to lock in the global-minimum sign pattern of the J-cost away from its fixed point at unity. The proof is a one-line wrapper that unfolds the definition of h and hands the resulting expression to the positivity tactic.
Claim. Let $h : ℝ → ℝ$ be the log-space representative of the J-cost. Then $h(t) > 0$ for every real $t ≠ 0$.
background
The module establishes the structural identities of the J-cost in log coordinates. The J-cost satisfies J(1) = 0 with a unique global minimum at x = 1 and obeys J(x) = J(x^{-1}). Setting t = ln(x) produces g(t) := J(e^t), which is even, vanishes at t = 0, and is positive for t ≠ 0; the function h is the corresponding positive representative sharing these properties with the log-ratio (1/2)(ln x)^2. The module documentation states that both families share the same fixed point, symmetry, and sign pattern, supplying the key identities for the ALEXIS closed-loop control result.
proof idea
The proof is a one-line wrapper. It unfolds the definition of h and applies the positivity tactic, which directly yields the strict inequality from the algebraic form of the expression.
why it matters
This declaration completes the sign-pattern component of the structural identity required by the ALEXIS closed-loop control result. It confirms that the J-cost and its log-ratio approximation share the same positivity away from the fixed point, consistent with T5 J-uniqueness in the forcing chain. The result sits alongside sibling theorems (h_nonneg, h_even, g_pos_off_zero) that together establish the full set of properties listed in the module note; no open scaffolding remains for this specific claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.