zeroDefect_invariant_under_conjugation
plain-language theorem explainer
Conjugation of a complex number ρ leaves its zero-location defect unchanged. Researchers deriving symmetry invariants for zeta zeros in the Recognition Science framework would cite this when closing the conjugation leg of pairing statements. The proof is a three-step calc that rewrites via zeroDefect_eq_J_log, applies the conjugation rule for zeroDeviation, and closes by symmetry.
Claim. Let $ρ ∈ ℂ$. Then the zero-location defect of the complex conjugate of $ρ$ equals the zero-location defect of $ρ$, where the zero-location defect is defined as $J_{log}(2( Re ρ - 1/2 ))$ and $J_{log}(t) = cosh t - 1$.
background
The Zero Location Cost module formalizes the RS dictionary between zeta-zero location and zero-defect cost: zeroDeviation ρ = 2 (Re ρ - 1/2) and zeroDefect ρ = defect(exp(zeroDeviation ρ)). The critical line Re ρ = 1/2 is therefore exactly the zero-defect locus. J_log(t) = cosh(t) - 1 is the defect expressed in logarithmic coordinates, as defined in DiscretenessForcing and equivalently in ContinuumBridge; defect(x) = J(x) for positive x appears in LawOfExistence.
proof idea
The proof is a calc chain. It begins with zeroDefect(conj ρ) = J_log(zeroDeviation(conj ρ)) by zeroDefect_eq_J_log. It rewrites the argument via zeroDeviation_conj. It concludes by the symmetric form of zeroDefect_eq_J_log.
why it matters
This supplies the conjugation invariance required by functionalEquation_gives_pairing_invariants in CompletedXiSymmetry, which states that reflection and conjugation give the exact zero-location invariants available from the completed-ξ surface. It closes one symmetry component in the Recognition Science treatment of the xi functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.