zeroDefect_invariant_under_conjugation
Conjugation leaves the zero-location defect unchanged for any complex ρ. Researchers establishing symmetry properties of zeta zeros under the Recognition Science dictionary cite this invariance when deriving pairing results on the completed xi surface. The proof is a three-step calc that substitutes the conjugation invariance of zeroDeviation into the J_log expression for zeroDefect.
claimFor any complex number ρ, zeroDefect(conj ρ) = zeroDefect(ρ), where zeroDefect(ρ) := J_log(2(Re ρ − 1/2)) and J_log(t) := cosh(t) − 1.
background
The module formalizes the RS dictionary between zeta-zero location and zero-defect cost. It sets zeroDeviation ρ := 2(Re ρ − 1/2) and zeroDefect ρ := defect(exp(zeroDeviation ρ)), so that the critical line Re ρ = 1/2 is exactly the zero-defect locus. The defect equals J_log of the deviation, where J_log(t) := cosh(t) − 1 is the log-coordinate form of the J-cost (a convex bowl minimized at t = 0).
proof idea
The proof is a calc block. It rewrites zeroDefect(conj ρ) as J_log(zeroDeviation(conj ρ)) by zeroDefect_eq_J_log, replaces the argument by zeroDeviation ρ via rw [zeroDeviation_conj], and recovers zeroDefect ρ by the symmetric form of zeroDefect_eq_J_log.
why it matters in Recognition Science
The result supplies the conjugation half of the pairing invariants in functionalEquation_gives_pairing_invariants. It reinforces that the critical line is the zero-defect locus, consistent with the J-uniqueness and self-similar fixed point of the forcing chain. The invariance is required for any argument that treats reflection and conjugation symmetrically on the completed xi surface.
scope and limits
- Does not locate any zeros.
- Does not derive the functional equation.
- Applies only to the defined zeroDeviation and zeroDefect.
- Does not address other transformations.
formal statement (Lean)
143theorem zeroDefect_invariant_under_conjugation (ρ : ℂ) :
144 zeroDefect (conj ρ) = zeroDefect ρ := by
proof body
Tactic-mode proof.
145 calc
146 zeroDefect (conj ρ)
147 =
148 Foundation.DiscretenessForcing.J_log
149 (zeroDeviation (conj ρ)) := zeroDefect_eq_J_log _
150 _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
151 rw [zeroDeviation_conj]
152 _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
153
154/-- Reflection plus conjugation preserves the zero-location defect. -/