charge_zero_of_covered

formal source

  83  not_DefectTopologicalFloorCovered _ sensor hm
  84
  85/-- If floor coverage holds for the sampled package, the charge must be 0. -/
  86theorem charge_zero_of_covered (σ₀ : ℝ) (hσ : 1/2 < σ₀)
  87    (sensor : DefectSensor)
  88    (hcover : DefectTopologicalFloorCovered (eulerSampledCoveringPackage σ₀ hσ) sensor) :
  89    sensor.charge = 0 :=
  90  (floorCovered_iff_charge_zero σ₀ hσ sensor).mp hcover
  91
  92/-! ### §4. Zero-free criterion (analytic route target) -/
  93
  94/-- The zero-free criterion for the pure analytic route.
  95
  96This structure packages the honest analytic target: witnessed ζ⁻¹ defect data
  97in the strip gives an honest phase-family package, and analytic estimates then
  98force the corresponding defect charge to vanish.
  99
 100**Field status (April 2026):**
 101- `logDeriv_bounded_on_strip`: **PROVED** (`carrierDerivBound_pos`).
 102- `carrier_nonvanishing_on_strip`: **PROVED** (`carrier_nonvanishing`).
 103- `honest_phase_family`: **PROVED** via `honest_argument_principle_phase_family`,
 104  now using `zetaDerivedPhaseFamily` (genuine phase data from meromorphic
 105  factorization) rather than the former `trivialDefectPhaseFamily` scaffold.
 106- `charge_zero_of_honest_phase`: **NARROWED TARGET**. Honest phase data now
 107  comes with a canonical perturbation witness, and the present sampled family
 108  sits exactly on the topological floor (`annularExcess = 0`). The remaining
 109  content is to upgrade the honest sampled family to bounded total cost / floor
 110  coverage, forcing charge = 0.
 111
 112This replaces the deprecated `defect_annular_cost_bounded` as the proper
 113analytic-route target. -/
 114structure ZeroFreeCriterion where
 115  logDeriv_bounded_on_strip :
 116    ∀ σ, 1/2 < σ → 0 < carrierDerivBound σ