xiMap_strictMono
plain-language theorem explainer
The defect-coordinate map sending real part σ to exp(2(σ − 1/2)) is strictly increasing. Researchers bridging the Riemann xi function to the J-cost functional would cite this to confirm the coordinate change preserves order between the critical strip and positive reals. The proof is a direct one-line reduction to the strict monotonicity of the real exponential after applying linear arithmetic to the exponent difference.
Claim. The map $σ ↦ exp(2(σ − 1/2))$ is strictly monotone increasing on the reals.
background
The ξ(s)–J(x) Bridge module equates the completed Riemann xi functional equation ξ(s) = ξ(1−s) with J-cost reciprocal symmetry J(x) = J(1/x) via the defect-coordinate change x = exp(2(Re(s) − 1/2)). Under this map the critical line Re(s) = 1/2 corresponds to x = 1, the unique minimum of J, while reflection s ↦ 1−s corresponds to x ↦ 1/x. The upstream definition of xiMap supplies the explicit form exp(2(σ − 1/2)), and zeroDeviation supplies the aligned log-deviation 2(ρ.re − 1/2) that matches the RS defect scale. The PrimitiveDistinction.from result anchors the construction in seven axioms reduced to four structural conditions.
proof idea
The term proof introduces a < b, simplifies xiMap to obtain exp(2(a − 1/2)) and exp(2(b − 1/2)), then applies Real.exp_strictMono to the inequality 2(a − 1/2) < 2(b − 1/2) which linarith discharges immediately.
why it matters
This result secures the order-preserving character of the defect-coordinate map, a prerequisite for transferring monotonicity and ordering statements between the critical strip and the positive reals in the J-cost formulation. It supports the module's main results, including rh_equivalent_to_zero_cost (RH ↔ all zeros have J-cost zero) and rcl_defect_coordinates. Within the Recognition Science framework it reinforces the T5 J-uniqueness and the eight-tick octave by guaranteeing that the coordinate change does not invert inequalities when mapping zero locations onto the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.