toyXi
plain-language theorem explainer
A toy completed-ξ function is defined that depends only on the real part of its complex argument and vanishes exactly on the vertical lines Re(s) = 1/4 and Re(s) = 3/4. Researchers testing whether reflection and conjugation symmetries alone suffice to force critical-line zeros would cite this explicit counterexample. The definition is a direct term that embeds a product of squared real-part deviations into the complex numbers.
Claim. Define the toy function by $xi(s) := ((Re(s) - 3/4)^2 * (Re(s) - 1/4)^2)$ for $s in mathbb{C}$, taking values in the reals. Its zero set is the union of the lines $Re(s) = 1/4$ and $Re(s) = 3/4$.
background
The module formalizes the Vector C stage gate: functional-equation reflection symmetry plus conjugation symmetry produce pairing data on zeros but do not force the critical line. This is certified by an explicit toy completed-ξ surface whose zeros occur on the off-line pair Re(s) = 1/4, 3/4. The toyXi function supplies the xi component of that surface and is required to be invariant under functionalReflection and under complex conjugation while remaining real-valued and non-negative.
proof idea
The definition is given directly as Complex.ofReal of the product of squared deviations from the lines Re(s) = 1/4 and Re(s) = 3/4. No lemmas or tactics are applied; it is a pure term definition.
why it matters
This definition supplies the concrete counterexample for the symmetry-only no-go result. It is instantiated as the xi field of toyCompletedXiSurface, which supports toyCompletedXiSurface_has_off_critical_zero and the theorem zeroDeviationSet_neg_closed_not_enough showing that a negation-closed deviation set need not contain only the zero deviation. It fills the main stage gate for Vector C described in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.