xiMap_eq_exp_zeroDeviation
plain-language theorem explainer
The map xiMap applied to the real part of any complex ρ equals the exponential of its zeroDeviation. Researchers linking the Riemann xi functional equation to J-cost symmetry in Recognition Science would cite this identity. The proof is a one-line simplification that unfolds the definitions of xiMap and zeroDeviation.
Claim. For any complex number $ρ$, the defect-coordinate map applied to the real part of $ρ$ equals the exponential of the zero-deviation of $ρ$, where the map sends $σ$ to $e^{2(σ-1/2)}$ and zero-deviation quantifies the J-cost distance from the critical line.
background
The module sets up the ξ(s)–J(x) bridge in which the completed Riemann xi satisfies ξ(s)=ξ(1−s) while J-cost satisfies J(x)=J(1/x). Under the coordinate change x=e^{2(Re(s)−1/2)}, the critical line Re(s)=1/2 maps to x=1 (the unique minimum of J) and functional reflection s↦1−s maps to x↦1/x. The defect functional is defined as defect(x):=J(x) for positive x, and zeroDeviation is the corresponding deviation measure imported from ZeroLocationCost. Upstream results supply the J-cost structures from PhiForcingDerived and the recognition-event cost from ObserverForcing.
proof idea
The proof is a one-line term-mode wrapper that applies simp with the definitions of xiMap and zeroDeviation, reducing both sides to the same expression.
why it matters
This identity supplies the explicit coordinate translation needed to restate the ξ functional equation as J-cost reciprocal symmetry. It directly supports the downstream claim that RH is equivalent to all zeros having zero J-cost, completing one of the five main results listed in the module. The step sits inside the Recognition Science forcing chain after T5 J-uniqueness and before the RCL in defect coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.