zeroDefect_invariant_under_functional_reflection
plain-language theorem explainer
The zero-location defect attached to a complex number ρ is unchanged when ρ is sent to its reflection 1 − ρ across the critical line. Researchers formalizing zeta-zero symmetries via the completed xi surface cite this result to establish that defect sets are closed under the functional equation. The proof is a four-step calc that rewrites the defect through J_log, flips the sign of the deviation, invokes evenness of J_log, and returns to the original defect.
Claim. Let ρ ∈ ℂ. Then d(ρ) = d(1 − ρ), where d(ρ) := J(exp(2(Re ρ − 1/2))) and J(x) = cosh(log x) − 1 for x > 0.
background
The module translates zeta-zero location into a Recognition Science cost. zeroDeviation ρ measures twice the real-part offset from the critical line: zeroDeviation ρ = 2(Re ρ − 1/2). zeroDefect ρ is then defined as defect(exp(zeroDeviation ρ)), which equals J_log(zeroDeviation ρ) with J_log(t) = cosh(t) − 1. This cost is zero precisely when Re ρ = 1/2.
proof idea
The proof is a calc chain. It rewrites zeroDefect(functionalReflection ρ) as J_log(zeroDeviation(functionalReflection ρ)) by zeroDefect_eq_J_log. The deviation of the reflection equals the negative of the original deviation. J_log of the negative equals J_log of the positive by J_log_symmetric. The chain closes by the symmetric application of zeroDefect_eq_J_log.
why it matters
The result is used to prove that the completed xi functional equation preserves the realized zero-defect set and to list the pairing invariants available from reflection and conjugation. It supplies the invariance step that links the J-uniqueness property (T5) to the symmetry statements for the xi surface, confirming that the defect structure is compatible with the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.