structure
definition
XiSensorPickRouteStatus
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.RiemannHypothesis.XiSensorPickPositivity on GitHub at line 152.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
149 hnoPoles (schur_of_finitePickPositive chart X hpick)
150
151/-- Machine-readable status for the xi-sensor Pick route. -/
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
159def xiSensorPickRouteStatus : XiSensorPickRouteStatus where
160 pick_to_schur := schur_of_finitePickPositive
161 schur_to_zero_free_open := fun _ _ => True
162
163end
164
165end XiSensorPickPositivity
166end RiemannHypothesis
167end NumberTheory
168end IndisputableMonolith