module module high

`IndisputableMonolith.NumberTheory.ZeroLocationCost`

ZeroLocationCost defines the critical-line predicate for complex points together with associated deviation and defect measures built from the J-cost functional. Researchers pursuing cost-minimization proofs of the Riemann Hypothesis cite these objects to convert zero locations into nonnegative observables. The module consists entirely of definitions and elementary equivalences with no theorem proofs.

claimThe critical-line predicate is given by $OnCriticalLine(s) :⇔ Re(s)=1/2$. The associated deviation and defect are $zeroDeviation(s)=|Re(s)-1/2|$ and $zeroDefect(s)=J(e^{2(Re(s)-1/2)})$ where $J(x)=½(x+x^{-1})-1$.

background

The module sits inside the NumberTheory domain and imports DiscretenessForcing, which shows that the cost landscape J(x)=½(x+x^{-1})-1 forces discreteness by possessing a unique minimum at x=1 (equivalently cosh(t)-1 in logarithmic coordinates). It also imports LawOfExistence, whose central statement equates existence of an object with vanishing defect.

proof idea

This is a definition module, no proofs. It introduces the predicates OnCriticalLine, zeroDeviation, zeroDefect together with the elementary equivalences zeroDeviation=0 iff on critical line and zeroDefect=0 iff on critical line, plus the nonnegativity of zeroDefect.

why it matters in Recognition Science

These definitions supply the zero-location observables required by CompletedXiSymmetry (for reflection and conjugation invariants), ZeroCompositionLaw (for the composition law on defects induced by the Recognition Composition Law), and ZeroDoublingLaw (for the recurrence D(2t)=2D(t)^2+4D(t)). The constructions therefore form the interface layer for Vector-C style forcing arguments toward the Riemann Hypothesis.

scope and limits

Does not derive or assume the functional equation of the zeta function.
Does not prove that all zeros lie on the critical line.
Does not compute or approximate any explicit zero locations.
Does not import the explicit formula or connect to prime-counting.

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