zeroDeviation_functionalReflection
Functional reflection across Re(s)=1/2 negates the zero deviation of any complex number ρ. Number theorists working on zeta zero locations within the Recognition Science dictionary cite this symmetry when establishing pairing invariants for the completed ξ surface. The proof is a direct term reduction that unfolds the two definitions, applies simp, and closes with linear arithmetic.
claimFor any complex number ρ, the deviation δ(ρ) := 2(Re(ρ) − 1/2) satisfies δ(1 − ρ) = −δ(ρ), where the map ρ ↦ 1 − ρ is reflection across the line Re(s) = 1/2.
background
The module encodes the Recognition Science dictionary linking zeta-zero location to defect cost. Zero deviation of ρ is defined as twice the offset of its real part from 1/2; zero defect is then the defect of the exponential of that deviation. The critical line Re ρ = 1/2 is therefore exactly the zero-defect locus.
proof idea
Unfold zeroDeviation and functionalReflection to obtain an expression linear in the real part of ρ. Apply simp to reduce the arithmetic, then close with linarith.
why it matters in Recognition Science
The result supplies the sign-flip property used in functionalEquation_gives_pairing_invariants to list the zero-location invariants available from the completed ξ surface. It also enters the proof that zero defect is invariant under functional reflection. In the framework this confirms the critical line as the zero-defect locus, consistent with the forcing chain landmarks T5–T8.
scope and limits
- Does not locate any specific zeta zeros.
- Does not prove the Riemann hypothesis.
- Does not extend to other L-functions.
- Applies only to the zero deviation measure defined in this module.
formal statement (Lean)
112@[simp] theorem zeroDeviation_functionalReflection (ρ : ℂ) :
113 zeroDeviation (functionalReflection ρ) = -zeroDeviation ρ := by
proof body
Term-mode proof.
114 unfold zeroDeviation functionalReflection
115 simp
116 linarith
117