xiMap_mul_reflection
plain-language theorem explainer
Defect coordinates under the map xiMap obey the reciprocal relation xiMap(σ) xiMap(1-σ) = 1. Researchers bridging the Riemann xi functional equation to J-cost symmetry in Recognition Science cite this to confirm the multiplicative reflection. The proof rewrites the second term via xiMap_reflection and cancels using non-vanishing.
Claim. For every real number $σ$, if $ξ_{map}$ denotes the defect coordinate map, then $ξ_{map}(σ) · ξ_{map}(1-σ) = 1$.
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 change of variables x = exp(2(σ - 1/2)), reflection s ↦ 1-s maps to x ↦ 1/x, turning the functional equation into a statement about reciprocal coordinates. The defect functional itself is defined by defect(x) := J(x) (LawOfExistence.defect). Upstream results supply the reflection lemma xiMap_reflection (which encodes the reciprocal action) and the non-vanishing lemma xiMap_ne_zero.
proof idea
The proof is a one-line wrapper. It rewrites the second factor with xiMap_reflection to obtain the reciprocal of the first factor, then applies mul_inv_cancel₀ to the nonzero value supplied by xiMap_ne_zero σ.
why it matters
This theorem supplies the multiplicative form of reflection symmetry inside the ξ–J bridge, directly supporting the module's listed main results such as rcl_defect_coordinates and rh_equivalent_to_zero_cost. It translates the classical xi functional equation into defect coordinates and J-cost reciprocal symmetry, which rests on the Recognition Science forcing chain (T5 J-uniqueness and the reciprocal property J(x) = J(1/x)). No open questions are closed here, but the result is required for any later equivalence between the Riemann hypothesis and zero J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.