RightHalfStrip
plain-language theorem explainer
RightHalfStrip specifies the open right half of the critical strip as the set of complex s with 1/2 < Re(s) < 1. Analysts formalizing Pick and Schur positivity for the xi-sensor Cayley field in the Recognition Science route to the Riemann hypothesis would cite this region to localize their domain restrictions. The declaration is a direct predicate definition with no proof steps.
Claim. The predicate holds for $s$ in the open right half of the critical strip precisely when $1/2 < Re(s) < 1$.
background
This definition sits in the XiSensorPickPositivity module, which develops the first algebraic facts needed for Pick/Schur positivity of the xi-sensor Cayley field X(s) = (2*(xi'/xi)(s) - 1)/(2*(xi'/xi)(s) + 1). The module documentation states that the unconditional route should not assume bounded defect cost (already RH-equivalent) and targets positivity statements inside the right half-strip instead.
proof idea
The definition is introduced directly as the conjunction 1/2 < s.re ∧ s.re < 1, serving as the domain predicate for the HalfStripDiskChart structure and the quantifiers in OnePointPickPositive and SchurOnRightHalfStrip.
why it matters
RightHalfStrip supplies the precise domain for the disk chart φ and the positivity statements OnePointPickPositive and SchurOnRightHalfStrip. These advance the module goal of showing that one-point Pick positivity forces the pointwise Schur bound, a step toward excluding poles of xi'/xi in the right half-strip. The construction supports the Recognition Science program of deriving RH properties from the xi-sensor field without extra defect-cost assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.