kernel_perturbation

formal source

 242the wavenumber saturates at `k_min`, capping the enhancement at
 243`kernel(k_min)`. The IR cutoff `k_min` is physically the inverse recognition
 244horizon `a H / c`. -/
 245noncomputable def kernel_perturbation (P : KernelParams) (k_min k a : ℝ) : ℝ :=
 246  1 + P.C * (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
 247
 248/-- The ILG background kernel: identically `1`.
 249
 250The homogeneous Friedmann–Robertson–Walker background sits at the J-cost
 251minimum `J(1) = 0` with zero ledger gradient flow. The recognition operator
 252is at equilibrium on a homogeneous state, so there is no lag and no
 253enhancement. The background Poisson equation is unmodified standard GR. -/
 254@[simp] noncomputable def kernel_background : ℝ := 1
 255
 256@[simp] theorem kernel_background_eq_one : kernel_background = 1 := rfl
 257
 258/-- The Hubble-saturated kernel: an IR cutoff specialization with
 259    `k_min = a · H` (in units where `c = 1`). -/
 260noncomputable def kernel_with_Hubble (P : KernelParams) (a H k : ℝ) : ℝ :=
 261  kernel_perturbation P (a * H) k a
 262
 263/-- The perturbation kernel reduces to the original `kernel` when the
 264    wavenumber is at or above the IR cutoff. -/
 265theorem kernel_perturbation_eq_kernel_of_ge
 266    (P : KernelParams) {k_min k : ℝ} (a : ℝ) (h : k_min ≤ k) :
 267    kernel_perturbation P k_min k a = kernel P k a := by
 268  unfold kernel_perturbation kernel
 269  have hmax : max k_min k = k := max_eq_right h
 270  rw [hmax]
 271
 272/-- The perturbation kernel collapses to the IR-saturated value when
 273    `k ≤ k_min`. -/
 274theorem kernel_perturbation_at_IR_floor
 275    (P : KernelParams) {k_min k : ℝ} (a : ℝ) (h : k ≤ k_min) :