toyCompletedXiSurface
plain-language theorem explainer
Defines a concrete completed-ξ surface obeying reflection and conjugation symmetries whose zeros lie exactly on the lines Re(s) = 1/4 and Re(s) = 3/4. Vector C researchers cite the construction to exhibit a symmetry-only counterexample showing that functional-equation pairing data does not force critical-line support. The definition assembles the surface by direct substitution of the toyXi function and its two pre-verified symmetry theorems into the CompletedXiSurface structure.
Claim. Let $Ξ$ be the completed-ξ surface with $Ξ(s) = ((Re(s) - 3/4)^2 (Re(s) - 1/4)^2)$ (embedded in $ℂ$), satisfying $Ξ(1-s) = Ξ(s)$ and $Ξ(¯s) = ¯(Ξ(s))$ for all $s ∈ ℂ$.
background
The CompletedXiSurface structure packages a function xi : ℂ → ℂ with two symmetry axioms: reflection xi(1-s) = xi(s) and conjugation xi(conj s) = conj(xi s). The toyXi function is the real-valued map s ↦ ((Re s - 3/4)^2 · (Re s - 1/4)^2), whose zero set is the union of the vertical lines Re s = 1/4 and Re s = 3/4. The module shows that these symmetries alone produce zero-pairing data without constraining zeros to the critical line Re s = 1/2.
proof idea
One-line wrapper that supplies the toyXi function as the xi component and inserts the pre-proved toyXi_reflection and toyXi_conjugation theorems into the reflection and conjugation fields of the CompletedXiSurface structure.
why it matters
This definition supplies the explicit counterexample used by completedXiSurface_symmetry_only_no_go, which proves that reflection and conjugation symmetries of the completed-ξ surface are insufficient to force all zeros onto the critical line. It also feeds pureVectorCDoublingData_offline_example and zeroDeviationSet_neg_closed_not_enough. In the Recognition framework it illustrates the Vector C stage gate: functional-equation symmetries alone do not imply the critical-line support required for the full theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.