classical_zfr

formal source

  45  width_pos : ∀ t, 1 < t → 0 < width t
  46  width_decreasing : ∀ t₁ t₂, 1 < t₁ → t₁ < t₂ → width t₂ ≤ width t₁
  47
  48def classical_zfr (c : ℝ) (hc : 0 < c) : ZeroFreeRegion where
  49  width := fun t => c / Real.log t
  50  width_pos := by
  51    intro t ht
  52    exact div_pos hc (Real.log_pos ht)
  53  width_decreasing := by
  54    intro t₁ t₂ ht₁ ht₁₂
  55    apply div_le_div_of_nonneg_left (le_of_lt hc) (Real.log_pos ht₁)
  56    exact Real.log_le_log (by linarith) (le_of_lt ht₁₂)
  57
  58/-! ## Defect Budget Bound
  59
  60The RS defect-budget bridge constrains the total defect in the ledger.
  61This translates to a constraint on zeta zeros via the explicit formula. -/
  62
  63structure DefectBudget where
  64  total_defect : ℝ
  65  defect_positive : 0 < total_defect
  66  defect_bounded : total_defect ≤ 1  -- normalized
  67
  68theorem defect_implies_zero_free (db : DefectBudget) :
  69    ∃ c : ℝ, 0 < c ∧ ∀ t, 1 < t → c / Real.log t > 0 := by
  70  use db.total_defect
  71  exact ⟨db.defect_positive, fun t ht => div_pos db.defect_positive (Real.log_pos ht)⟩
  72
  73/-! ## RS Chain Sufficiency
  74
  75The RS number theory chain needs only the classical zero-free region,
  76not the full Riemann Hypothesis. -/
  77
  78structure RSChainRequirements where