xiMap_pos
plain-language theorem explainer
The defect-coordinate map sending real σ to exp(2(σ - 1/2)) is strictly positive. Researchers bridging the Riemann xi functional equation to J-cost symmetry cite this to keep the image inside the positive reals where J is defined. The proof is a one-line application of the standard positivity of the real exponential.
Claim. For every real number $σ$, $0 < exp(2(σ - 1/2))$.
background
xiMap is the defect-coordinate map σ ↦ exp(2(σ - 1/2)). It sends the critical strip to the positive reals, with the line Re(s) = 1/2 mapping to x = 1, the unique minimum of J-cost. The module establishes that the completed xi functional equation ξ(s) = ξ(1-s) is algebraically identical to J(x) = J(1/x) under this coordinate change.
proof idea
One-line wrapper that applies the lemma Real.exp_pos.
why it matters
Positivity keeps the image of xiMap inside the domain of Jcost. It is invoked directly by jcost_xiMap_nonneg to obtain nonnegativity of J-cost on defect coordinates and by xiMap_ne_zero to exclude zero. In the Recognition framework this supports the bridge that equates the Riemann hypothesis with zero J-cost at the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.