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

kernel

show as:
view Lean formalization →

The BIT kernel function selects one of three models for the redshift dependence of the cosmic-Z-aging amplitude δw(z). Forecasters of dark-energy equation-of-state evolution cite it when running DESI Y3 w(z) forecasts. The definition is a direct case split on the KernelFamily inductive tag, returning the constant 1, the factor 1/(1+z), or the exponential decay exp(−z/z0).

claimFor a kernel family tag $k$ the function $K(z)$ is defined by case analysis: $K(z)=1$ when $k$ is the constant family, $K(z)=1/(1+z)$ when $k$ is the inverse-linear family, and $K(z)=e^{-z/z_0}$ when $k$ is the exponential family (with optional scale $z_0$ defaulting to 1).

background

The module defines three explicit kernel families for the BIT cosmic-Z-aging amplitude written δw(z)=δw₀·K(z). KernelFamily is the inductive type whose constructors are constant_kernel, inv_one_plus_z and exponential; each constructor tags one of the three functional forms listed in the module documentation. All kernels are required to map z≥0 into [0,1], with the prefactor δw₀ itself bounded by J(φ) from the BIT theorem.

proof idea

The definition is a one-line wrapper that performs exhaustive pattern matching on the KernelFamily inductive value. The constant_kernel case returns the literal 1, the inv_one_plus_z case returns the reciprocal 1/(1+z), and the exponential case returns Real.exp(−z/z0).

why it matters in Recognition Science

This definition supplies the concrete kernels used in forty downstream declarations, including universalResponseCert in Applied.UniversalEquilibriumResponseC7 and the Duhamel-kernel convergence structures in ClassicalBridge.Fluids.ContinuumLimit2D. It realizes the three models enumerated in the module documentation for the BIT amplitude, thereby closing the interface between the abstract KernelFamily tag and the numerical forecasting scripts.

scope and limits

formal statement (Lean)

  46def kernel (k : KernelFamily) (z : ℝ) (z0 : ℝ := 1) : ℝ :=

proof body

Definition body.

  47  match k with
  48  | KernelFamily.constant_kernel  => 1
  49  | KernelFamily.inv_one_plus_z   => 1 / (1 + z)
  50  | KernelFamily.exponential      => Real.exp (- z / z0)
  51
  52/-- All three kernels equal 1 at `z = 0`. -/

used by (40)

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

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.