FinitePickPositive
plain-language theorem explainer
FinitePickPositive packages full finite Pick positivity for the xi-sensor Cayley field over an abstract half-strip disk chart as a structure. It explicitly carries the one-point positivity condition because that is the only part used at theorem strength downstream. Researchers working on the Pick/Schur route to a zero-free region for xi would cite this interface. It is introduced purely as a definition with the second field set to True.
Claim. Let $C$ be a conformal chart from the right half-strip to the open unit disk and let $X$ be the xi-sensor Cayley field. Finite Pick positivity is the structure consisting of the one-point condition that $0 ≤ (1 - |X(s)|^2)/(1 - |C(s)|^2)$ for every $s$ in the right half-strip, together with the trivial assertion that the finite matrices are positive.
background
The XiSensorPickPositivity module develops the unconditional algebraic route to Pick/Schur positivity for the xi-sensor Cayley field on the right half-strip; the module document states that bounded defect cost is already RH-equivalent and therefore avoided. HalfStripDiskChart supplies an arbitrary conformal map φ into the unit disk that sends the right half-strip inside the open unit disk. XiCayleyField is the abstract map X(s) = (2(ξ'/ξ)(s) - 1)/(2(ξ'/ξ)(s) + 1). OnePointPickPositive is the N = 1 principal minor: the inequality 0 ≤ (1 - |X(s)|^2)/(1 - |φ(s)|^2) for all s in the right half-strip.
proof idea
FinitePickPositive is introduced as a bare structure definition whose only non-trivial field is the one_point projection carrying the OnePointPickPositive proposition; the finite_matrices_positive field is set to True. No lemmas are invoked and no tactics are used.
why it matters
The structure supplies the hypothesis for schur_of_finitePickPositive, which extracts the pointwise Schur bound on the right half-strip, and for criticalStripBridge_of_pickPositive, which combines that bound with the XiSchurNoPolesPrinciple to obtain the critical-strip zero-free bridge. It therefore fills the first algebraic step in the xi-sensor Pick route toward excluding poles of ξ'/ξ in the right half-strip, a prerequisite for the Riemann hypothesis zero-free region in the Recognition Science formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.