XiCayleyField
plain-language theorem explainer
XiCayleyField names the function space of maps from the complex plane to itself that carries the Cayley transform of the xi-sensor. Number theorists working on an unconditional Riemann hypothesis proof via Schur-Pick positivity on the right half-strip cite this abbreviation as the carrier for the positivity predicates. The declaration is a direct type alias with no computational content or additional axioms.
Claim. Let $X : {}$ be the abstract xi-sensor Cayley field. In the intended application it takes the explicit form $X(s) = (2 (xi'/xi)(s) - 1) / (2 (xi'/xi)(s) + 1)$.
background
The module develops the algebraic steps for Pick/Schur positivity of the xi-sensor Cayley field without assuming bounded defect cost, already known to be RH-equivalent. The xi function is the completed Riemann zeta function, and the Cayley field is the image of its logarithmic derivative under the Möbius map that sends the right half-plane to the unit disk. The local target is the pointwise Schur bound on the right half-strip, which would exclude poles of xi'/xi there.
proof idea
The declaration is a one-line abbreviation that identifies the type with maps from the complex numbers to the complex numbers. No lemmas or tactics are invoked.
why it matters
XiCayleyField supplies the function space for OnePointPickPositive and FinitePickPositive. These feed schur_of_onePointPickPositive and schur_of_finitePickPositive, which in turn support criticalStripBridge_of_pickPositive. The bridge combines finite Pick positivity with the XiSchurNoPolesPrinciple to obtain the CriticalStripZeroFreeBridge. In the Recognition Science setting this advances the analytic step that connects the T5 J-uniqueness and T8 D=3 forcing chain to zero-free regions in the critical strip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.