rcl_defect_coordinates
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the Riemann hypothesis or locate any zeros.
- Does not extend the defect map to complex arguments.
- Does not compute numerical values or bounds on J-cost.
- Does not address physical constants or forcing-chain steps T0-T8.
formal statement (Lean)
120theorem rcl_defect_coordinates (σ₁ σ₂ : ℝ) :
121 Jcost (xiMap σ₁ * xiMap σ₂) + Jcost (xiMap σ₁ / xiMap σ₂) =
122 2 * Jcost (xiMap σ₁) * Jcost (xiMap σ₂) +
123 2 * Jcost (xiMap σ₁) + 2 * Jcost (xiMap σ₂) := by
proof body
Term-mode proof.
124 have h₁ : xiMap σ₁ ≠ 0 := xiMap_ne_zero σ₁
125 have h₂ : xiMap σ₂ ≠ 0 := xiMap_ne_zero σ₂
126 have h₃ : xiMap σ₁ * xiMap σ₂ ≠ 0 := mul_ne_zero h₁ h₂
127 have h₄ : xiMap σ₁ / xiMap σ₂ ≠ 0 := div_ne_zero h₁ h₂
128 simp only [Jcost]
129 field_simp
130 ring
131
132/-- The product of defect coordinates for reflected points is 1. -/