rcl_defect_coordinates
plain-language theorem explainer
Researchers bridging the Riemann xi functional equation to Recognition Science cost functionals cite this result to confirm that the composition law holds verbatim on defect coordinates. The verification applies to any pair of real strip coordinates. Algebraic simplification after non-zero checks establishes the identity.
Claim. Let $x_1$ and $x_2$ be the defect coordinates of real parameters $σ_1$ and $σ_2$. Then $J(x_1 x_2) + J(x_1 / x_2) = 2 J(x_1) J(x_2) + 2 J(x_1) + 2 J(x_2)$, where $J$ is the J-cost functional.
background
The module sets up an exact algebraic bridge: the completed Riemann xi satisfies ξ(s) = ξ(1-s), which translates under the defect-coordinate map x = exp(2(σ - 1/2)) into the reciprocal symmetry J(x) = J(1/x). The defect functional is defined as defect(x) := J(x) for positive x. Upstream results supply the J-cost structure (PhiForcingDerived.of) and the defect identification (LawOfExistence.defect).
proof idea
Non-vanishing of xiMap σ₁ and xiMap σ₂ (hence of product and quotient) is obtained from the sibling lemma xiMap_ne_zero. The definition of Jcost is unfolded by simp, field_simp clears the division, and ring verifies the resulting polynomial identity.
why it matters
This confirms the Recognition Composition Law holds on defect coordinates, the third main result listed in the module documentation. It directly supports the later equivalence rh_equivalent_to_zero_cost between the Riemann hypothesis and zero J-cost at all zeros. In the framework it shows the RCL is compatible with the xi functional equation without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.