rh_equivalent_to_zero_cost
plain-language theorem explainer
The declaration shows that a complex number lies on the critical line if and only if the J-cost of its image under the defect-coordinate map xiMap vanishes. Number theorists working inside the Recognition Science framework cite the result when translating the Riemann hypothesis into a statement about cost minimization. The proof is a bidirectional tactic argument that rewrites via the cosh identity for J-cost and reduces the zero condition to the argument of cosh being zero.
Claim. For a complex number $ρ$, $ρ$ lies on the critical line if and only if the J-cost of the image of its real part under the defect map $x = e^{2(σ - 1/2)}$ is zero, where J-cost is the defect functional satisfying $J(e^t) = cosh(t) - 1$.
background
The module establishes a direct algebraic bridge between the completed Riemann xi function and the J-cost functional. The defect map xiMap sends real part σ to x = exp(2(σ − 1/2)), so the critical line Re(s) = 1/2 maps to the unique minimum x = 1 of J, while functional reflection s ↦ 1−s maps to x ↦ 1/x. The explicit identity J(xiMap(σ)) = cosh(2(σ − 1/2)) − 1 then converts the zero-cost condition into the statement that the deviation from the critical line is zero.
proof idea
The tactic proof opens with constructor to split the biconditional. The forward direction rewrites with jcost_xiMap_eq_cosh, then simplifies the assumption OnCriticalLine together with cosh(0) = 1. The reverse direction rewrites the zero-cost hypothesis, extracts the equation J_log(2(ρ.re − 1/2)) = 0, applies J_log_eq_zero_iff to obtain the deviation vanishes, and closes with linarith.
why it matters
This is the fifth main result listed in the XiJBridge module and supplies the explicit equivalence between the Riemann hypothesis and vanishing J-cost on defect coordinates. It realizes the translation of the xi functional equation into J-symmetry under the Recognition Composition Law and the J-uniqueness property (T5). The result sits at the end of the forcing chain that derives D = 3 and the eight-tick octave from the single functional equation, closing the link between analytic number theory and the cost-minimization picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.