module module moderate

`IndisputableMonolith.NumberTheory.ZeroLocationCost`

The module defines the critical-line predicate for complex points together with the associated zeroDefect cost derived from the J-functional. Researchers formalizing zeta-zero location via Recognition Science cost landscapes would cite these objects when building symmetry or composition arguments. The module supplies direct definitions and basic equivalences such as zeroDefect vanishing precisely on the critical line.

claimThe predicate $\text{OnCriticalLine}(s)$ holds for complex $s$ precisely when $\Re(s)=1/2$. The defect is $\text{zeroDefect}(s)=J(e^{2(\Re(s)-1/2)})$ with $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$.

background

The module imports DiscretenessForcing, whose doc states that J(x) = ½(x + x⁻¹) - 1 has a unique minimum at x = 1 and that in log coordinates J(eᵗ) = cosh(t) - 1 forms a convex bowl centered at t = 0. It also imports LawOfExistence, which encodes the sharp equivalence x exists ⟺ defect(x) = 0.

ZeroLocationCost applies these notions to complex points by introducing the predicate OnCriticalLine and the observable zeroDefect (with siblings zeroDeviation, functionalReflection, and the listed equivalences zeroDefect_eq_J_log, zeroDefect_eq_cosh_sub_one). The local setting is therefore the translation of the J-cost landscape into a coordinate measuring deviation of a complex number from the line Re(s) = 1/2.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply the zero-location cost interface used by CompletedXiSymmetry (which obtains reflection and conjugation invariants for zeroDeviation / zeroDefect), by ZeroCompositionLaw (which induces the composition law on zeta zero defects), and by ZeroDoublingLaw (which records the doubling recurrence D(2t) = 2 D(t)² + 4 D(t)). The module therefore encodes the cost landscape that connects J-uniqueness to the functional-equation symmetry surface required for Vector C.

scope and limits

Does not prove the Riemann hypothesis.
Does not compute explicit zero locations or ordinates.
Does not derive the functional equation of the zeta function.
Does not address pair correlations or higher moments of zeros.
Does not import or invoke the explicit formula.

used by (6)

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

IndisputableMonolith.NumberTheory.CompletedXiSymmetry module_import
IndisputableMonolith.NumberTheory.CompositionDivergence module_import
IndisputableMonolith.NumberTheory.XiJBridge module_import
IndisputableMonolith.NumberTheory.ZeroCompositionInterface module_import
IndisputableMonolith.NumberTheory.ZeroCompositionLaw module_import
IndisputableMonolith.NumberTheory.ZeroDoublingLaw module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Foundation.LawOfExistence module_import

declarations in this module (19)

def OnCriticalLine L25
def functionalReflection L29
def criticalReflection L33
def zeroDeviation L38
def zeroDefect L42
theorem zeroDefect_eq_J_log L46
theorem zeroDefect_eq_cosh_sub_one L53
theorem zeroDeviation_eq_zero_iff_on_critical_line L58
theorem zeroDefect_zero_iff_on_critical_line L68
theorem zeroDefect_pos_iff_off_critical_line L83
theorem zeroDefect_nonneg L100
theorem functionalReflection_re L104
theorem criticalReflection_re L108
theorem zeroDeviation_functionalReflection L112
theorem zeroDeviation_conj L118
theorem zeroDeviation_criticalReflection L122
theorem zeroDefect_invariant_under_functional_reflection L129
theorem zeroDefect_invariant_under_conjugation L143
theorem zeroDefect_invariant_under_reflection L155