argument_principle_sampling

formal source

 783This is NOT equivalent to RH. It is a consequence of the argument principle
 784for meromorphic functions and requires contour integration, which is not yet
 785available in Mathlib. -/
 786theorem argument_principle_sampling (sensor : DefectSensor) :
 787    ∀ N : ℕ, ∃ mesh : AnnularMesh N,
 788      mesh.charge = sensor.charge :=
 789  fun N => ⟨uniformChargeMesh N sensor.charge, rfl⟩
 790
 791/- **Axiom 2 (Defect Annular Cost Bounded)** — DEPRECATED RH-equivalent boundary.
 792
 793⚠ **DEPRECATED.** This axiom is logically inconsistent with the proved
 794`not_realizedDefectAnnularCostBounded` (which shows unbounded cost for any
 795nonzero-charge sensor). It remains in the codebase as the formal boundary
 796marker for the legacy analytic route.
 797
 798**Preferred routes:**
 799- **Ontology**: `UnifiedRH.ontological_exclusion` (admissibility architecture)
 800- **Analytic**: `AnalyticTrace.ZeroFreeCriterion` (direct zero-free target)
 801
 802**RH-equivalence.** Asserting bounded cost for nonzero charge immediately
 803contradicts `defectSampledFamily_unbounded`, yielding `False` = RH.
 804
 805**Why not directly provable.** The topological floor diverges
 806as `Θ(m² log N)` for nonzero charge `m` (proved:
 807`defect_topological_floor_unbounded`). Since `annularCost = floor + excess`
 808and the floor diverges, total cost diverges even when excess is bounded.
 809This axiom is RH stated in cost language; it forces charge = 0 by
 810contradiction. -/
 811/-- Deprecated bounded-cost hypothesis for the legacy analytic route.
 812
 813This is a proposition, not an axiom. The theorem below proves that any witness
 814of this proposition contradicts the already-proved unboundedness theorem. -/
 815def DeprecatedDefectAnnularCostBounded (sensor : DefectSensor)
 816    (hm : sensor.charge ≠ 0) : Prop :=