jcost_xiMap_nonneg
plain-language theorem explainer
J-cost is nonnegative on the image of the xi-map for every real parameter. Researchers bridging the Riemann xi functional equation to J-cost symmetry cite this to confirm nonnegativity throughout defect coordinates in the strip. The proof is a one-line wrapper applying the general J-cost nonnegativity lemma to the positivity of the xi-map image.
Claim. For every real number $σ$, the J-cost evaluated at the defect coordinate $x(σ)$ is nonnegative, where $x(σ)$ is the positive real given by the xi-map from the critical strip.
background
The XiJBridge module identifies the completed Riemann xi functional equation ξ(s) = ξ(1−s) with J-cost symmetry J(x) = J(1/x) under the defect coordinate map x = exp(2(σ − 1/2)), where σ = Re(s). J-cost is the functional J(x) = (x + x^{-1})/2 − 1 for x > 0, which equals the defect functional and is nonnegative by AM-GM with equality only at x = 1 (corresponding to the critical line Re(s) = 1/2). The module lists this nonnegativity as one of its main results supporting the full bridge, including rcl_defect_coordinates and rh_equivalent_to_zero_cost.
proof idea
This is a one-line wrapper that applies the upstream lemma Jcost_nonneg (J(x) ≥ 0 for x > 0, proved via squaring or AM-GM) directly to the positivity of xiMap σ established in the sibling result xiMap_pos.
why it matters
The result confirms J-cost remains nonnegative on all defect coordinates in the strip, directly supporting the equivalence of the Riemann hypothesis to zero J-cost at every zero (rh_equivalent_to_zero_cost from the module). It instantiates T5 J-uniqueness and the Recognition Composition Law in strip coordinates, closing part of the algebraic identification between the xi functional equation and J-cost reciprocal symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.