IndisputableMonolith.Gravity.ParameterizationBridge

   1import Mathlib
   2
   3/-!
   4# Gravity: Parameterization Bridge (Acceleration ↔ Dynamical Time)
   5
   6This module formalizes the exact algebraic identities that relate:
   7- circular-orbit acceleration \(a = v^2/r\),
   8- orbital/dynamical time \(T_{\rm dyn} = 2\pi r/v\),
   9and the common "characteristic time" \(T_0 = 2\pi\sqrt{r_0/a_0}\).
  10
  11These identities are the precise bridge underlying the relationship between
  12"acceleration-parameterized" and "time-parameterized" weight forms.
  13
  14## Status
  15
  16All bridge identities and exponent-mapping theorems in this module are fully proven
  17(no `sorry`).
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Gravity
  22namespace ParameterizationBridge
  23
  24open Real
  25
  26noncomputable section
  27
  28/-- Circular-orbit centripetal acceleration from speed `v` and radius `r`. -/
  29def accel (v r : ℝ) : ℝ := v^2 / r
  30
  31/-- Orbital (dynamical) time for circular motion (one full revolution). -/
  32def Tdyn (v r : ℝ) : ℝ := 2 * Real.pi * r / v
  33
  34/-- Characteristic dynamical time constructed from a length scale `r0` and acceleration scale `a0`:
  35\[
  36T_0 = 2\pi\sqrt{r_0/a_0}.
  37\]
  38-/
  39def T0 (r0 a0 : ℝ) : ℝ := 2 * Real.pi * Real.sqrt (r0 / a0)
  40
  41/-- Core identity: \(a\,T_{\rm dyn}^2 = 4\pi^2 r\). -/
  42theorem accel_mul_Tdyn_sq (v r : ℝ) (hv : v ≠ 0) (hr : r ≠ 0) :
  43    accel v r * (Tdyn v r)^2 = 4 * (Real.pi ^ 2) * r := by
  44  unfold accel Tdyn
  45  field_simp [hv, hr]
  46  ring
  47
  48/-- Square of the characteristic time: \(T_0^2 = 4\pi^2 (r_0/a_0)\). -/
  49theorem T0_sq (r0 a0 : ℝ) (hr0 : 0 ≤ r0) (ha0 : 0 < a0) :
  50    (T0 r0 a0)^2 = 4 * (Real.pi ^ 2) * (r0 / a0) := by
  51  unfold T0
  52  have hnonneg : 0 ≤ r0 / a0 := div_nonneg hr0 (le_of_lt ha0)
  53  have hsq : Real.sqrt (r0 / a0) ^ 2 = r0 / a0 := Real.sq_sqrt hnonneg
  54  calc (2 * Real.pi * Real.sqrt (r0 / a0))^2
  55      = (2 * Real.pi)^2 * (Real.sqrt (r0 / a0))^2 := by ring
  56    _ = 4 * Real.pi^2 * (r0 / a0) := by rw [hsq]; ring
  57
  58/-- **Bridge identity (exact):**
  59\[
  60\left(\frac{T_{\rm dyn}}{T_0}\right)^2 = \left(\frac{a_0}{a}\right)\left(\frac{r}{r_0}\right)
  61\]
  62for circular motion with \(a=v^2/r\) and \(T_{\rm dyn}=2\pi r/v\).
  63
  64This is the fundamental kinematic identity underlying the acceleration↔time parameterization.
  65-/
  66theorem time_ratio_sq_eq_accel_ratio_mul_r_ratio
  67    (v r a0 r0 : ℝ) (hv : 0 < v) (hr : 0 < r) (ha0 : 0 < a0) (hr0 : 0 < r0) :
  68    let a := accel v r
  69    let T := Tdyn v r
  70    let Tref := T0 r0 a0
  71    (T / Tref)^2 = (a0 / a) * (r / r0) := by
  72  -- Direct algebraic verification
  73  intro a T Tref
  74  dsimp [a, T, Tref]
  75  have hv0 : v ≠ 0 := ne_of_gt hv
  76  have hr0' : r ≠ 0 := ne_of_gt hr
  77  have ha0_ne : a0 ≠ 0 := ne_of_gt ha0
  78  have hr0_ne : r0 ≠ 0 := ne_of_gt hr0
  79
  80  have ha : accel v r ≠ 0 := by
  81    unfold accel
  82    exact div_ne_zero (pow_ne_zero 2 hv0) hr0'
  83
  84  -- Expand the square of a ratio as a ratio of squares.
  85  rw [div_pow (Tdyn v r) (T0 r0 a0) 2]
  86
  87  -- Use the pre-proved square identities for `Tdyn` and `T0`.
  88  have hT_sq : (Tdyn v r)^2 = (4 * (Real.pi ^ 2) * r) / accel v r := by
  89    have h := accel_mul_Tdyn_sq (v := v) (r := r) hv0 hr0'
  90    apply (eq_div_iff ha).2
  91    -- Commute multiplication to match the target.
  92    simpa [mul_comm, mul_left_comm, mul_assoc] using h
  93
  94  have hT0_sq : (T0 r0 a0)^2 = 4 * (Real.pi ^ 2) * (r0 / a0) :=
  95    T0_sq r0 a0 (le_of_lt hr0) ha0
  96
  97  rw [hT_sq, hT0_sq]
  98  -- Clear denominators and finish by ring normalization.
  99  field_simp [ha, ha0_ne, hr0_ne]
 100
 101/-- Rearranged bridge:
 102\[
 103\frac{a_0}{a} = \left(\frac{T_{\rm dyn}}{T_0}\right)^2\left(\frac{r_0}{r}\right).
 104\]
 105-/
 106theorem accel_ratio_eq_time_ratio_sq_mul_r0_over_r
 107    (v r a0 r0 : ℝ) (hv : 0 < v) (hr : 0 < r) (ha0 : 0 < a0) (hr0 : 0 < r0) :
 108    let a := accel v r
 109    let T := Tdyn v r
 110    let Tref := T0 r0 a0
 111    (a0 / a) = (T / Tref)^2 * (r0 / r) := by
 112  -- Algebraic rearrangement of time_ratio_sq_eq_accel_ratio_mul_r_ratio
 113  intro a T Tref
 114  have hbridge :
 115      (T / Tref)^2 = (a0 / a) * (r / r0) := by
 116    simpa [a, T, Tref] using
 117      time_ratio_sq_eq_accel_ratio_mul_r_ratio (v := v) (r := r) (a0 := a0) (r0 := r0) hv hr ha0 hr0
 118
 119  have hr_ne : r ≠ 0 := ne_of_gt hr
 120  have hr0_ne : r0 ≠ 0 := ne_of_gt hr0
 121
 122  have hcancel : (r / r0) * (r0 / r) = (1 : ℝ) := by
 123    field_simp [hr_ne, hr0_ne]
 124
 125  -- Multiply both sides of the bridge by `r0/r` and simplify.
 126  have hmul := congrArg (fun x => x * (r0 / r)) hbridge
 127  have : (T / Tref)^2 * (r0 / r) = a0 / a := by
 128    -- Reassociate and cancel `(r/r0) * (r0/r) = 1`.
 129    simpa [mul_assoc, hcancel] using hmul
 130
 131  exact this.symm
 132
 133/-- **Exponent bridge (canonical special case):** at the characteristic radius \(r=r_0\),
 134\[
 135\left(\frac{a_0}{a}\right)^\alpha = \left(\frac{T_{\rm dyn}}{T_0}\right)^{2\alpha}.
 136\]
 137
 138This is the exact statement behind the common "acceleration exponent vs time exponent" mapping:
 139if a model is written with \((a_0/a)^{\alpha_{\rm acc}}\), the corresponding exponent on
 140the time-ratio base is \(2\alpha_{\rm acc}\) (at \(r=r_0\)).
 141-/
 142theorem accel_power_eq_time_power_at_r_eq_r0
 143    (v r0 a0 α : ℝ) (hv : 0 < v) (hr0 : 0 < r0) (ha0 : 0 < a0) :
 144    let a := accel v r0
 145    let T := Tdyn v r0
 146    let Tref := T0 r0 a0
 147    (a0 / a) ^ α = (T / Tref) ^ ((2 : ℝ) * α) := by
 148  intro a T Tref
 149  -- At r = r0, from the bridge: (T/Tref)^2 = a0/a
 150  -- Thus (a0/a)^α = ((T/Tref)^2)^α = (T/Tref)^(2α)
 151  have h : (T / Tref)^2 = a0 / a := by
 152    have hbridge := time_ratio_sq_eq_accel_ratio_mul_r_ratio v r0 a0 r0 hv hr0 ha0 hr0
 153    have hr00 : r0 ≠ 0 := ne_of_gt hr0
 154    simp only [div_self hr00, mul_one] at hbridge
 155    exact hbridge
 156  rw [← h]
 157  have hT_pos : 0 < T := by
 158    unfold T Tdyn
 159    have h2pi : 0 < (2 : ℝ) * Real.pi := by nlinarith [Real.pi_pos]
 160    exact div_pos (mul_pos h2pi hr0) hv
 161  have hTref_pos : 0 < Tref := by
 162    unfold Tref T0
 163    have hpos : 0 < r0 / a0 := div_pos hr0 ha0
 164    have hsqrt : 0 < Real.sqrt (r0 / a0) := Real.sqrt_pos.mpr hpos
 165    have h2pi : 0 < (2 : ℝ) * Real.pi := by nlinarith [Real.pi_pos]
 166    exact mul_pos h2pi hsqrt
 167  have hratio_pos : 0 < T / Tref := div_pos hT_pos hTref_pos
 168  have hratio_nonneg : 0 ≤ T / Tref := le_of_lt hratio_pos
 169  -- ((T/Tref)^2)^α = (T/Tref)^(2*α)
 170  rw [← Real.rpow_natCast (T / Tref) 2]
 171  rw [← Real.rpow_mul hratio_nonneg]
 172  norm_cast
 173
 174/-- **Exponent bridge (time→acceleration form):** at the characteristic radius \(r=r_0\),
 175\[
 176\left(\frac{T_{\rm dyn}}{T_0}\right)^{\alpha}
 177= \left(\frac{a_0}{a}\right)^{\alpha/2}.
 178\]
 179
 180This is the exact mapping when the exponent \(\alpha\) is interpreted as the
 181**time-exponent** (as in a time-kernel), and one rewrites the model in acceleration space.
 182-/
 183theorem time_power_eq_accel_power_at_r_eq_r0
 184    (v r0 a0 α : ℝ) (hv : 0 < v) (hr0 : 0 < r0) (ha0 : 0 < a0) :
 185    let a := accel v r0
 186    let T := Tdyn v r0
 187    let Tref := T0 r0 a0
 188    (T / Tref) ^ α = (a0 / a) ^ (α / 2) := by
 189  intro a T Tref
 190  -- Use the already-proved form with exponent α/2
 191  have h := accel_power_eq_time_power_at_r_eq_r0 v r0 a0 (α / 2) hv hr0 ha0
 192  -- h: (a0/a)^(α/2) = (T/Tref)^(2*(α/2)) = (T/Tref)^α
 193  have : 2 * (α / 2) = α := by ring
 194  simp only [this] at h
 195  exact h.symm
 196
 197end
 198end ParameterizationBridge
 199end Gravity
 200end IndisputableMonolith
 201