pith. sign in
module module high

IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo

show as:
view Lean formalization →

The module constructs an explicit toy completed-xi function depending only on the real part of s, with zeros exactly on the lines Re(s)=1/4 and Re(s)=3/4. Researchers developing Vector C cite it to test whether reflection and conjugation symmetries suffice for critical-line forcing. The construction proceeds by direct definition of the toy surface and verification that its zero set respects the required pairing invariants while lying off the line Re(s)=1/2.

claimLet $f$ be a function of the real part alone such that the zero set of the associated completed-ξ surface is precisely the union of the vertical lines Re$(s)=1/4$ and Re$(s)=3/4$. The surface then obeys the reflection symmetry $smapsto 1-s$ and conjugation symmetry while admitting zeros with Re$(s)neq 1/2$.

background

The module operates inside the NumberTheory domain and imports three upstream modules. CompletedXiSymmetry records the minimal functional-equation symmetry surface needed for Vector C, supplying reflection and conjugation invariants for zeroDeviation and zeroDefect but no forcing theorem. ZeroCompositionInterface isolates the abstract interface Vector C would require to convert a zero-location observable into a critical-line statement; it is classified as an alternate path. ZeroDoublingLaw encodes the concrete doubling recurrence satisfied by the defect observable: D(2t)=2D(t)^2+4D(t). The local setting is therefore a controlled toy model that isolates symmetry from additional structure.

proof idea

This is a definition module containing no proofs. It introduces the explicit objects toyXi, toyXi_reflection, toyXi_conjugation, toyCompletedXiSurface, and completedXiSurface_symmetry_only_no_go, then verifies by direct computation that the zero set lies on the stated vertical lines while the reflection and conjugation properties hold.

why it matters in Recognition Science

The module supplies a negative result that feeds the Vector C program: the symmetries recorded in CompletedXiSymmetry are insufficient by themselves to force zeros onto the critical line. It sharpens the alternate interface described in ZeroCompositionInterface by exhibiting the precise gap that must be closed by further structure such as the doubling law. The construction therefore clarifies why an additional observable beyond symmetry is required.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (12)