DeprecatedDefectAnnularCostBounded

formal source

 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 :=
 817  ∃ K : ℝ, ∀ N : ℕ,
 818    annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) ≤ K
 819
 820/-- **Formal inconsistency proof.**
 821
 822The axiom `defect_annular_cost_bounded` is logically inconsistent with
 823`not_realizedDefectAnnularCostBounded`, which proves that bounded cost is
 824impossible for any sampled family with nonzero charge. This theorem
 825makes the inconsistency machine-checkable so it cannot be overlooked. -/
 826theorem defect_annular_cost_bounded_inconsistent (sensor : DefectSensor)
 827    (hm : sensor.charge ≠ 0)
 828    (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) : False := by
 829  let fam := canonicalDefectSampledFamily sensor hm
 830  have hfam : fam.sensor.charge ≠ 0 := by
 831    simpa [fam, canonicalDefectSampledFamily_sensor] using hm
 832  obtain ⟨K, hK⟩ := hbounded
 833  obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hfam K
 834  exact not_lt_of_ge (hK N) hN
 835
 836/-- **RH from the deprecated bounded-cost axiom (legacy path).**
 837
 838⚠ **INCONSISTENT**: derives `False` from the contradictory axiom
 839`defect_annular_cost_bounded`. See `defect_annular_cost_bounded_inconsistent`.
 840For the preferred path, see `UnifiedRH.unified_rh` (ontology) or
 841`AnalyticTrace.ZeroFreeCriterion` (analytic). -/
 842theorem rh_from_complex_analysis_axioms (sensor : DefectSensor)
 843    (hm : sensor.charge ≠ 0)
 844    (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) : False :=
 845  defect_annular_cost_bounded_inconsistent sensor hm hbounded