toyCompletedXiSurface_has_off_critical_zero
plain-language theorem explainer
The toy completed ξ surface vanishes at s = 3/4, which lies off the critical line. Researchers examining symmetry-only constraints on zero locations cite this explicit counterexample. The proof is a direct term-mode computation that normalizes the surface definition and the critical-line predicate.
Claim. Let Ξ be the toy completed ξ-surface. Then Ξ(3/4) = 0 and 3/4 does not lie on the critical line.
background
The module Vector C Symmetry-Only No-Go shows that functional-equation reflection symmetry plus conjugation symmetry produce zero-pairing data but do not force the critical line. The toyCompletedXiSurface is defined so its zeros occur at real parts 1/4 and 3/4. OnCriticalLine is the predicate that a complex number lies on the line Re(s) = 1/2.
proof idea
Constructor splits the conjunction. The first norm_num reduces the zero equality using the definitions of toyCompletedXiSurface and toyXi. The second norm_num reduces the negation using the definition of OnCriticalLine.
why it matters
This supplies the off-critical zero used by completedXiSurface_symmetry_only_no_go to prove that symmetry alone cannot force every zero onto the critical line. It realizes the module statement that reflection and conjugation symmetries are insufficient. The result separates the symmetry stage from any later structure that would recover the critical line in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.