IndisputableMonolith.NumberTheory.CompletedXiSymmetry
Module CompletedXiSymmetry supplies the base symmetry data for the completed ξ function in Vector C analysis. It encodes reflection from the completed functional equation and conjugation from reality symmetry. Stronger zero-location constraints must be added separately. Researchers examining symmetry-only implications in Recognition Science cite it as the starting surface before no-go arguments. It is a definition module with no proofs.
claimThe completed-$\\$xi surface carries reflection invariance under the functional equation and conjugation invariance under complex conjugation, yielding zero-pairing data without forcing the critical line.
background
This module sits in the NumberTheory domain and imports the zero-location cost dictionary. Upstream, zeroDeviation $\rho$ equals $2(\operatorname{Re} \rho - 1/2)$ and zeroDefect $\rho$ equals defect$(\exp(\text{zeroDeviation }\rho))$. The supplied doc-comment states that reflection is the completed functional equation and conjugation is the standard reality symmetry; any stronger zero-location constraint must be added on top.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds VectorCSymmetryOnlyNoGo, which shows that reflection plus conjugation produce pairing invariants on zeros but do not force the critical line. It supplies the explicit toy completed-$\$xi surface used to certify the symmetry-only no-go for Vector C.
scope and limits
- Does not assert that zeros lie on the critical line.
- Does not add zero-location constraints beyond reflection and conjugation.
- Does not formalize the completed $\xi$ function itself.
used by (1)
depends on (1)
declarations in this module (12)
-
structure
CompletedXiSurface -
def
XiZeroSet -
def
zeroDeviationSet -
def
zeroDefectSet -
theorem
xi_reflection_invariant -
theorem
xi_conjugation_invariant -
theorem
zero_pairing_under_reflection -
theorem
zero_pairing_under_conjugation -
theorem
zero_pairing_under_critical_reflection -
theorem
functionalEquation_gives_pairing_invariants -
theorem
zeroDeviationSet_neg_closed -
theorem
zeroDefectSet_reflection_invariant