toyXi_conjugation
plain-language theorem explainer
The conjugation symmetry of the toy completed-ξ function holds because the function is constructed to depend only on the real part of its argument. Researchers constructing explicit symmetry-only no-go examples for the Riemann hypothesis would cite this result when showing that reflection and conjugation together permit off-critical-line zeros. The short tactic proof unfolds the definition of toyXi and reduces the claim to the elementary fact that conjugation leaves the real part unchanged.
Claim. Let $xi(s) := ((Re(s) - 3/4)^2 (Re(s) - 1/4)^2)$ for $s in mathbb{C}$. Then $xi(overline{s}) = overline{xi(s)}$ for every complex $s$.
background
The Vector C Symmetry-Only No-Go module exhibits a completed-ξ surface that obeys functional-equation reflection and conjugation symmetries yet places zeros on the vertical lines Re(s) = 1/4 and Re(s) = 3/4. The toyXi function is defined explicitly as a real-valued quartic in the real part alone, so its zero set automatically satisfies both symmetries while remaining off the critical line. Module documentation states that this construction supplies pairing data on zeros without forcing critical-line support.
proof idea
The tactic proof unfolds the definition of toyXi, rewrites the outer conjugate using Complex.conj_ofReal, introduces the auxiliary equality (conj s).re = s.re by simp, and substitutes to obtain the required identity. No upstream lemmas beyond the definition of toyXi and basic complex arithmetic are invoked.
why it matters
This theorem supplies the conjugation field required by the toyCompletedXiSurface definition, which serves as the concrete counterexample demonstrating that FE-style reflection plus conjugation symmetries are insufficient to force critical-line zeros. It occupies the main stage gate in the Vector C analysis and leaves open the question of which additional structure (phi-ladder Poisson summation or zero-doubling laws) would be needed to reach the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.