zeroDefect_invariant_under_reflection
plain-language theorem explainer
The zero-location defect of a complex number ρ equals the defect of its reflection across Re(s) = 1/2 composed with conjugation. Researchers examining zeta-zero symmetries or the completed xi functional equation would cite the result to obtain pairing invariants. The proof is a four-line calculation that rewrites the defect through J_log, negates the deviation under reflection, applies evenness of J_log, and returns to the defect definition.
Claim. For any complex number $ρ$, the zero-location defect of $1 - conj(ρ)$ equals the zero-location defect of $ρ$, where zero-location defect is $J_{log}(2(Re ρ - 1/2))$ and $J_{log}(t) = cosh(t) - 1$.
background
The module formalizes the Recognition Science dictionary that maps zeta-zero location to a defect cost. zeroDeviation ρ is defined as twice the real part of ρ minus one, measuring signed distance from the critical line. zeroDefect ρ is then the J-cost of the exponential of that deviation, which reduces exactly to J_log(zeroDeviation ρ) with J_log(t) := cosh(t) − 1, a convex bowl minimized at zero. criticalReflection ρ is the map 1 − conjugate(ρ), which sends any point to its mirror image across Re(s) = 1/2 while negating the deviation.
proof idea
The proof is a calc chain of four equalities. It first replaces zeroDefect with its J_log form via zeroDefect_eq_J_log. The deviation after reflection is rewritten as the negation of the original deviation by zeroDeviation_criticalReflection. J_log_symmetric then equates the J_log value on the negated argument to the value on the original argument. The chain closes by applying zeroDefect_eq_J_log in reverse.
why it matters
The invariance supplies the zero-location cost preservation needed by functionalEquation_gives_pairing_invariants, which concludes that vanishing of the completed xi at ρ implies vanishing at the reflected point with identical defect. It therefore confirms that the critical line is precisely the zero-defect locus in the Recognition Science dictionary, consistent with the J-uniqueness and self-similar fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.