mode_partition_homogeneous

formal source

 375/-- **Background mode of the partition is unmodified.** When `δρ = 0`,
 376the effective source equals the background source — no ILG enhancement
 377on the homogeneous mode. -/
 378theorem mode_partition_homogeneous (P : KernelParams) (k_min k a ρ_bar : ℝ) :
 379    mode_partition P k_min k a ρ_bar 0 = ρ_bar := by
 380  rw [mode_partition_eq]; ring
 381
 382/-! ### Dynamical-time form (no cumulative-time integration)
 383
 384The companion form for galactic systems is parameterized by the dynamical
 385time `T_dyn` of the orbit, never by cumulative cosmic time `t`. This
 386eliminates the literal Riemann–Liouville integral and resolves
 387Beltracchi's concern (1).
 388-/
 389
 390/-- The dynamical-time ILG kernel: depends only on the local orbital
 391period `T_dyn`, the recognition tick `τ₀`, the lag amplitude `C`, and the
 392self-similarity exponent `α`. For a stationary orbit `T_dyn` is constant,
 393so the enhancement is constant, and the acceleration on an isolated mass
 394does not grow in time. -/
 395noncomputable def kernel_dynamical_time (P : KernelParams) (T_dyn : ℝ) : ℝ :=
 396  1 + P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha
 397
 398/-- The dynamical-time kernel is positive. -/
 399theorem kernel_dynamical_time_pos (P : KernelParams) (T_dyn : ℝ) :
 400    0 < kernel_dynamical_time P T_dyn := by
 401  unfold kernel_dynamical_time
 402  have hmax_pos : 0 < max 0.01 (T_dyn / P.tau0) := by
 403    apply lt_max_of_lt_left; norm_num
 404  have hpow_nonneg : 0 ≤ (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
 405    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
 406  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (T_dyn / P.tau0)) ^ P.alpha :=
 407    mul_nonneg P.C_nonneg hpow_nonneg
 408  linarith