rightHalfPlaneDiskChart
plain-language theorem explainer
The definition supplies a concrete conformal chart from the right half-strip to the unit disk by shifting the critical line to the imaginary axis and applying the Cayley transform. Analysts working on Pick-matrix positivity for the xi function or zero-free regions would cite this chart when reducing the Riemann hypothesis to Schur bounds. The construction is a direct definition whose maps-to-disk property follows from one application of the strict Cayley norm lemma after real-part simplification.
Claim. Define the map $φ(s) = cayley(s - 1/2)$ on the right half-strip (the region $Re(s) > 1/2$), where $cayley$ is the standard Cayley transform sending the open right half-plane to the open unit disk. This yields a disk chart satisfying $‖φ(s)‖ < 1$ for every $s$ in the right half-strip.
background
The module XiSensorPickPositivity develops an unconditional algebraic route to Pick/Schur positivity for the xi-sensor Cayley field. A HalfStripDiskChart is any map $φ: ℂ → ℂ$ satisfying $‖φ(s)‖ < 1$ whenever $s$ lies in the right half-strip (the open region to the right of the critical line). The present definition realizes this abstract structure by the explicit shift $s ↦ s - 1/2$ followed by the Cayley transform, which translates the critical line to the imaginary axis before mapping the resulting right half-plane into the unit disk.
proof idea
The definition supplies the map $φ(s) := cayley(s - 1/2)$ and discharges the maps-to-disk obligation by a single application of the norm-cayley-lt-one-of-re-pos lemma. After simp on the real part of the shifted argument, the hypothesis that $s$ belongs to the right half-strip is rewritten as a positive real-part condition and fed directly to the lemma.
why it matters
This chart is the first concrete coordinate system required by the module's route from finite Pick positivity to the pointwise Schur bound. It feeds the one-point and finite Pick positivity statements that precede the missing analytic step: showing that the resulting Schur bound excludes poles of ξ'/ξ inside the right half-strip. In the Recognition Science setting the construction supports the unconditional written path that avoids any bounded-defect-cost hypothesis, consistent with the T5 J-uniqueness and RCL landmarks, while the analytic closure of the argument remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.