pith. machine review for the scientific record. sign in
def definition def or abbrev

kernel_perturbation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 245noncomputable def kernel_perturbation (P : KernelParams) (k_min k a : ℝ) : ℝ :=

proof body

Definition body.

 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. -/

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.