XiSensorPickRouteStatus
plain-language theorem explainer
XiSensorPickRouteStatus packages the algebraic implication that finite Pick positivity yields the Schur bound on the right half-strip together with a placeholder for the analytic no-poles step. Number theorists assembling a Pick-matrix route to a zero-free region for xi would cite this record when chaining positivity to contractivity. The declaration is a pure structure definition with no proof obligations or lemmas applied.
Claim. A status record for the xi-sensor Pick route consisting of: (i) for every conformal chart mapping the right half-strip into the unit disk and every xi-Cayley field $X$, finite Pick positivity of $X$ implies that $||X(s)||$ is at most 1 for all $s$ in the right half-strip; (ii) for every xi-Cayley field $X$, the Schur no-poles principle applied to $X$ yields a proposition.
background
The XiSensorPickPositivity module targets Pick/Schur positivity for the xi-sensor Cayley field without assuming bounded defect cost, since the unconditional route is already RH-equivalent. HalfStripDiskChart abstracts any conformal map from the right half-strip to the open unit disk. XiCayleyField denotes the abstract field $X(s) = (2(xi'/xi)(s)-1)/(2(xi'/xi)(s)+1)$. FinitePickPositive packages one-point positivity with a placeholder for finite matrices. SchurOnRightHalfStrip asserts the pointwise bound $||X(s)|| <= 1$ inside the right half-strip. XiSchurNoPolesPrinciple states that this bound implies the critical-strip zero-free bridge.
proof idea
The declaration is a structure definition that simply declares the two fields pick_to_schur and schur_to_zero_free_open. No tactics or lemmas are applied inside the structure itself; it serves only as a typed bundle for the algebraic implication and the analytic placeholder.
why it matters
This structure is instantiated by xiSensorPickRouteStatus, which discharges the first field via schur_of_finitePickPositive while leaving the second as a trivial implication to True. It records the algebraic step in the module's strategy toward excluding poles of xi'/xi in the right half-strip via Schur contractivity. The remaining analytic step is the removable-singularity argument that would close the critical-strip bridge. In the Recognition framework this supplies the interface needed before the phi-ladder and mass-formula constructions can invoke a zero-free region.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.