pith. sign in
module module high

IndisputableMonolith.NumberTheory.ZeroDoublingLaw

show as:
view Lean formalization →

The ZeroDoublingLaw module defines the doubled zero defect as the J-cost of a zeta zero whose deviation from the critical line has been doubled. Researchers examining symmetry implications of the functional equation in the Recognition Science framework cite it when testing whether reflection alone locates zeros. The module consists of definitions and recurrences built directly from the imported cost mappings and bridge lemmas.

claimThe doubled zero defect for a zero $\rho$ is the value $J(\exp(2 \cdot \delta(\rho)))$, where $\delta(\rho) = 2(\operatorname{Re} \rho - 1/2)$ is the zero deviation and $J(x) = \frac12(x + x^{-1}) - 1$.

background

The module sits inside NumberTheory and imports three upstream modules. DiscretenessForcing shows that $J(x) = \frac12(x + x^{-1}) - 1$ has a unique minimum at $x=1$, which becomes a convex bowl $\cosh(t)-1$ in logarithmic coordinates. XiJBridge maps the completed xi functional equation $\xi(s)=\xi(1-s)$ to the J-symmetry $J(x)=J(1/x)$ under the coordinate change $x = \exp(2(\operatorname{Re}s - 1/2))$, sending the critical line to the J-minimum. ZeroLocationCost supplies the explicit dictionary zeroDeviation $\rho = 2(\operatorname{Re}\rho - 1/2)$ and zeroDefect $\rho =$ defect$(\exp($zeroDeviation $\rho))$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the doubled zero defect object imported by VectorCSymmetryOnlyNoGo. That downstream module uses the construction to certify that functional-equation reflection symmetry plus conjugation symmetry yield pairing data on zeros but do not force the critical line, serving as the explicit stage gate for Vector C.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (6)