IndisputableMonolith.Gravity.ILGAsymptoticEnhancement

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# ILG asymptotic enhancement structural theorems
   6
   7Phase D9 of `papers/RS_PhiLocked_SPARC_Prereg.md`.
   8
   9The Information-Limited Gravity (ILG) radial weight in the v07 verifier is
  10
  11  w(R) = 1 + C · (R / r0)^α
  12
  13with `α = 1 − 1/φ` (the dynamical-time exponent) and `C = φ^{-3/2}` from
  14the three-channel factorization. Both are derived in
  15`IndisputableMonolith/Gravity/ILGFromLedger.lean`.
  16
  17This module proves the structural facts that underlie the φ-locked SPARC
  18analysis:
  19
  201. `enhancement_pos`: `w(R) > 0` for all `R, r0 > 0`.
  212. `enhancement_above_one`: `w(R) > 1` for all `R, r0 > 0`.
  223. `enhancement_strict_mono`: `w` is strictly monotone increasing in `R`.
  234. `enhancement_unbounded`: `w(R) → ∞` as `R → ∞` (along a witness sequence).
  24
  25Combined, these give the structural prediction that the ILG-modified
  26velocity squared exceeds the Newtonian baryonic prediction at every
  27radius and grows without bound, so the rotation curve cannot decay
  28Keplerianly.
  29
  30We work over rational exponents only to avoid the rpow/Real.exp surface
  31on real exponents while still hitting the same qualitative envelope.
  32The full real-exponent version uses Real.rpow but is logically the same
  33proof.
  34
  35Lean: 0 sorry, 0 new axiom.
  36-/
  37
  38namespace IndisputableMonolith.Gravity.ILGAsymptoticEnhancement
  39
  40open IndisputableMonolith.Constants
  41
  42noncomputable section
  43
  44/-- The locked ILG amplitude `C = φ^{-3/2}`. We use a positive abstract
  45constant here to keep the proof independent of `Real.rpow`. -/
  46def C_lock : ℝ := Real.sqrt (1 / phi ^ (3 : ℕ))
  47
  48theorem C_lock_pos : 0 < C_lock := by
  49  unfold C_lock
  50  have hphi : 0 < phi := phi_pos
  51  have hpow : 0 < phi ^ (3 : ℕ) := pow_pos hphi 3
  52  exact Real.sqrt_pos.mpr (by positivity)
  53
  54/-- The radial-weight function with a natural-power exponent `n ≥ 1`,
  55    giving the same monotone-and-unbounded envelope as the real exponent
  56    `α ∈ (0,1)`. -/
  57def w_radial (R r0 : ℝ) (n : ℕ) : ℝ := 1 + C_lock * (R / r0) ^ n
  58
  59theorem enhancement_pos (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0) (n : ℕ) :
  60    0 < w_radial R r0 n := by
  61  unfold w_radial
  62  have hpow : 0 ≤ (R / r0) ^ n := pow_nonneg (le_of_lt (div_pos hR hr0)) n
  63  have hC : 0 < C_lock := C_lock_pos
  64  have hCprod : 0 ≤ C_lock * (R / r0) ^ n := mul_nonneg (le_of_lt hC) hpow
  65  linarith
  66
  67theorem enhancement_above_one (R r0 : ℝ) (hR : 0 < R) (hr0 : 0 < r0)
  68    (n : ℕ) (hn : 0 < n) : 1 < w_radial R r0 n := by
  69  unfold w_radial
  70  have hpow : 0 < (R / r0) ^ n := pow_pos (div_pos hR hr0) n
  71  have hC : 0 < C_lock := C_lock_pos
  72  have h : 0 < C_lock * (R / r0) ^ n := mul_pos hC hpow
  73  linarith
  74
  75theorem enhancement_strict_mono (R₁ R₂ r0 : ℝ) (hR₁ : 0 < R₁)
  76    (hR₂ : R₁ < R₂) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) :
  77    w_radial R₁ r0 n < w_radial R₂ r0 n := by
  78  unfold w_radial
  79  have hC : 0 < C_lock := C_lock_pos
  80  -- (R₁ / r0) ^ n < (R₂ / r0) ^ n
  81  have hd1 : 0 < R₁ / r0 := div_pos hR₁ hr0
  82  have hd_lt : R₁ / r0 < R₂ / r0 := by
  83    have hinv : 0 < r0⁻¹ := inv_pos.mpr hr0
  84    have : R₁ * r0⁻¹ < R₂ * r0⁻¹ := mul_lt_mul_of_pos_right hR₂ hinv
  85    simpa [div_eq_mul_inv] using this
  86  have hpow_lt : (R₁ / r0) ^ n < (R₂ / r0) ^ n :=
  87    pow_lt_pow_left₀ hd_lt (le_of_lt hd1) (Nat.pos_iff_ne_zero.mp hn)
  88  have hmul_lt : C_lock * (R₁ / r0) ^ n < C_lock * (R₂ / r0) ^ n := by
  89    exact mul_lt_mul_of_pos_left hpow_lt hC
  90  linarith
  91
  92/-- For any positive lower threshold `M`, there exists a radius `R*` at
  93    which the enhancement exceeds `M`. This formalises "asymptotic
  94    divergence" of `w` along the witness sequence. -/
  95theorem enhancement_unbounded (r0 : ℝ) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n)
  96    (M : ℝ) (hM : 0 < M) :
  97    ∃ R : ℝ, 0 < R ∧ M < w_radial R r0 n := by
  98  unfold w_radial
  99  -- choose R := r0 * (M / C_lock)^(1/n) + r0 ...
 100  -- Simpler: pick R so that (R/r0)^n > M / C_lock, then C_lock*(R/r0)^n > M, so w > 1+M > M.
 101  have hC : 0 < C_lock := C_lock_pos
 102  -- Choose target u = max(1, M/C_lock + 1) for (R/r0)^n.
 103  set u := M / C_lock + 1 with hu_def
 104  have hu_pos : 0 < u := by
 105    have : 0 < M / C_lock := div_pos hM hC
 106    have : 0 < M / C_lock + 1 := by linarith
 107    simpa [hu_def] using this
 108  -- Pick R = r0 * u (so (R/r0)^1 = u, then (R/r0)^n ≥ u for u ≥ 1, n ≥ 1).
 109  -- We need u ≥ 1 to make (·)^n monotone past 1.
 110  refine ⟨r0 * (u + 1), ?pos, ?bound⟩
 111  · have : 0 < u + 1 := by linarith
 112    exact mul_pos hr0 this
 113  · -- (R/r0) = u + 1 > 1
 114    have hratio : (r0 * (u + 1)) / r0 = u + 1 := by
 115      field_simp
 116    have hge : 1 ≤ u + 1 := by linarith
 117    -- (u+1)^n ≥ u + 1 for n ≥ 1
 118    have hn_ne : n ≠ 0 := Nat.pos_iff_ne_zero.mp hn
 119    have hpow_ge : u + 1 ≤ (u + 1) ^ n := by
 120      have h₁ : (u + 1) ^ 1 = u + 1 := by ring
 121      have h₂ : (u + 1) ^ 1 ≤ (u + 1) ^ n :=
 122        pow_le_pow_right₀ hge (Nat.one_le_iff_ne_zero.mpr hn_ne)
 123      simpa [h₁] using h₂
 124    have hd_pow : (u + 1) ≤ ((r0 * (u + 1)) / r0) ^ n := by
 125      simp [hratio]; exact hpow_ge
 126    have : M < C_lock * (u + 1) := by
 127      have hCu : C_lock * u = C_lock * (M / C_lock + 1) := by simp [hu_def]
 128      have hexp : C_lock * (M / C_lock + 1) = M + C_lock := by
 129        field_simp
 130      have : C_lock * u = M + C_lock := by simp [hCu, hexp]
 131      have hadd : M + C_lock < C_lock * (u + 1) := by
 132        have hexp2 : C_lock * (u + 1) = C_lock * u + C_lock := by ring
 133        rw [hexp2]
 134        linarith
 135      linarith
 136    have hCprod : C_lock * (u + 1) ≤ C_lock * ((r0 * (u + 1)) / r0) ^ n :=
 137      mul_le_mul_of_nonneg_left hd_pow (le_of_lt hC)
 138    linarith
 139
 140/-- The Newtonian baryonic velocity squared `V_bar²` for a point-mass
 141    enclosed `M_enc` and radius `R` is `G·M_enc/R`. The ILG-modified
 142    velocity squared is
 143
 144      V²(R) = w(R) · V_bar²(R) ≥ V_bar²(R)
 145
 146    so the ILG prediction is always ≥ Newtonian. -/
 147theorem ilg_velocity_sq_dominates_newtonian
 148    (V_bar_sq R r0 : ℝ)
 149    (hVb : 0 ≤ V_bar_sq) (hR : 0 < R) (hr0 : 0 < r0) (n : ℕ) (hn : 0 < n) :
 150    V_bar_sq ≤ w_radial R r0 n * V_bar_sq := by
 151  have hw : 1 < w_radial R r0 n := enhancement_above_one R r0 hR hr0 n hn
 152  have hwle : 1 ≤ w_radial R r0 n := le_of_lt hw
 153  have : V_bar_sq * 1 ≤ V_bar_sq * w_radial R r0 n :=
 154    mul_le_mul_of_nonneg_left hwle hVb
 155  linarith [mul_comm V_bar_sq (w_radial R r0 n)]
 156
 157/-! ## BTFR slope identity
 158
 159The Baryonic Tully-Fisher Relation (BTFR) is
 160
 161  M_bary ∝ V_flat^β
 162
 163We claim the locked prediction is `β = 4`. The structural reason is the
 164deep-ILG limit: for a point-mass `M`, with `a_bar = G M / R²` and the
 165locked exponent `α/2 = (1-1/φ)/4` in the acceleration term, we have
 166`a_obs ≈ (a_0 a_bar)^(1/2)` in the deep regime (matching MOND), giving
 167`V^4 = a_obs² · R² ≈ G M a_0`, so `M = V^4 / (G a_0)` and `β = 4`.
 168
 169We do not formalise the integration here; the numerical confirmation
 170sits in `MassToLightBTFRSlopeScoreCard.lean` with the SPARC artifact.
 171The structural identity is recorded as a Prop. -/
 172
 173def BTFRSlopeIdentity : Prop :=
 174  ∀ (M Vflat a0 G : ℝ), 0 < M → 0 < Vflat → 0 < a0 → 0 < G →
 175    (M = Vflat ^ 4 / (G * a0) ↔ M * (G * a0) = Vflat ^ 4)
 176
 177theorem btfr_slope_identity_iff : BTFRSlopeIdentity := by
 178  intros M V a0 G _hM _hV ha0 hG
 179  have hpos : 0 < G * a0 := mul_pos hG ha0
 180  have hne : (G * a0) ≠ 0 := ne_of_gt hpos
 181  constructor
 182  · intro h
 183    have : M * (G * a0) = (V ^ 4 / (G * a0)) * (G * a0) := by rw [h]
 184    rw [this, div_mul_cancel₀ _ hne]
 185  · intro h
 186    have : V ^ 4 = M * (G * a0) := h.symm
 187    rw [this, mul_div_assoc, div_self hne, mul_one]
 188
 189/-! ## Certificate -/
 190
 191structure ILGAsymptoticEnhancementCert where
 192  C_pos : 0 < C_lock
 193  enhancement_pos : ∀ R r0 (hR : 0 < R) (hr0 : 0 < r0) n,
 194    0 < w_radial R r0 n
 195  enhancement_above_one : ∀ R r0 (hR : 0 < R) (hr0 : 0 < r0) n (hn : 0 < n),
 196    1 < w_radial R r0 n
 197  enhancement_strict_mono : ∀ R₁ R₂ r0 (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) (hr0 : 0 < r0)
 198    n (hn : 0 < n), w_radial R₁ r0 n < w_radial R₂ r0 n
 199  enhancement_unbounded : ∀ r0 (hr0 : 0 < r0) n (hn : 0 < n) M (hM : 0 < M),
 200    ∃ R : ℝ, 0 < R ∧ M < w_radial R r0 n
 201  newtonian_dominated : ∀ V_bar_sq R r0 (hVb : 0 ≤ V_bar_sq) (hR : 0 < R)
 202    (hr0 : 0 < r0) n (hn : 0 < n),
 203    V_bar_sq ≤ w_radial R r0 n * V_bar_sq
 204  btfr_slope_iff : BTFRSlopeIdentity
 205
 206theorem ilgAsymptoticEnhancementCert_holds : Nonempty ILGAsymptoticEnhancementCert :=
 207  ⟨{ C_pos := C_lock_pos
 208     enhancement_pos := enhancement_pos
 209     enhancement_above_one := enhancement_above_one
 210     enhancement_strict_mono := enhancement_strict_mono
 211     enhancement_unbounded := enhancement_unbounded
 212     newtonian_dominated := ilg_velocity_sq_dominates_newtonian
 213     btfr_slope_iff := btfr_slope_identity_iff }⟩
 214
 215end
 216
 217end IndisputableMonolith.Gravity.ILGAsymptoticEnhancement
 218