jcost_xiMap_eq_cosh
plain-language theorem explainer
The theorem equates J-cost at the defect coordinate xiMap(σ) to cosh(2(σ − 1/2)) − 1. Researchers linking the Riemann hypothesis to Recognition Science cost minima would cite it to translate zero locations into the J minimum at x = 1. The proof is a direct one-line substitution of the defect map into the exponential identity for J-cost.
Claim. For real σ let x = exp(2(σ − 1/2)) be the defect coordinate. Then the J-cost of x equals cosh(2(σ − 1/2)) − 1.
background
The ξ–J bridge treats the functional equation ξ(s) = ξ(1−s) as identical to the reciprocal symmetry J(x) = J(1/x) once coordinates are changed to the defect map. This map xiMap sends σ to exp(2(σ − 1/2)), carrying the critical line Re(s) = 1/2 to x = 1, the unique minimum of J. Jcost is the cost function induced by a multiplicative recognizer (equivalently the cost of any recognition event). Upstream, jcost_exp_eq_cosh states J(exp(t)) = cosh(t) − 1 directly from the definition of Jcost on exponentials.
proof idea
The proof is a one-line wrapper that applies jcost_exp_eq_cosh to the concrete argument 2(σ − 1/2) produced by xiMap.
why it matters
This supplies the explicit cosh expression that converts the J minimum at x = 1 into the statement that J-cost vanishes on the critical line. It is used by rh_equivalent_to_zero_cost to obtain the equivalence “RH holds if and only if every zero has zero J-cost.” In the Recognition framework it realizes T5 J-uniqueness (J(x) = cosh(log x) − 1) inside the critical-strip coordinates, confirming that the ξ functional equation is the same algebraic structure as J-cost reciprocal symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.