IndisputableMonolith.Gravity.ILGDerivation

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Gravity.ILG
   4
   5namespace IndisputableMonolith.Gravity.ILG
   6
   7open Constants
   8
   9/-- **THEOREM: ILG Time-Kernel Derivation**
  10    The time-kernel $w_t$ is uniquely determined by the recognition lag $C_{lag} = \varphi^{-5}$
  11    and the fine-structure exponent $\alpha$.
  12
  13    This theorem formalizes the connection between the RRF gradient cost and the
  14    effective modified gravity at large scales. -/
  15theorem w_t_formula_grounded (P : Params) (Tdyn τ0 : ℝ) :
  16    P.Clag = phi ^ (-(5 : ℝ)) →
  17    P.alpha = (1 - 1/phi) / 2 →
  18    w_t P Tdyn τ0
  19      = 1 + (phi ^ (-(5 : ℝ)))
  20          * (Real.rpow (max defaultConfig.eps_t (Tdyn / τ0)) ((1 - 1/phi) / 2) - 1) := by
  21  intro hClag hAlpha
  22  simp [w_t, w_t_with, hClag, hAlpha]
  23
  24/-- **Kernel strict monotonicity (rotational flattening, part 1).**
  25    On the un-clamped region (`eps_t ≤ Tdyn/τ0`), the ILG time-kernel is
  26    strictly increasing in the dynamical time whenever `alpha > 0` and
  27    `Clag > 0`. Longer orbits get a strictly larger recognition-lag
  28    enhancement, so the ILG rotation curve decays strictly slower than
  29    Keplerian at every radius: `w(T₂)·K/r₂ ÷ w(T₁)·K/r₁ > (K/r₂)/(K/r₁)`. -/
  30theorem w_t_strictMono_unclamped (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
  31    (hα : 0 < P.alpha) (hC : 0 < P.Clag) :
  32    ∀ T₁ T₂ : ℝ, defaultConfig.eps_t ≤ T₁ / τ0 → T₁ < T₂ →
  33      w_t P T₁ τ0 < w_t P T₂ τ0 := by
  34  intro T₁ T₂ h1 hlt
  35  have heps : (0 : ℝ) < defaultConfig.eps_t := by norm_num [defaultConfig]
  36  have h1pos : (0 : ℝ) < T₁ / τ0 := lt_of_lt_of_le heps h1
  37  have hdiv : T₁ / τ0 < T₂ / τ0 := by gcongr
  38  have hm1 : max defaultConfig.eps_t (T₁ / τ0) = T₁ / τ0 := max_eq_right h1
  39  have hm2 : max defaultConfig.eps_t (T₂ / τ0) = T₂ / τ0 :=
  40    max_eq_right (le_trans h1 hdiv.le)
  41  have hr : Real.rpow (T₁ / τ0) P.alpha < Real.rpow (T₂ / τ0) P.alpha :=
  42    Real.rpow_lt_rpow h1pos.le hdiv hα
  43  simp only [w_t, w_t_with, hm1, hm2]
  44  nlinarith [hr, hC]
  45
  46/-- **Kernel divergence (rotational flattening, part 2).**
  47    For `alpha > 0`, `Clag > 0`, the enhancement is unbounded in the
  48    dynamical time: `w_t → ∞` as `Tdyn → ∞`. No finite radius exhausts the
  49    recognition-lag correction. -/
  50theorem w_t_tendsto_atTop (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
  51    (hα : 0 < P.alpha) (hC : 0 < P.Clag) :
  52    Filter.Tendsto (fun Tdyn => w_t P Tdyn τ0) Filter.atTop Filter.atTop := by
  53  have h1 : Filter.Tendsto (fun T : ℝ => T / τ0) Filter.atTop Filter.atTop :=
  54    Filter.tendsto_id.atTop_div_const hτ
  55  have h2 : Filter.Tendsto (fun T : ℝ => max defaultConfig.eps_t (T / τ0))
  56      Filter.atTop Filter.atTop :=
  57    Filter.tendsto_atTop_mono (fun T => le_max_right _ _) h1
  58  have h3 : Filter.Tendsto (fun t : ℝ => Real.rpow t P.alpha)
  59      Filter.atTop Filter.atTop := tendsto_rpow_atTop hα
  60  have h4 := h3.comp h2
  61  have h5 := Filter.tendsto_atTop_add_const_right Filter.atTop (-1 : ℝ) h4
  62  have h6 := Filter.Tendsto.const_mul_atTop hC h5
  63  have h7 := Filter.tendsto_atTop_add_const_left Filter.atTop (1 : ℝ) h6
  64  simpa [w_t, w_t_with, Function.comp, sub_eq_add_neg] using h7
  65
  66/-- **THEOREM: Rotational flattening forced (honest form).**
  67    Replaces the former vacuous placeholder (`∃ v_flat, ... ∀ r, True`, which
  68    proved nothing). What the ILG kernel actually forces, and what this
  69    theorem states: for `alpha > 0` and `Clag > 0` the enhancement
  70    (i) strictly grows with dynamical time on the un-clamped region, and
  71    (ii) diverges as `Tdyn → ∞`. Consequently the enhanced squared velocity
  72    `w_t(Tdyn(r)) · v_N(r)²` decays strictly slower than the Newtonian
  73    `v_N(r)² ∝ 1/r` at every scale, which is the structural content of
  74    "rotation curves flatten." The exact asymptotic velocity value is an
  75    empirical matter (SPARC fits), not a theorem, and is not claimed here. -/
  76theorem rotational_flatness_forced (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
  77    (hα : 0 < P.alpha) (hC : 0 < P.Clag) :
  78    (∀ T₁ T₂ : ℝ, defaultConfig.eps_t ≤ T₁ / τ0 → T₁ < T₂ →
  79      w_t P T₁ τ0 < w_t P T₂ τ0)
  80    ∧ Filter.Tendsto (fun Tdyn => w_t P Tdyn τ0) Filter.atTop Filter.atTop :=
  81  ⟨w_t_strictMono_unclamped P τ0 hτ hα hC, w_t_tendsto_atTop P τ0 hτ hα hC⟩
  82
  83/-- The enhancement exceeds every finite bound: for any `M` there is a
  84    dynamical time beyond which `w_t > M`. (Direct consequence of the
  85    divergence half of `rotational_flatness_forced`.) -/
  86theorem rotational_flatness_unbounded (P : Params) (τ0 : ℝ) (hτ : 0 < τ0)
  87    (hα : 0 < P.alpha) (hC : 0 < P.Clag) (M : ℝ) :
  88    ∃ T : ℝ, ∀ T' ≥ T, M < w_t P T' τ0 := by
  89  have h := (rotational_flatness_forced P τ0 hτ hα hC).2
  90  have hev : ∀ᶠ T' in Filter.atTop, M + 1 ≤ w_t P T' τ0 :=
  91    Filter.tendsto_atTop.mp h (M + 1)
  92  rcases Filter.eventually_atTop.mp hev with ⟨T, hT⟩
  93  exact ⟨T, fun T' hT' => lt_of_lt_of_le (by linarith) (hT T' hT')⟩
  94
  95end ILG
  96end IndisputableMonolith.Gravity
  97