IndisputableMonolith.Gravity.RunningGDerivation

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4import IndisputableMonolith.Gravity.RunningG
   5
   6namespace IndisputableMonolith.Gravity.RunningG
   7
   8open Constants
   9
  10/-- **CONSTANT: Voxel Density Scaling**
  11    The effective number of recognition voxels $N(r)$ as a function of radius. -/
  12def voxel_density_scaling (r : ℝ) : ℝ := r ^ beta_running
  13
  14/-- **THEOREM: Beta Running Derivation**
  15    The gravitational running exponent $\beta$ is uniquely determined by the
  16    ratio of the recognition lag $C_{lag} = \varphi^{-5}$ to the self-similarity
  17    scaling factor.
  18
  19    Derivation from Voxel Density:
  20    1. Let $\rho_{vox}(r)$ be the effective voxel density.
  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
  55      apply DifferentiableAt.rpow_const
  56      · apply DifferentiableAt.div_const
  57        exact differentiableAt_id
  58      · exact Or.inl (ne_of_gt (div_pos hr href))
  59  · -- differentiability of const 1
  60    exact differentiableAt_const 1
  61  · -- differentiability of the second term
  62    apply DifferentiableAt.const_mul
  63    apply DifferentiableAt.rpow_const
  64    · apply DifferentiableAt.div_const
  65      exact differentiableAt_id
  66    · exact Or.inl (ne_of_gt (div_pos hr href))
  67
  68end RunningG
  69end IndisputableMonolith.Gravity
  70