zeroDeviation_functionalReflection
plain-language theorem explainer
Reflection of a complex number ρ across Re(s) = 1/2 negates its zero deviation. Number theorists tracking zeta-zero symmetries under the functional equation cite this when deriving pairing invariants. The proof is a term-mode reduction that unfolds the two definitions, applies simp, and closes with linarith.
Claim. Let ρ ∈ ℂ. Then 2(Re(1 − ρ) − 1/2) = −2(Re ρ − 1/2), where the left-hand side is the zero deviation of the functional reflection of ρ.
background
The module formalizes the RS dictionary between zeta-zero location and zero-defect cost. Zero deviation of ρ is defined as 2(Re ρ − 1/2). Functional reflection of ρ is defined as 1 − ρ, the map that reflects across the line Re(s) = 1/2. The critical line Re ρ = 1/2 is therefore exactly the zero-defect locus. Upstream, functionalReflection supplies the reflection map and zeroDeviation supplies the deviation measure expressed in the log-coordinate scale compatible with the RS defect functional.
proof idea
Term-mode proof. Unfold zeroDeviation and functionalReflection, apply simp to reduce the arithmetic, then invoke linarith to obtain the negation.
why it matters
Feeds directly into functionalEquation_gives_pairing_invariants, which records the zero-location invariants available from the completed-ξ surface, and into zeroDefect_invariant_under_functional_reflection, which shows the defect itself is unchanged under reflection. The result supplies the sign-reversal property required for the RS treatment of the functional equation and the eight-tick octave symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.