`ArgumentPrincipleSensorCert`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor
domain: NumberTheory
line: 30 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.ArgumentPrincipleSensor on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  27
  28/-- Argument-principle data: a witnessed defect sensor carries genuine
  29zeta-derived phase-family data. -/
  30structure ArgumentPrincipleSensorCert where
  31  witnessed_phase_family :
  32    ∀ sensor : WitnessedDefectSensor, sensor.charge ≠ 0 →
  33      ∃ zfd : ZetaPhaseFamilyData,
  34        zfd.sensor = sensor.toDefectSensor ∧
  35          zfd.phaseFamily.sensor = sensor.toDefectSensor
  36  zero_gives_charged_sensor :
  37    ∀ ρ : ℂ, riemannZeta ρ = 0 → 1 / 2 < ρ.re → ρ.re < 1 →
  38      ∃ sensor : DefectSensor, sensor.charge ≠ 0 ∧ sensor.realPart = ρ.re
  39
  40/-- The current argument-principle sensor certificate. -/
  41def argumentPrincipleSensorCert : ArgumentPrincipleSensorCert where
  42  witnessed_phase_family := fun sensor hm =>
  43    honest_argument_principle_phase_family sensor hm
  44  zero_gives_charged_sensor := zeta_zero_gives_charged_sensor
  45
  46end NumberTheory
  47end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.