IndisputableMonolith.NumberTheory.RiemannHypothesis.XiSensorPickPositivity
This module sets up the open right half of the critical strip as the working domain for Schur-class and positivity arguments in the BRF route to the Riemann hypothesis. Researchers formalizing analytic number theory or bounded-real-function proofs of RH would cite the definitions and charts it supplies. The module structures its content by importing the Cayley-Schur plumbing and the proven zero-free region on Re(s) ≥ 1.
claimThe open right half of the critical strip is the domain $\{ s \in \mathbb{C} \mid \operatorname{Re}(s) > 1/2 \}$ inside $0 < \operatorname{Re}(s) < 1$, equipped with Cayley transforms and Pick-positive functions for the Schur class.
background
BRFPlumbing defines a function H as Herglotz when $0 \leq \operatorname{Re} H$, with Cayley transform $\Theta = (H-1)/(H+1)$ Schur when $|\Theta| \leq 1$. StripZeroFreeRegion records the Mathlib zero-free result on the half-plane $\operatorname{Re}(s) \geq 1$ as Phase 5 of the RS-native zeta program. The present module supplies the local domain and auxiliary charts (RightHalfStrip, XiCayleyField, HalfStripDiskChart) needed to apply these transforms inside the critical strip.
proof idea
This is a definition module, no proofs. It assembles the right-half-strip objects by importing the two upstream modules and declaring the sibling definitions that later lemmas (OnePointPickPositive, SchurOnRightHalfStrip) will use.
why it matters in Recognition Science
The module supplies the domain for the BRF/Schur route to RH and feeds the downstream lemmas on pick positivity and the critical-strip bridge. It fills the setup step between the zero-free region on Re(s) ≥ 1 and the algebraic Schur principle inside the strip.
scope and limits
- Does not prove zero-freeness inside the critical strip.
- Does not contain the full Schur-no-poles principle.
- Does not import or define the zeta function itself.
- Does not address the left half of the strip.
depends on (2)
declarations in this module (14)
-
def
RightHalfStrip -
abbrev
XiCayleyField -
structure
HalfStripDiskChart -
theorem
norm_cayley_lt_one_of_re_pos -
def
rightHalfPlaneDiskChart -
def
OnePointPickPositive -
structure
FinitePickPositive -
def
SchurOnRightHalfStrip -
theorem
schur_of_onePointPickPositive -
theorem
schur_of_finitePickPositive -
def
XiSchurNoPolesPrinciple -
theorem
criticalStripBridge_of_pickPositive -
structure
XiSensorPickRouteStatus -
def
xiSensorPickRouteStatus