module module moderate

`IndisputableMonolith.NumberTheory.ZeroLocationCost`

This module defines the critical-line predicate for a complex point via the J-cost applied to the defect coordinate map. Researchers linking Recognition Science to zeta zero locations cite it as the base interface for symmetry and composition arguments. The module consists of definitions and elementary equivalences with no deep proofs.

claimThe critical-line predicate for $s \in \mathbb{C}$ is given by $\text{OnCriticalLine}(s) \iff \text{zeroDefect}(s) = 0$, where $\text{zeroDefect}(s) = J(e^{2(\operatorname{Re}(s)-1/2)})$ and $J(x) = \frac12(x + x^{-1}) - 1$.

background

The module sits inside the NumberTheory layer and imports DiscretenessForcing and LawOfExistence. DiscretenessForcing states that $J(x) = \frac12(x + x^{-1}) - 1$ has a unique minimum at $x=1$; in logarithmic coordinates this is the convex bowl $J(e^t) = \cosh(t) - 1$ centered at $t=0$. LawOfExistence supplies the equivalence "$x$ exists $\iff$ defect$(x)=0$". These two results are applied to the defect coordinate $x = e^{2(\operatorname{Re}(s)-1/2)}$ that converts the real part of a complex point into a positive real variable whose J-cost vanishes exactly on the line $\operatorname{Re}(s)=1/2$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the zero-location cost observables (zeroDefect, zeroDeviation, OnCriticalLine) that are imported by CompletedXiSymmetry, XiJBridge, ZeroCompositionLaw and ZeroDoublingLaw. XiJBridge records the functional-equation symmetry $\xi(s)=\xi(1-s)$ as J-symmetry under the same coordinate map; ZeroCompositionLaw and ZeroDoublingLaw then lift the RCL to recurrence relations on these defects. The definitions therefore close the interface between the J-cost landscape and the completed xi functional equation.

scope and limits

Does not contain any analytic continuation or explicit zero computations.
Does not prove the Riemann Hypothesis or any conditional form of it.
Does not import or use the classical functional equation of $\xi(s)$ beyond the imported foundations.
Does not address multiplicity or spacing of zeros.

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