paired_zero_composition
plain-language theorem explainer
The theorem delivers the algebraic identity J(x²) = 2[J(x)]² + 4J(x) for the defect coordinate x obtained from any real σ via the xi map. Researchers linking the Riemann functional equation to Recognition Science cost symmetry would cite it when quantifying quadratic defect growth for paired zeros. The term proof reduces the claim by first confirming non-vanishing of the map and then applying field simplification followed by ring arithmetic on the unfolded J-cost definition.
Claim. For any real number σ, let x = ξ_map(σ). Then J(x²) = 2[J(x)]² + 4J(x), where J denotes the J-cost functional and ξ_map is the defect-coordinate map sending the real part of s in the critical strip to the positive real x satisfying the reciprocal symmetry J(x) = J(1/x).
background
The module bridges the completed Riemann xi function ξ(s) = ξ(1-s) with the J-cost functional that obeys J(x) = J(1/x). Under the coordinate change x = e^{2(Re(s) − 1/2)}, the critical line maps to x = 1 (the unique J minimum) and functional reflection maps to x ↦ 1/x. The Recognition Composition Law supplies the underlying addition formula J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
The term proof first invokes the sibling lemma xiMap_ne_zero to obtain xiMap σ ≠ 0, then unfolds Jcost via simp only [Jcost], clears denominators with field_simp, and closes the resulting polynomial identity with ring.
why it matters
The declaration is listed as the fourth main result in the module doc-comment, supplying the amplification equation that follows from substituting a reciprocal pair into the Recognition Composition Law. It supports the downstream claim that the Riemann hypothesis is equivalent to zero J-cost on all zeros and quantifies how defect grows quadratically away from the critical line. The result sits inside the T5–T6 forcing chain that derives J-uniqueness and the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.