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 the squared deviation factor generated by composing functional equation reflection with the recognition composition law. Researchers analyzing symmetry constraints on zeta zeros inside the Recognition Science framework cite it when testing whether reflection data alone can force the critical line. The module supplies the core definition plus direct algebraic identities for its properties.

claimLet zeroDeviation(ρ) = 2(Re ρ − 1/2). The doubled zero defect is J(exp(2 · zeroDeviation(ρ))), where J(x) = (x + x^{-1})/2 − 1.

background

The module belongs to the NumberTheory section and extends the dictionary between zero location and J-cost. DiscretenessForcing establishes that J(x) = ½(x + x^{-1}) − 1 has a unique minimum at x = 1, equivalently cosh(t) − 1 in logarithmic coordinates. XiJBridge connects the completed xi functional equation ξ(s) = ξ(1−s) to J(x) = J(1/x) via the map x = exp(2(Re(s) − 1/2)), sending the critical line to the J-minimum. ZeroLocationCost supplies zeroDeviation(ρ) = 2(Re ρ − 1/2) and zeroDefect(ρ) = defect(exp(zeroDeviation(ρ))).

proof idea

This is a definition module, no proofs. It introduces the doubledZeroDefect definition and derives its equivalence to a cosh expression, recurrence, non-negativity, and vanishing on the critical line by direct substitution into the J-functional and its algebraic identities.

why it matters in Recognition Science

The module supplies the doubled zero defect imported by VectorCSymmetryOnlyNoGo, which exhibits a toy completed-ξ surface whose zeros lie off the critical line despite reflection and conjugation symmetries. It realizes the virtual next-step observable suggested by FE reflection plus RCL self-composition. The construction engages J-uniqueness (T5) and the recognition composition law from the forcing chain.

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)