IndisputableMonolith.Cost.ClassicalResults

   1import Mathlib
   2
   3/-!
   4# Classical Mathematical Results
   5
   6This module declares well-established mathematical results as axioms pending
   7full Lean formalization. Each axiom is justified with academic references.
   8
   9These are NOT new physical assumptions - they are standard mathematical facts
  10from real analysis, complex analysis, and functional equations that would
  11require substantial Mathlib infrastructure to prove formally.
  12
  13## Justification
  14
  15All axioms in this module are:
  161. **Textbook results** with multiple independent proofs in literature
  172. **Computationally verifiable** (can be checked numerically to arbitrary precision)
  183. **Used routinely** in mathematical physics without re-proving
  194. **Candidates for future formalization** when infrastructure is available
  20
  21## References
  22
  231. Aczél, J. (1966). *Lectures on Functional Equations and Their Applications*. Academic Press.
  242. Kuczma, M. (2009). *An Introduction to the Theory of Functional Equations and Inequalities*. Birkhäuser.
  253. Ahlfors, L. V. (1979). *Complex Analysis* (3rd ed.). McGraw-Hill.
  264. Conway, J. B. (1978). *Functions of One Complex Variable*. Springer.
  275. Apostol, T. M. (1974). *Mathematical Analysis* (2nd ed.). Addison-Wesley.
  286. Rudin, W. (1976). *Principles of Mathematical Analysis* (3rd ed.). McGraw-Hill.
  29
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Cost
  34namespace ClassicalResults
  35
  36open Real Complex
  37
  38/-! ## Provable Classical Results -/
  39
  40private lemma spherical_cap_pos (θmin : ℝ) (hθ : θmin ∈ Set.Icc (0 : ℝ) (Real.pi/2)) :
  41    0 ≤ (2 * Real.pi * (1 - Real.cos θmin)) := by
  42  have h1 : Real.cos θmin ≤ 1 := Real.cos_le_one θmin
  43  have h2 : 0 ≤ 1 - Real.cos θmin := by linarith
  44  have h3 : 0 ≤ 2 * Real.pi := by positivity
  45  exact mul_nonneg h3 h2
  46
  47private lemma exp_mul_rearrange (c₁ c₂ φ₁ φ₂ : ℝ) :
  48    Complex.exp (-(c₁+c₂)/2) * Complex.exp ((φ₁+φ₂) * I) =
  49    (Complex.exp (-c₁/2) * Complex.exp (φ₁ * I)) * (Complex.exp (-c₂/2) * Complex.exp (φ₂ * I)) := by
  50  rw [← Complex.exp_add, ← Complex.exp_add, ← Complex.exp_add, ← Complex.exp_add]
  51  congr 1
  52  push_cast
  53  ring
  54
  55/-- Provable version with integrability hypotheses -/
  56theorem piecewise_path_integral_additive_integrable (f : ℝ → ℝ) (a b c : ℝ)
  57    (hab : IntervalIntegrable f MeasureTheory.volume a b)
  58    (hbc : IntervalIntegrable f MeasureTheory.volume b c) :
  59    ∫ x in a..c, f x = (∫ x in a..b, f x) + (∫ x in b..c, f x) :=
  60  (intervalIntegral.integral_add_adjacent_intervals hab hbc).symm
  61
  62/-! ## Real/Complex Hyperbolic Functions -/
  63
  64theorem real_cosh_exponential_expansion (t : ℝ) :
  65    ((Real.exp t + Real.exp (-t)) / 2) = Real.cosh t := by
  66  simpa using (Real.cosh_eq t).symm
  67
  68/-! ## Complex Exponential Norms -/
  69
  70theorem complex_norm_exp_ofReal (r : ℝ) : ‖Complex.exp r‖ = Real.exp r := by
  71  rw [Complex.norm_exp]
  72  simp [Complex.ofReal_re]
  73
  74theorem complex_norm_exp_I_mul (θ : ℝ) : ‖Complex.exp (θ * I)‖ = 1 := by
  75  simpa using Complex.norm_exp_ofReal_mul_I θ
  76
  77/-! ## Trigonometric/logarithmic limits and monotonic consequences -/
  78
  79theorem neg_log_sin_tendsto_atTop_at_zero_right :
  80    Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by
  81  -- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞
  82  -- Use: f → -∞ implies -f → +∞
  83  rw [← Filter.tendsto_neg_atBot_iff]
  84  simp only [neg_neg]
  85  -- Now need: log(sin θ) → -∞ as θ → 0⁺
  86
  87  -- sin θ → 0 as θ → 0 (from continuity)
  88  have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by
  89    have h_cont : Continuous Real.sin := Real.continuous_sin
  90    simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds
  91
  92  -- sin θ > 0 near 0⁺ (eventually)
  93  have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by
  94    have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos
  95    filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi
  96    exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi
  97
  98  -- Combine: sin θ → 0⁺ as θ → 0⁺
  99  have h_sin_tends_zero_pos :
 100      Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by
 101    rw [tendsto_nhdsWithin_iff]
 102    exact ⟨h_sin_tends_zero, h_sin_pos⟩
 103
 104  -- log x → -∞ as x → 0⁺
 105  have h_log_atBot := Real.tendsto_log_nhdsGT_zero
 106
 107  -- Compose
 108  exact h_log_atBot.comp h_sin_tends_zero_pos
 109
 110theorem theta_min_spec_inequality :
 111    ∀ (Amax θ : ℝ), 0 < Amax → 0 < θ → θ ≤ π/2 →
 112      (- Real.log (Real.sin θ) ≤ Amax) →
 113      θ ≥ Real.arcsin (Real.exp (-Amax)) := by
 114  intro Amax θ _hAmax hθpos hθle hlog
 115  have h1 : Real.log (Real.sin θ) ≥ -Amax := by linarith
 116  have hsin_pos : 0 < Real.sin θ := Real.sin_pos_of_pos_of_lt_pi hθpos (by linarith [Real.pi_pos])
 117  have h2 : Real.sin θ ≥ Real.exp (-Amax) := by
 118    have := Real.exp_log hsin_pos
 119    rw [← this]
 120    exact Real.exp_le_exp.mpr h1
 121  have h3 : Real.arcsin (Real.sin θ) = θ := by
 122    apply Real.arcsin_sin
 123    · linarith
 124    · linarith [Real.pi_pos]
 125  rw [← h3]
 126  exact Real.arcsin_le_arcsin h2
 127
 128theorem theta_min_range :
 129    ∀ Amax > 0,
 130      0 < Real.arcsin (Real.exp (-Amax)) ∧ Real.arcsin (Real.exp (-Amax)) ≤ π/2 := by
 131  intro Amax hAmax
 132  constructor
 133  · rw [Real.arcsin_pos]
 134    exact Real.exp_pos _
 135  · exact Real.arcsin_le_pi_div_two _
 136
 137theorem spherical_cap_measure_bounds :
 138    ∀ θmin ∈ Set.Icc (0 : ℝ) (Real.pi/2),
 139      0 ≤ (2 * Real.pi * (1 - Real.cos θmin)) :=
 140  spherical_cap_pos
 141
 142/-! ## Complex Exponential Algebra -/
 143
 144theorem complex_exp_mul_rearrange :
 145    ∀ (c₁ c₂ φ₁ φ₂ : ℝ),
 146      Complex.exp (-(c₁+c₂)/2) * Complex.exp ((φ₁+φ₂) * I) =
 147      (Complex.exp (-c₁/2) * Complex.exp (φ₁ * I)) * (Complex.exp (-c₂/2) * Complex.exp (φ₂ * I)) :=
 148  exp_mul_rearrange
 149
 150/-!
 151NOTE: `continuousOn_extends_to_continuous` was removed because it is mathematically false.
 152Counterexample: `sin(1/x)` is continuous on `(0, ∞)` but has no continuous extension to `0`.
 153See `docs/FALSE_AXIOMS_ANALYSIS.md` for details.
 154-/
 155
 156end ClassicalResults
 157end Cost
 158end IndisputableMonolith
 159