xiMap_ne_zero
plain-language theorem explainer
The defect-coordinate map xiMap sends every real σ to a positive real via the exponential, hence never vanishes. Researchers bridging the Riemann xi functional equation to J-cost symmetry cite this to guarantee that defect coordinates support division and multiplication without singularity. The proof is a one-line application of the positivity result for xiMap.
Claim. For every real number $σ$, $exp(2(σ - 1/2)) ≠ 0$.
background
In the ξ(s)–J(x) bridge the defect-coordinate map is defined by xiMap(σ) := exp(2(σ − 1/2)). This sends the critical strip to the positive reals, with the critical line Re(s)=1/2 mapping to x=1, the unique minimum of the J-cost functional J(x)=(x + 1/x)/2 − 1. The module shows that the functional equation ξ(s)=ξ(1−s) corresponds exactly to the reciprocity J(x)=J(1/x) under this coordinate change.
proof idea
The proof is a one-line wrapper that applies the positivity theorem xiMap_pos σ and invokes the fact that every positive real is nonzero.
why it matters
This result is invoked in four downstream theorems: paired_zero_composition, rcl_defect_coordinates, xiMap_div_reflection and xiMap_mul_reflection. It ensures defect coordinates lie in the multiplicative group of positive reals so that the Recognition Composition Law can be stated without division-by-zero issues. It supports the module claim that the Riemann hypothesis is equivalent to zero J-cost on the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.