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

kernel

show as:
view Lean formalization →

The ILG kernel supplies the weighting function w(k,a) = 1 + C (max(0.01, a/(k τ₀)))^α for wavenumber k and scale factor a in infra-luminous gravity models. Researchers constructing Duhamel integrals for 2D fluid continuum limits or universal equilibrium response certificates cite this definition when assembling integral operators. It is realized by a direct arithmetic expression that inserts a numerical safeguard to avoid zero denominators.

claim$w(k,a) = 1 + C (max(0.01, a/(k τ₀)))^α$, where $C$, $α$, and $τ₀$ are the amplitude, exponent, and reference time supplied by the KernelParams structure.

background

The module formalizes the Infra-Luminous Gravity kernel w(k,a) = 1 + C (a/(k τ₀))^α, with exponent α = (1 - 1/φ)/2 taken from self-similarity. KernelParams is the structure that packages alpha, C, and tau0 together with the positivity hypothesis 0 < tau0. Upstream, tau0 is the fundamental tick duration imported from Constants.tau0 and from the BIT kernel families, which supply analogous constant, inverse-linear, and exponential kernels for comparison.

proof idea

This is a one-line wrapper that directly evaluates the arithmetic expression 1 + P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha using the three fields of the KernelParams structure.

why it matters in Recognition Science

The definition is invoked inside universalResponseCert to furnish the kernel component of the UniversalResponseCert structure and inside DuhamelKernelDominatedConvergenceAt and duhamelKernelIntegral for the 2D continuum limit. It supplies the concrete weighting required by the CPM coercivity constants and the ILG exponent derived from the Recognition Science self-similar fixed point.

scope and limits

formal statement (Lean)

  79noncomputable def kernel (P : KernelParams) (k a : ℝ) : ℝ :=

proof body

Definition body.

  80  1 + P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha
  81
  82/-- Simplified kernel when k = 1 (reference wavenumber). -/

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.