theorem proved term proof

`kernel_unity_at_saturation`

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

formal statement (Lean)

 155theorem kernel_unity_at_saturation {R : ℝ} (hR : 0 < R) :
 156    bandwidthKernel R R = 1 := by

Term-mode proof.

 157  unfold bandwidthKernel
 158  exact div_self (ne_of_gt hR)
 159
 160/-- The bandwidth kernel exceeds 1 when demand > bandwidth (ILG regime). -/

Lean names referenced from this declaration's body.

kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
bandwidthKernel in IndisputableMonolith.Unification.BandwidthSaturation decl_use
bandwidth in IndisputableMonolith.Unification.RecognitionBandwidth decl_use