eulerCostCoveringPackage

formal source

 769  refine ⟨eulerBudgetedCarrier σ₀ hσ, rfl, rfl⟩
 770
 771/-- Package the concrete Euler budgeted carrier. -/
 772noncomputable def eulerCostCoveringPackage (σ₀ : ℝ) (hσ : 1/2 < σ₀) : CostCoveringPackage where
 773  carrier := eulerBudgetedCarrier σ₀ hσ
 774
 775/-! ### §7b. Complex-analysis axioms for RH -/
 776
 777/-- **Axiom 1 (Argument Principle Sampling).**
 778
 779Standard complex analysis: if ζ has a zero of order `m` at ρ with Re(ρ) > 1/2,
 780then sampling the phase of ζ(s)⁻¹ on `N` concentric rings around ρ produces an
 781annular mesh whose per-ring winding is exactly `m`.
 782
 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