zeroDeviation_conj
plain-language theorem explainer
The declaration shows that zero deviation from the critical line is unchanged under complex conjugation. Researchers studying zero locations and their costs in the Recognition Science model cite it to confirm conjugate-pair symmetry. The proof is a one-line wrapper that applies simp to the explicit real-part definition of zeroDeviation.
Claim. For any complex number $ρ$, the zero deviation satisfies $2( Re(¯ρ) - 1/2 ) = 2( Re ρ - 1/2 )$.
background
The module formalizes the RS dictionary between zeta-zero location and zero-defect cost. zeroDeviation ρ is defined as twice the real-part deviation of ρ from the critical line Re ρ = 1/2, expressed in a log-coordinate scale compatible with the defect functional. This deviation enters the cost via zeroDefect ρ = defect(exp(zeroDeviation ρ)), so the critical line is exactly the zero-defect locus.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of zeroDeviation. Because that definition depends only on the real part, conjugation leaves the value unchanged.
why it matters
This supplies the conjugation invariance required by functionalEquation_gives_pairing_invariants, which extracts zero-location invariants from the completed-ξ surface, and by zeroDefect_invariant_under_conjugation. It confirms that deviation costs are preserved under the symmetries of the functional equation, consistent with the critical line being the zero-defect locus in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.