xiMap_at_half
plain-language theorem explainer
The defect-coordinate map sends the critical-line point 1/2 to the value 1. Researchers examining the Riemann hypothesis through Recognition Science cost functionals cite this to equate the critical line with the global minimum of J. The proof is a one-line simplification that unfolds the definition of the defect map.
Claim. Under the defect-coordinate change of variables $x = e^{2(Re(s)-1/2)}$, the map from the completed Riemann xi argument to the J-cost coordinate satisfies $x(1/2) = 1$.
background
The module sets up an exact algebraic bridge between the completed Riemann xi function, which obeys the functional equation ξ(s) = ξ(1−s), and the J-cost functional J(x) = (x + x^{-1})/2 − 1, which obeys J(x) = J(1/x). The change of variables is x = exp(2(Re(s) − 1/2)), so the critical line Re(s) = 1/2 is sent to x = 1, the unique minimum of J. The defect map is the concrete realization of this coordinate change inside the module.
proof idea
The proof is a one-line wrapper that applies simplification using the definition of the defect map.
why it matters
The result is invoked by the downstream theorem establishing that J-cost vanishes on the critical line. It supplies the concrete identification needed for the Recognition Science claim that the Riemann hypothesis is equivalent to all zeros having zero J-cost, realizing the functional reflection as reciprocal inversion in defect coordinates and aligning with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.