xiMap_reflection
The defect-coordinate map satisfies xiMap(1 − σ) = 1 / xiMap(σ) for real σ. Researchers translating the completed Riemann xi functional equation into Recognition Science cost symmetry would cite this identity. The proof substitutes the exponential definition of xiMap, applies a ring identity to negate the exponent, and invokes exp(−y) = 1/exp(y).
claimLet the defect-coordinate map be defined by $x(σ) = exp(2(σ − 1/2))$. Then $x(1 − σ) = x(σ)^{-1}$.
background
The module translates the completed Riemann xi functional equation ξ(s) = ξ(1−s) into J-cost symmetry via the defect-coordinate map x = exp(2(Re(s) − 1/2)). Under this change of variables the critical line Re(s) = 1/2 maps to x = 1 (the unique minimum of J) and reflection s ↦ 1−s maps to x ↦ 1/x, realizing J(x) = J(1/x) as the same algebraic structure. The defect functional is defined to equal J for positive x.
proof idea
The term proof substitutes the definition of xiMap, rewrites the exponent 2((1−σ)−1/2) as −(2(σ−1/2)) by a ring calculation, and applies the exponential negation rule to obtain the reciprocal.
why it matters in Recognition Science
This identity is invoked by jcost_xiMap_functional_symmetry to obtain J-cost invariance under reflection, and by xiMap_mul_reflection and xiMap_div_reflection to derive the product-one and squared-quotient relations. It supplies the first main result listed in the module documentation, realizing the J-uniqueness property (T5) and the reciprocal symmetry required by the Recognition Composition Law in defect coordinates.
scope and limits
- Does not locate any zeros of the xi function.
- Does not assume or imply the Riemann hypothesis.
- Does not extend the identity to complex σ.
- Does not compute numerical values of xiMap.
Lean usage
rw [xiMap_reflection]formal statement (Lean)
61theorem xiMap_reflection (σ : ℝ) : xiMap (1 - σ) = (xiMap σ)⁻¹ := by
proof body
Term-mode proof.
62 simp only [xiMap]
63 rw [show 2 * ((1 : ℝ) - σ - 1 / 2) = -(2 * (σ - 1 / 2)) from by ring]
64 simp [Real.exp_neg]
65
66/-- The defect-coordinate map is strictly monotone on the strip. -/