beta_running_derived

formal source

  21    2. At nm scales, $\rho_{vox}(r) \propto r^\beta$ where $\beta$ is the
  22       strain induced by the $\varphi^{-5}$ lag.
  23    3. The effective G is proportional to the local resolution $\rho_{vox}$. -/
  24theorem beta_running_derived :
  25    beta_running = -(phi - 1) / (phi ^ 5) := by
  26  unfold beta_running
  27  rfl
  28
  29/-- **THEOREM: Nanoscale Strengthening Scaling**
  30    The effective gravitational constant $G_{eff}$ strengthens as $r \to 0$
  31    with the forced exponent $\beta$. -/
  32theorem running_g_scaling (r r_ref : ℝ) (hr : r > 0) (href : r_ref > 0) :
  33    deriv (fun x => G_ratio x r_ref) r =
  34    (abs beta_running * beta_running / r_ref) * (r / r_ref) ^ (beta_running - 1) := by
  35  unfold G_ratio
  36  rw [deriv_add]
  37  · rw [deriv_const, zero_add]
  38    rw [deriv_mul_const]
  39    · -- deriv (fun x => (x / r_ref) ^ beta_running) r
  40      -- = beta_running * (r / r_ref) ^ (beta_running - 1) * (1 / r_ref)
  41      have h_deriv : deriv (fun x => (x / r_ref) ^ beta_running) r =
  42          beta_running * (r / r_ref) ^ (beta_running - 1) * (1 / r_ref) := by
  43        -- Use chain rule: (f ∘ g)' = f'(g(x)) * g'(x)
  44        -- f(u) = u ^ beta_running, g(x) = x / r_ref
  45        rw [deriv_rpow_const]
  46        · -- u ^ (beta_running - 1) * deriv (fun x => x / r_ref) r
  47          rw [deriv_div_const]
  48          · rw [deriv_id'']
  49            ring
  50        · -- g(x) = r / r_ref > 0
  51          exact div_pos hr href
  52      rw [h_deriv]
  53      ring
  54    · -- differentiability of (fun x => (x / r_ref) ^ beta_running) at r