name
The definition maps each of the three BIT kernel families to a descriptive string label for use in cosmic expansion forecasts. Researchers analyzing DESI Y3 data for w(z) evolution cite these labels when selecting between constant, inverse, and exponential kernels. The implementation consists of a direct pattern match on the KernelFamily inductive constructors.
claimThe function that sends each kernel family tag to its string descriptor: the constant kernel to ``K1 (constant)'', the inverse one-plus-redshift kernel to ``K2 (1/(1+z))'', and the exponential kernel to ``K3 (exp(-z/z0))''.
background
The BIT kernel families module defines three models for the amplitude factor K(z) in the cosmic-Z-aging correction δw(z) = δw_0 · K(z). These are the constant kernel K(z) = 1, the canonical RS arc-11 kernel K(z) = 1/(1+z), and the exponential K(z) = exp(-z/z0). The module documentation states that each kernel is bounded in [0,1] for z ≥ 0, with maximum amplitude δw_0 drawn from the BIT theorem.
proof idea
The definition is realized by pattern matching on the three constructors of the KernelFamily inductive type and returning the corresponding string literal in each case.
why it matters in Recognition Science
This naming definition supports the BIT kernel families framework for modeling the dark energy equation of state evolution w(z). It feeds into the forecasting pipeline referenced in the module documentation for DESI Y3 analysis. The labels align with the three kernel forms introduced in the BIT theorem application to cosmology, where the inverse kernel corresponds to the RS arc-11 form.
scope and limits
- Does not evaluate the kernel function at any redshift.
- Does not incorporate the amplitude δw_0 or the BIT theorem bounds.
- Does not interact with the ILG kernel or scalar field definitions.
- Does not provide numerical values or bounds checks.
formal statement (Lean)
38def name : KernelFamily → String
39 | constant_kernel => "K1 (constant)"
40 | inv_one_plus_z => "K2 (1/(1+z))"
41 | exponential => "K3 (exp(-z/z0))"
42
43end KernelFamily
44
45/-- The BIT kernel function. -/