norm_cayley_lt_one_of_re_pos
plain-language theorem explainer
Analysts working on the Riemann hypothesis via Pick-Nevanlinna interpolation cite this bound when mapping the open right half-plane into the unit disk for the xi-sensor Cayley field. It supplies the strict contraction property required by the disk-chart construction in the positivity argument. The proof reduces the norm inequality to a direct comparison of squared norms via the algebraic identity for normSq(z+1) minus normSq(z-1), followed by division and extraction of the square root.
Claim. If $z$ is a complex number with positive real part, then the modulus of the Cayley transform $(z-1)/(z+1)$ is strictly less than one.
background
The Cayley transform is the map sending the open right half-plane to the open unit disk, defined by cayley(z) = (z-1)/(z+1). The module XiSensorPickPositivity develops the algebraic facts needed for Pick/Schur positivity of the xi-sensor Cayley field without assuming bounded defect cost. The upstream identity Complex.normSq(z+1) - Complex.normSq(z-1) = 4 * z.re is obtained by expanding the squared-norm formula in real and imaginary coordinates and simplifying by ring arithmetic.
proof idea
The argument first shows z+1 is nonzero by contradiction: z = -1 would imply negative real part, violating the hypothesis. It then applies the norm-square difference identity to obtain normSq(z-1) < normSq(z+1). Division yields the squared modulus of the transform less than one; non-negativity of the modulus and nlinarith extract the strict inequality on the modulus itself, after which the definition of cayley is substituted.
why it matters
The result is invoked inside rightHalfPlaneDiskChart to define the chart map from the right half-strip to the disk. It supplies the first nontrivial algebraic step in the module's route toward finite Pick positivity implying the pointwise Schur bound. In the Recognition framework this supports the missing analytic step that would exclude poles of xi'/xi in the right half-strip, advancing the unconditional Pick/Schur positivity argument for the xi function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.