xiMap_mul_reflection

formal source

 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
 151    This is the "amplification equation": the composition defect of a
 152    functional-equation pair grows quadratically in the individual defect.
 153
 154    Proof: substitute x₁=x, x₂=1/x into the RCL. Then x₁·x₂=1 (J=0)
 155    and x₁/x₂=x², giving J(x²) = 2J(x)²+4J(x) since J(x)=J(1/x). -/
 156theorem paired_zero_composition (σ : ℝ) :
 157    Jcost ((xiMap σ) ^ 2) =
 158    2 * (Jcost (xiMap σ)) ^ 2 + 4 * Jcost (xiMap σ) := by
 159  have hx : xiMap σ ≠ 0 := xiMap_ne_zero σ
 160  have hx2 : (xiMap σ) ^ 2 ≠ 0 := pow_ne_zero 2 hx
 161  simp only [Jcost]
 162  field_simp
 163  ring