xiMap_div_reflection
plain-language theorem explainer
Defect coordinates for reflected points in the critical strip obey the relation that their quotient equals the square of the first coordinate. Researchers bridging the Riemann xi functional equation to J-cost symmetry in Recognition Science cite this when deriving quadratic amplification of defects for paired zeros. The argument proceeds by direct substitution of the reflection property followed by field simplification after confirming non-vanishing.
Claim. Let $x:ℝ→ℝ$ denote the defect coordinate map sending real part $σ$ to the corresponding positive real defect coordinate. Then for every real $σ$, $x(σ)/x(1-σ)=[x(σ)]^2$.
background
The module sets up the ξ(s)–J(x) Bridge: the completed Riemann xi satisfies ξ(s)=ξ(1−s) while the J-cost satisfies J(x)=J(1/x). The defect-coordinate map is given by x=e^{2(σ−1/2)}, sending the critical line Re(s)=1/2 to x=1 (unique J minimum) and functional reflection s↦1−s to x↦1/x. This is the same algebraic structure, not an analogy. The defect functional is defined as defect(x):=J(x) for positive x, with defect at unity equal to zero. Upstream results include the structure of J-cost from PhiForcingDerived and the LedgerFactorization of (ℝ₊,×).
proof idea
The proof is a short term-mode argument. It rewrites the left-hand side using the reflection lemma that sends xiMap(1−σ) to the reciprocal of xiMap(σ), invokes the non-vanishing lemma to clear the denominator, and finishes with field_simp to obtain the squared term.
why it matters
This identity is listed among the module’s main results and directly enables the self-composition formula J(x²)=2J(x)²+4J(x) for paired zeros (ρ,1−ρ). It supports the later claim that RH is equivalent to all zeros having zero J-cost. In the Recognition framework it instantiates the J-uniqueness property (T5) and the Recognition Composition Law in strip coordinates, closing one step of the functional-equation symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.