pith. sign in
module module high

IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo

show as:
view Lean formalization →

This module constructs a toy completed-ξ function depending only on the real part of s, with zeros exactly on the lines Re(s)=1/4 and Re(s)=3/4. It satisfies reflection and conjugation symmetries from the functional equation yet places zeros off the critical line. Vector C researchers cite the example to show why symmetry data alone cannot force the Riemann hypothesis. The construction proceeds by explicit real-part dependence and direct zero-set verification.

claimLet $\tilde{\xi}(s)$ be a completed-$\xi$-style function with $\tilde{\xi}(s) = f(\Re(s))$. Its zero set equals $\{\Re(s)=1/4\} \cup \{\Re(s)=3/4\}$, satisfying reflection and conjugation symmetries while admitting off-critical zeros.

background

The module sits inside the NumberTheory exploration of Vector C. It imports CompletedXiSymmetry, which records the minimal functional-equation symmetry surface needed for Vector C and yields reflection and conjugation invariants for zeroDeviation and zeroDefect but not yet any forcing to the critical line. It also draws on ZeroDoublingLaw, whose defect observable obeys the doubling recurrence D(2t) = 2 D(t)^2 + 4 D(t), and on ZeroCompositionInterface, which isolates the abstract theorem interface required to convert a zero-location observable into a critical-line forcing result.

proof idea

This is a definition module, no proofs. The argument consists of an explicit construction of the toy function together with direct verification that its zero set lies on the stated vertical lines and that the reflection and conjugation maps preserve the function.

why it matters in Recognition Science

The module supplies a concrete counterexample showing that the symmetry surface from CompletedXiSymmetry is insufficient by itself. It therefore feeds the interface recorded in ZeroCompositionInterface and underscores the necessity of the doubling law from ZeroDoublingLaw to obtain critical-line forcing. It touches the open question of what additional structure beyond functional-equation symmetries is required in the Recognition Science approach to the Riemann hypothesis.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (12)