xiMap_strictMono
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not locate any zeros of xi or zeta.
- Does not prove the Riemann hypothesis.
- Does not extend the map to complex arguments.
- Does not incorporate the phi-ladder or mass formulas.
formal statement (Lean)
67theorem xiMap_strictMono : StrictMono xiMap := by
proof body
Term-mode proof.
68 intro a b hab
69 simp only [xiMap]
70 exact Real.exp_strictMono (by linarith)
71
72/-! ## §2. Connection to ZeroLocationCost -/
73
74/-- xiMap agrees with exp(zeroDeviation) from ZeroLocationCost. -/