g_pos_off_zero
plain-language theorem explainer
The transformed J-cost g(t) = J(exp t) is strictly positive for every nonzero real t. Log-space analysts of recognition costs cite this to lock in the sign pattern that matches the quadratic log-ratio approximation while preserving the fixed point at unity. The proof is a direct reduction: unfold the definition then invoke the upstream positivity lemma for J away from 1, using that the exponential is positive and equals 1 only at t = 0.
Claim. Let $g(t) := J(e^{t})$ for real $t$. Then $g(t) > 0$ for all $t ≠ 0$.
background
The module proves that the J-cost, which has unique global minimum J(1) = 0 and satisfies J(x) = J(x^{-1}), remains convex and sign-consistent when pulled back to logarithmic coordinates t = ln x. In these coordinates the auxiliary function g(t) = J(e^t) satisfies g(0) = 0, even symmetry, and strict positivity off zero; the same properties hold for the quadratic h(t) = t²/2, which approximates g near the origin. The local setting is the ALEXIS closed-loop control identity that equates the original J-cost family with its log-ratio form.
proof idea
Unfold the definition of g, then apply the lemma Jcost_pos_of_ne_one at the point exp t. Supply the hypothesis that exp t is positive. The remaining subgoal is discharged by contradiction: assume exp t = 1, apply log to both sides, and obtain t = 0, contradicting the given t ≠ 0.
why it matters
This theorem supplies the positivity clause required by the downstream JCostLogSpaceCert record, which bundles the zero, even, and positive properties for both g and h. It thereby completes the structural identity underlying the ALEXIS note: J-cost and the log-ratio share the fixed point at unity, the inversion symmetry, and the strict sign pattern away from that point. The result sits inside the Recognition forcing chain after the definition of J and before the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.