kernel
plain-language theorem explainer
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).
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.