rcl_defect_coordinates

formal source

 117/-- **The RCL holds on defect coordinates.**
 118    For any two points σ₁, σ₂ in the strip, the composition law
 119    constrains their joint defect. -/
 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
 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. -/
 133theorem xiMap_mul_reflection (σ : ℝ) : xiMap σ * xiMap (1 - σ) = 1 := by
 134  rw [xiMap_reflection]
 135  exact mul_inv_cancel₀ (xiMap_ne_zero σ)
 136
 137/-- The quotient of defect coordinates for reflected points squares. -/
 138theorem xiMap_div_reflection (σ : ℝ) : xiMap σ / xiMap (1 - σ) = (xiMap σ) ^ 2 := by
 139  rw [xiMap_reflection]
 140  have hx : xiMap σ ≠ 0 := xiMap_ne_zero σ
 141  field_simp
 142
 143/-! ## §5. Self-composition for paired zeros -/
 144
 145/-- **Self-composition formula for functional-equation pairs.**
 146
 147    For a paired zero (ρ, 1−ρ) with defect coordinate x = xiMap(σ):
 148
 149      J(x²) = 2·J(x)² + 4·J(x)
 150