pith. machine review for the scientific record. sign in
def definition def or abbrev high

xiMap

show as:
view Lean formalization →

The defect-coordinate map sends real σ in the critical strip to the positive real x = exp(2(σ − 1/2)), placing the critical line σ = 1/2 at x = 1. Researchers bridging the Riemann xi functional equation to J-cost symmetry cite this map to convert reflection s ↦ 1−s into the reciprocal symmetry x ↦ 1/x under J. It is supplied as a direct definition with no lemmas or proof steps.

claimThe defect coordinate map is defined by $x(σ) := exp(2(σ − 1/2))$ for $σ ∈ ℝ$. This sends the critical line $σ = 1/2$ to $x = 1$ and converts functional reflection $σ ↦ 1−σ$ into reciprocal symmetry $x ↦ 1/x$ under the J-cost.

background

The module sets up the ξ(s)–J(x) bridge by equating the functional equation ξ(s) = ξ(1−s) with J(x) = J(1/x) under the coordinate change x = exp(2(Re(s) − 1/2)). The defect-coordinate map implements this change, sending the critical strip to the positive reals so that zero defect J(x) = 0 occurs exactly when x = 1. J-cost is the functional J(x) = (x + 1/x)/2 − 1 whose unique minimum is zero at x = 1. The map is constructed to be strictly positive and to satisfy the reflection property xiMap(1 − σ) = 1 / xiMap(σ).

proof idea

The declaration is a one-line definition: xiMap σ := Real.exp (2 * (σ - 1 / 2)). No lemmas are applied and no tactics are used; it simply encodes the exponential change of variable that aligns the critical strip with the positive reals under J-cost symmetry.

why it matters in Recognition Science

This definition supplies the coordinate bridge that lets the J-cost formalism reproduce the Riemann xi functional equation. It is used by jcost_xiMap_eq_cosh to recover J(e^{2η}) = cosh(2η) − 1, by rcl_defect_coordinates to verify the composition law in strip variables, and by rh_equivalent_to_zero_cost to equate the Riemann hypothesis with vanishing J-cost on all zeros. In the Recognition Science framework it realizes T5 J-uniqueness and the recognition composition law in the number-theoretic setting, linking the phi-ladder to the critical line.

scope and limits

formal statement (Lean)

  49def xiMap (σ : ℝ) : ℝ := Real.exp (2 * (σ - 1 / 2))

proof body

Definition body.

  50

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.