toyXi_reflection
plain-language theorem explainer
The theorem establishes invariance of the toy completed-ξ function under reflection across Re(s) = 1/2. Researchers studying symmetry constraints on zero locations in zeta-like functions cite it to isolate reflection from the critical-line property. The proof is a direct algebraic reduction that substitutes the explicit definitions of toyXi and functionalReflection then normalizes the resulting identity.
Claim. Let $f(s) = ((s.re - 3/4)^2) ((s.re - 1/4)^2)$ viewed as a complex-valued function of $s$. Then $f(1-s) = f(s)$ for all $s$ in the complex plane.
background
The Vector C Symmetry-Only No-Go module constructs an explicit completed-ξ surface obeying functional-equation reflection and conjugation yet admitting zeros off the critical line. The toyXi definition supplies a function that depends only on the real part: its zero set is the union of the vertical lines Re(s) = 1/4 and Re(s) = 3/4, satisfying both symmetries while remaining off-critical. The functionalReflection map is the standard reflection ρ ↦ 1-ρ across Re(s) = 1/2.
proof idea
The proof is a one-line wrapper. It applies simp to unfold the definitions of toyXi and functionalReflection, then invokes the ring tactic to normalize the resulting polynomial identity in the real and imaginary parts.
why it matters
This supplies the reflection field required by the toyCompletedXiSurface definition, which exhibits a concrete surface whose zeros lie on the off-critical pair Re(s) = 1/4, 3/4. The result therefore demonstrates that functional-equation-style pairing data alone does not force critical-line support, directly advancing the module's no-go statement for Vector C. It leaves open what additional structure beyond reflection and conjugation is needed to pin zeros to Re(s) = 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.