`KernelParams`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.Kernel on GitHub at line 39.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  36/-! ## Kernel Parameters -/
  37
  38/-- ILG kernel parameter bundle with explicit RS-derived values. -/
  39structure KernelParams where
  40  /-- Exponent α = (1 - 1/φ) / 2 -/
  41  alpha : ℝ
  42  /-- Amplitude constant C -/
  43  C : ℝ
  44  /-- Reference time scale τ₀ -/
  45  tau0 : ℝ
  46  /-- Positivity of τ₀ -/
  47  tau0_pos : 0 < tau0
  48  /-- Nonnegativity of α -/
  49  alpha_nonneg : 0 ≤ alpha
  50  /-- Nonnegativity of C -/
  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,

papers checked against this theorem

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