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

lambda_8

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)

  66noncomputable def lambda_8 : ℝ := 8

proof body

Definition body.

  67
  68/-- The recognition strain Q at a given scale k.
  69
  70    Q(k) = J(k/k_8) where k_8 = 2π/λ_8 is the 8-tick wavenumber.
  71
  72    For k ≪ k_8: Q ≈ 0 (large scales, no suppression)
  73    For k ≫ k_8: Q ≈ J_max (small scales, maximum suppression) -/

depends on (7)

Lean names referenced from this declaration's body.