IndisputableMonolith.Gravity.ILGRealExponentEnhancement

   1import Mathlib
   2import IndisputableMonolith.Gravity.ILGAsymptoticEnhancement
   3
   4/-!
   5# ILG real-exponent enhancement structural theorems
   6
   7Phase D9 extension: the natural-power version in
   8`IndisputableMonolith/Gravity/ILGAsymptoticEnhancement.lean` covers the
   9qualitative envelope; this module extends the structural facts to the
  10locked real exponent `α = 1 − 1/φ ∈ (0,1)` via `Real.rpow`.
  11
  12We prove four facts about the real-exponent radial enhancement
  13`w_real(R, r0, α) = 1 + C · (R/r0)^α`:
  14
  151. `enhancement_real_above_one` — `w_real > 1` for all positive `R, r0`
  16   when `0 < α`.
  172. `enhancement_real_strict_mono` — `w_real` is strictly monotone in `R`
  18   when `0 < α`.
  193. `enhancement_real_unbounded` — `w_real(R) → ∞` as `R → ∞` when `0 < α`.
  204. `ilg_real_velocity_sq_dominates_newtonian` — `V² ≥ V_bar²` everywhere.
  21
  22Lean: 0 sorry, 0 new axiom.
  23-/
  24
  25namespace IndisputableMonolith.Gravity.ILGRealExponentEnhancement
  26
  27open IndisputableMonolith.Gravity.ILGAsymptoticEnhancement
  28
  29noncomputable section
  30
  31/-- The real-exponent radial weight, with `α : ℝ` (no positivity required
  32    by the definition itself). -/
  33def w_real (R r0 α : ℝ) : ℝ := 1 + C_lock * (R / r0) ^ α
  34
  35theorem enhancement_real_pos (R r0 α : ℝ)
  36    (hR : 0 < R) (hr0 : 0 < r0) :
  37    0 < w_real R r0 α := by
  38  unfold w_real
  39  have hC : 0 < C_lock := C_lock_pos
  40  have hd : 0 < R / r0 := div_pos hR hr0
  41  have hpow : 0 < (R / r0) ^ α := Real.rpow_pos_of_pos hd α
  42  have : 0 < C_lock * (R / r0) ^ α := mul_pos hC hpow
  43  linarith
  44
  45theorem enhancement_real_above_one (R r0 α : ℝ)
  46    (hR : 0 < R) (hr0 : 0 < r0) :
  47    1 < w_real R r0 α := by
  48  unfold w_real
  49  have hC : 0 < C_lock := C_lock_pos
  50  have hd : 0 < R / r0 := div_pos hR hr0
  51  have hpow : 0 < (R / r0) ^ α := Real.rpow_pos_of_pos hd α
  52  have : 0 < C_lock * (R / r0) ^ α := mul_pos hC hpow
  53  linarith
  54
  55theorem enhancement_real_strict_mono (R₁ R₂ r0 α : ℝ)
  56    (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) (hr0 : 0 < r0) (hα : 0 < α) :
  57    w_real R₁ r0 α < w_real R₂ r0 α := by
  58  unfold w_real
  59  have hC : 0 < C_lock := C_lock_pos
  60  have h1 : 0 < R₁ / r0 := div_pos hR₁ hr0
  61  have h2 : 0 < R₂ / r0 := div_pos (lt_trans hR₁ hR₂) hr0
  62  have hd : R₁ / r0 < R₂ / r0 := by
  63    have hinv : 0 < r0⁻¹ := inv_pos.mpr hr0
  64    have : R₁ * r0⁻¹ < R₂ * r0⁻¹ := mul_lt_mul_of_pos_right hR₂ hinv
  65    simpa [div_eq_mul_inv] using this
  66  have hpow_lt : (R₁ / r0) ^ α < (R₂ / r0) ^ α :=
  67    Real.rpow_lt_rpow (le_of_lt h1) hd hα
  68  have hmul_lt : C_lock * (R₁ / r0) ^ α < C_lock * (R₂ / r0) ^ α :=
  69    mul_lt_mul_of_pos_left hpow_lt hC
  70  linarith
  71
  72/-- Newtonian-domination at the real-exponent level. -/
  73theorem ilg_real_velocity_sq_dominates_newtonian
  74    (V_bar_sq R r0 α : ℝ)
  75    (hVb : 0 ≤ V_bar_sq) (hR : 0 < R) (hr0 : 0 < r0) :
  76    V_bar_sq ≤ w_real R r0 α * V_bar_sq := by
  77  have hw : 1 < w_real R r0 α := enhancement_real_above_one R r0 α hR hr0
  78  have hwle : 1 ≤ w_real R r0 α := le_of_lt hw
  79  have : V_bar_sq * 1 ≤ V_bar_sq * w_real R r0 α :=
  80    mul_le_mul_of_nonneg_left hwle hVb
  81  linarith [mul_comm V_bar_sq (w_real R r0 α)]
  82
  83/-- Asymptotic divergence of the real-exponent enhancement. -/
  84theorem enhancement_real_unbounded (r0 α : ℝ)
  85    (hr0 : 0 < r0) (hα : 0 < α)
  86    (M : ℝ) (hM : 0 < M) :
  87    ∃ R : ℝ, 0 < R ∧ M < w_real R r0 α := by
  88  unfold w_real
  89  -- Want C_lock * (R/r0)^α > M, i.e. (R/r0)^α > M/C_lock.
  90  set u : ℝ := M / C_lock + 1 with hu_def
  91  have hC : 0 < C_lock := C_lock_pos
  92  have hu_pos : 0 < u := by
  93    have h₁ : 0 < M / C_lock := div_pos hM hC
  94    have : 0 < M / C_lock + 1 := by linarith
  95    simpa [hu_def] using this
  96  -- Choose y so that y^α = u, namely y = u^(1/α).
  97  have hα_ne : α ≠ 0 := ne_of_gt hα
  98  set y : ℝ := u ^ (1 / α) with hy_def
  99  have hy_pos : 0 < y := by
 100    have : 0 < u ^ (1 / α) := Real.rpow_pos_of_pos hu_pos (1 / α)
 101    simpa [hy_def] using this
 102  have hyα : y ^ α = u := by
 103    have h_inv : (1 / α) * α = 1 := by
 104      field_simp
 105    have hmul := Real.rpow_mul (le_of_lt hu_pos) (1 / α) α
 106    -- hmul : u ^ ((1/α) * α) = (u ^ (1/α)) ^ α
 107    rw [hy_def, ← hmul, h_inv, Real.rpow_one]
 108  -- Set R = r0 * y; then (R/r0)^α = y^α = u, and C_lock * u = M + C_lock > M.
 109  refine ⟨r0 * y, mul_pos hr0 hy_pos, ?bound⟩
 110  have hratio : (r0 * y) / r0 = y := by field_simp
 111  have hRpow : ((r0 * y) / r0) ^ α = u := by rw [hratio]; exact hyα
 112  have hCu : C_lock * u = M + C_lock := by
 113    have : C_lock * (M / C_lock + 1) = M + C_lock := by field_simp
 114    simpa [hu_def] using this
 115  have hCpos : 0 < C_lock := hC
 116  have : C_lock * ((r0 * y) / r0) ^ α = M + C_lock := by
 117    rw [hRpow]; exact hCu
 118  linarith
 119
 120/-- Certificate bundling the real-exponent envelope. -/
 121structure ILGRealExponentEnhancementCert where
 122  C_pos : 0 < C_lock
 123  enhancement_pos : ∀ R r0 α (hR : 0 < R) (hr0 : 0 < r0),
 124    0 < w_real R r0 α
 125  enhancement_above_one : ∀ R r0 α (hR : 0 < R) (hr0 : 0 < r0),
 126    1 < w_real R r0 α
 127  enhancement_strict_mono : ∀ R₁ R₂ r0 α (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂)
 128    (hr0 : 0 < r0) (hα : 0 < α), w_real R₁ r0 α < w_real R₂ r0 α
 129  enhancement_unbounded : ∀ r0 α (hr0 : 0 < r0) (hα : 0 < α) M (hM : 0 < M),
 130    ∃ R : ℝ, 0 < R ∧ M < w_real R r0 α
 131  newtonian_dominated : ∀ V_bar_sq R r0 α (hVb : 0 ≤ V_bar_sq)
 132    (hR : 0 < R) (hr0 : 0 < r0), V_bar_sq ≤ w_real R r0 α * V_bar_sq
 133
 134theorem ilgRealExponentEnhancementCert_holds : Nonempty ILGRealExponentEnhancementCert :=
 135  ⟨{ C_pos := C_lock_pos
 136     enhancement_pos := enhancement_real_pos
 137     enhancement_above_one := enhancement_real_above_one
 138     enhancement_strict_mono := enhancement_real_strict_mono
 139     enhancement_unbounded := enhancement_real_unbounded
 140     newtonian_dominated := ilg_real_velocity_sq_dominates_newtonian }⟩
 141
 142end
 143
 144end IndisputableMonolith.Gravity.ILGRealExponentEnhancement
 145