xiMap_reflection
plain-language theorem explainer
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).
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.