mode_partition_eq

formal source

 367noncomputable def mode_partition (P : KernelParams) (k_min k a ρ_bar δρ : ℝ) : ℝ :=
 368  ρ_bar * kernel_background + δρ * kernel_perturbation P k_min k a
 369
 370theorem mode_partition_eq (P : KernelParams) (k_min k a ρ_bar δρ : ℝ) :
 371    mode_partition P k_min k a ρ_bar δρ
 372      = ρ_bar + δρ * kernel_perturbation P k_min k a := by
 373  unfold mode_partition kernel_background; ring
 374
 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