`rsKernelParams`

definition

show as: view math explainer →

module: IndisputableMonolith.ILG.Kernel
domain: ILG
line: 54 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ILG.Kernel on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  51  C_nonneg : 0 ≤ C
  52
  53/-- RS-canonical kernel parameters derived from golden ratio. -/
  54noncomputable def rsKernelParams (tau0 : ℝ) (h : 0 < tau0) : KernelParams := {
  55  alpha := alphaLock,
  56  C := phi ^ (-(3 : ℝ) / 2),
  57  tau0 := tau0,
  58  tau0_pos := h,
  59  alpha_nonneg := le_of_lt alphaLock_pos,
  60  C_nonneg := le_of_lt (Real.rpow_pos_of_pos phi_pos _)
  61}
  62
  63/-- Eight-tick aligned kernel parameters with c = 49/162. -/
  64noncomputable def eightTickKernelParams (tau0 : ℝ) (h : 0 < tau0) : KernelParams := {
  65  alpha := alphaLock,
  66  C := 49 / 162,
  67  tau0 := tau0,
  68  tau0_pos := h,
  69  alpha_nonneg := le_of_lt alphaLock_pos,
  70  C_nonneg := by norm_num
  71}
  72
  73/-! ## Kernel Definition -/
  74
  75/-- The ILG kernel function:
  76  w(k, a) = 1 + C · (a / (k τ₀))^α
  77
  78We use max with a small ε to avoid division issues when k τ₀ = 0. -/
  79noncomputable def kernel (P : KernelParams) (k a : ℝ) : ℝ :=
  80  1 + P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha
  81
  82/-- Simplified kernel when k = 1 (reference wavenumber). -/
  83noncomputable def kernelAtRefK (P : KernelParams) (a : ℝ) : ℝ :=
  84  1 + P.C * (max 0.01 (a / P.tau0)) ^ P.alpha

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.