rh_equivalent_to_zero_cost
plain-language theorem explainer
A complex number lies on the critical line precisely when the J-cost of its defect-coordinate image vanishes. Researchers linking the Riemann hypothesis to Recognition Science cost functionals would cite this equivalence. The tactic proof splits the biconditional and reduces each direction via the cosh identity for J-cost together with the uniqueness of the zero of J_log.
Claim. For a complex number $ρ$, the real part of $ρ$ equals $1/2$ if and only if the J-cost of the defect-coordinate image of that real part equals zero.
background
The module sets up the ξ(s)–J(x) Bridge: the completed Riemann xi satisfies ξ(s)=ξ(1−s) while J-cost satisfies J(x)=J(1/x). Under the defect-coordinate map x=e^{2(Re(s)−1/2)}, the critical line Re(s)=1/2 maps to x=1, the unique minimum of J. J_log(t) is defined as cosh(t)−1 and vanishes only at t=0 by the upstream theorem J_log_eq_zero_iff. The sibling result jcost_xiMap_eq_cosh states that J-cost on these coordinates equals cosh(2(σ−1/2))−1.
proof idea
Constructor splits the biconditional. Forward direction rewrites with jcost_xiMap_eq_cosh, then simplifies using the critical-line assumption to reach cosh(0)=0. Reverse direction rewrites the cost equation to obtain J_log(2*(re−1/2))=0, applies J_log_eq_zero_iff to conclude the argument is zero, and finishes by linarith.
why it matters
This is the fifth main result listed in the module documentation, establishing that the Riemann hypothesis is equivalent to all zeros having zero J-cost. It closes the algebraic identification between the classical functional equation and J-cost reciprocal symmetry, tying directly to J-uniqueness (T5) in the forcing chain. No downstream citations are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.