def definition def or abbrev

`kernel_background`

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

formal statement (Lean)

 254@[simp] noncomputable def kernel_background : ℝ := 1

Definition body.

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

alpha_from_self_similarity in IndisputableMonolith.ILG.Kernel decl_use
CausalityBoundsCert in IndisputableMonolith.ILG.Kernel decl_use
kernel_background_eq_one in IndisputableMonolith.ILG.Kernel decl_use
kernel_background_independent_of_params in IndisputableMonolith.ILG.Kernel decl_use
mode_partition in IndisputableMonolith.ILG.Kernel decl_use
mode_partition_eq in IndisputableMonolith.ILG.Kernel decl_use