jcost_xiMap_at_half
plain-language theorem explainer
J-cost vanishes at the defect coordinate corresponding to the critical line. Researchers linking the Riemann hypothesis to Recognition Science cost minima would cite this when identifying Re(s)=1/2 with the J-minimum. The proof is a one-line rewrite that substitutes the known value of xiMap at one-half and invokes the unit lemma for J-cost.
Claim. Let $J(x) = (x-1)^2/(2x)$ denote the J-cost and let $x = e^{2(Re(s)-1/2)}$ be the defect-coordinate map. Then $J(x(1/2)) = 0$.
background
J-cost is the quadratic ratio $J(x) = (x-1)^2/(2x)$ on positive reals, with unique minimum zero at $x=1$. The xiMap is the defect map $x = e^{2(Re(s)-1/2)}$ that sends the critical line Re(s)=1/2 to $x=1$. Module context identifies the completed xi functional equation with J-cost reciprocal symmetry under this coordinate change. Upstream lemma Jcost_unit0 states that Jcost 1 = 0 by direct simplification of the definition.
proof idea
One-line wrapper that rewrites via xiMap_at_half (which evaluates to unity) followed by Jcost_unit0.
why it matters
The result instantiates the module claim that zero J-cost is equivalent to the critical line, supporting the downstream equivalence RH ↔ all zeros have J-cost zero. It directly realizes the Recognition Science landmark that the critical line maps to the J-minimum at unity under the defect coordinate change. The declaration closes one link in the chain from T5 J-uniqueness through the RCL to the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.