OnePointPickPositive
plain-language theorem explainer
OnePointPickPositive encodes the one-point Pick positivity inequality for an abstract conformal chart from the right half-strip into the unit disk and the xi-sensor Cayley field X. Researchers pursuing the Recognition Science route to the Riemann Hypothesis via Schur-Pick theory cite it as the N=1 principal minor of the full Pick matrix. The declaration is a direct definition of the required non-negative ratio without any reduction steps or lemmas.
Claim. Let $φ$ be any conformal chart from the right half-strip into the open unit disk and let $X$ be the Cayley transform of the logarithmic derivative of the Riemann xi function. One-point Pick positivity asserts that $0 ≤ (1 - |X(s)|^2) / (1 - |φ(s)|^2)$ holds for every $s$ in the right half-strip.
background
The module develops an unconditional approach to the Riemann Hypothesis that targets Pick/Schur positivity for the xi-sensor Cayley field without assuming bounded defect cost. XiCayleyField is the abstract map $X(s) = (2(ξ'/ξ)(s) - 1)/(2(ξ'/ξ)(s) + 1)$. HalfStripDiskChart is a structure supplying a map φ that sends every point of the right half-strip strictly inside the unit disk. RightHalfStrip is the region of positive real part with imaginary part confined to a vertical strip; the inequality is the N=1 principal minor of the associated Pick matrix.
proof idea
As a definition the declaration states the inequality directly. No lemmas are applied and no tactics are used; the body is simply the universal quantification over the right half-strip of the displayed non-negative ratio.
why it matters
The definition supplies the one-point component required by the structure FinitePickPositive and is the hypothesis of the theorem schur_of_onePointPickPositive that derives the pointwise Schur bound on the right half-strip. It advances the Recognition Science forcing chain by furnishing the algebraic positivity condition needed to exclude poles of ξ'/ξ. The module records that the remaining analytic step, showing the Schur bound rules out such poles, is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.