pith. machine review for the scientific record. sign in
theorem proved term proof

xiMap_div_reflection

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 138theorem xiMap_div_reflection (σ : ℝ) : xiMap σ / xiMap (1 - σ) = (xiMap σ) ^ 2 := by

proof body

Term-mode proof.

 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). -/

depends on (15)

Lean names referenced from this declaration's body.