XiSensorPickRouteStatus
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove the analytic implication from Schur bound to absence of poles of xi'/xi.
- Does not supply a concrete disk chart or explicit xi-Cayley field.
- Does not assume or prove bounded defect cost.
- Does not address full finite-matrix positivity beyond the one-point case.
Lean usage
def xiSensorPickRouteStatus : XiSensorPickRouteStatus where pick_to_schur := schur_of_finitePickPositive schur_to_zero_free_open := fun _ _ => Trueformal statement (Lean)
152structure XiSensorPickRouteStatus where
153 pick_to_schur :
154 ∀ (chart : HalfStripDiskChart) (X : XiCayleyField),
155 FinitePickPositive chart X → SchurOnRightHalfStrip X
156 schur_to_zero_free_open :
157 ∀ X : XiCayleyField, XiSchurNoPolesPrinciple X → Prop
158