`ZeroWindingCert`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.EulerCarrierComplex
domain: NumberTheory
line: 123 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.EulerCarrierComplex on GitHub at line 123.

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

 120
 121/-- A zero-winding certificate: the function has zero winding around every
 122interior circle. This is the interface consumed by the sampled-trace layer. -/
 123structure ZeroWindingCert where
 124  center : ℂ
 125  radius : ℝ
 126  radius_pos : 0 < radius
 127  cert : ComplexCarrierCert
 128  cert_match : cert.center = center ∧ cert.radius = radius
 129  zero_winding : ∀ (r : ℝ), 0 < r → r < radius →
 130    contourWinding cert r = 0
 131
 132/-- Extract a `ZeroWindingCert` from a `ComplexCarrierCert`. -/
 133def ComplexCarrierCert.toZeroWindingCert (cert : ComplexCarrierCert) :
 134    ZeroWindingCert where
 135  center := cert.center
 136  radius := cert.radius
 137  radius_pos := cert.radius_pos
 138  cert := cert
 139  cert_match := ⟨rfl, rfl⟩
 140  zero_winding := carrier_zero_winding cert
 141
 142/-- The Euler carrier's zero-winding certificate for any σ₀ > 1/2. -/
 143noncomputable def eulerZeroWindingCert (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 144    ZeroWindingCert :=
 145  (mkComplexCarrierCert σ₀ hσ).toZeroWindingCert
 146
 147end
 148
 149end EulerCarrierComplex
 150end NumberTheory
 151end IndisputableMonolith

papers checked against this theorem

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