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

tests

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)

  85noncomputable def tests (P : KernelParams) (s : ILGState) : ℝ :=

proof body

Definition body.

  86  defectMass P s
  87
  88/-! ## CPM Constants for ILG -/
  89
  90/-- ILG-specific CPM constants derived from eight-tick geometry.
  91    - K_net = (9/7)² from ε = 1/8 covering
  92    - C_proj = 2 from J''(1) = 1 normalization
  93    - C_eng = 1 standard energy normalization
  94    - C_disp = 1 dispersion bound -/

used by (40)

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

… and 10 more

depends on (11)

Lean names referenced from this declaration's body.