schur_of_onePointPickPositive
plain-language theorem explainer
One-point Pick positivity for the xi-sensor Cayley field on the right half-strip implies the pointwise Schur bound. Analysts formalizing the Riemann hypothesis via Pick matrices cite this algebraic reduction. The proof is a short tactic sequence that clears the positive denominator from the positivity hypothesis and applies nonnegativity of the norm to conclude the desired inequality.
Claim. Let $φ$ be a conformal chart from the right half-strip to the open unit disk. Let $X$ be an abstract xi-sensor Cayley field. If $0 ≤ (1 - |X(s)|^2) / (1 - |φ(s)|^2)$ holds for every $s$ in the right half-strip, then $|X(s)| ≤ 1$ for every such $s$.
background
The module develops algebraic consequences of Pick positivity for the xi-sensor Cayley field without assuming bounded defect cost. HalfStripDiskChart is an abstract structure supplying a conformal map φ from the right half-strip to the unit disk with ||φ(s)|| < 1. XiCayleyField is the type of maps X : ℂ → ℂ intended to represent the Cayley transform of xi'/xi. OnePointPickPositive is the N=1 principal minor of the Pick matrix, requiring the displayed fractional inequality on the strip. SchurOnRightHalfStrip is the conclusion that ||X(s)|| ≤ 1 on the strip.
proof idea
The proof introduces an arbitrary s in the right half-strip. It establishes positivity of the denominator 1 - ||φ(s)||² from the chart mapping property. The hypothesis supplies nonnegativity of the fraction. Multiplication by the positive denominator yields nonnegativity of the numerator 1 - ||X(s)||². Nonnegativity of ||X(s)|| together with this fact implies ||X(s)|| ≤ 1 via nlinarith.
why it matters
This supplies the base case for the finite Pick positivity theorem in the same module, which applies it to the one-point component of the full Pick matrix. It advances the route to the Riemann hypothesis by establishing the Schur bound from the minimal positivity assumption, a prerequisite for the still-missing analytic argument that this bound precludes poles of xi'/xi in the right half-strip. The module documentation identifies it as the first nontrivial algebraic fact needed for the unconditional written route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.