def definition def or abbrev

`C_kernel`

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

formal statement (Lean)

  85def C_kernel : ℝ := phi ^ (-(2 : ℝ))

Definition body.

  86
  87/-- The kernel exponent (for cross-reference; same as `alphaLock`). -/

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

C_competing_gt_C_kernel in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_competing_violates_budget in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_is_complement_of_Jphi in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_kernel_band in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_kernel_eq_two_minus_phi in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_kernel_lt_half in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
C_kernel_pos in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
half_rung_budget in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
half_rung_budget_doubled in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
half_rung_components_band in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
ILGSpatialKernelCert in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
ilg_spatial_kernel_one_statement in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use
three_channel_factorization in IndisputableMonolith.Gravity.ILGSpatialKernel decl_use

Lean names referenced from this declaration's body.

alphaLock in IndisputableMonolith.Constants decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use