`WitnessedDefectSensor`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.EulerInstantiation
domain: NumberTheory
line: 581 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.EulerInstantiation on GitHub at line 581.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 578The existing `DefectSensor` only records charge and real part; this stronger
 579structure remembers the full center `ρ` and the analytic witness that the
 580charge comes from `zetaReciprocal` itself. -/
 581structure WitnessedDefectSensor where
 582  rho : ℂ
 583  charge : ℤ
 584  in_strip : 1/2 < rho.re ∧ rho.re < 1
 585  order_witness : meromorphicOrderAt zetaReciprocal rho = ↑(-charge)
 586
 587/-- Forget the complex witness and retain only the abstract charge/real-part
 588sensor data used by the annular-cost framework. -/
 589def WitnessedDefectSensor.toDefectSensor (sensor : WitnessedDefectSensor) : DefectSensor where
 590  charge := sensor.charge
 591  realPart := sensor.rho.re
 592  in_strip := sensor.in_strip
 593
 594@[simp] theorem WitnessedDefectSensor.toDefectSensor_charge
 595    (sensor : WitnessedDefectSensor) :
 596    sensor.toDefectSensor.charge = sensor.charge := rfl
 597
 598@[simp] theorem WitnessedDefectSensor.toDefectSensor_realPart
 599    (sensor : WitnessedDefectSensor) :
 600    sensor.toDefectSensor.realPart = sensor.rho.re := rfl
 601
 602/-- A witnessed strip sensor is automatically away from the pole `s = 1`. -/
 603theorem WitnessedDefectSensor.rho_ne_one (sensor : WitnessedDefectSensor) :
 604    sensor.rho ≠ 1 := by
 605  intro h
 606  have hre : sensor.rho.re = 1 := by simpa [h]
 607  linarith [sensor.in_strip.2]
 608
 609/-- A local meromorphic factorization of `zetaReciprocal` at a hypothetical
 610zero ρ of ζ in the strip. The regular factor `g` is analytic and nonvanishing
 611on a closed disk, extracted from Mathlib's `meromorphicOrderAt_eq_int_iff`. -/

papers checked against this theorem

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