KernelFamily
plain-language theorem explainer
The KernelFamily inductive enumerates three models for the redshift-dependent BIT kernel K(z) in cosmic aging forecasts. Cosmologists running DESI Y3 w(z) predictions cite the constant, inverse-linear, and exponential families to bound the amplitude δw0. The declaration is a bare inductive type with three constructors that derives decidable equality and inhabited.
Claim. An inductive type whose constructors label the constant kernel $K(z)=1$, the inverse-linear kernel $K(z)=1/(1+z)$, and the exponential kernel $K(z)=e^{-z/z_0}$.
background
The module introduces three kernel families for the BIT cosmic-Z-aging amplitude δw(z) = δw0 · K(z). The constant kernel is identically 1, the inverse-linear kernel is the canonical RS arc-11 form 1/(1+z), and the exponential kernel is exp(-z/z0). Each family is required to stay in [0,1] for z ≥ 0, with the amplitude δw0 taken from the BIT theorem bound J(φ).
proof idea
The declaration is an inductive definition that introduces the three constructors constant_kernel, inv_one_plus_z, and exponential, then derives DecidableEq and Inhabited.
why it matters
This definition supplies the enumeration required by the BITKernelFamiliesCert master certificate, which asserts kernel_at_zero_one together with the positivity and upper-bound statements on delta_w0_max. It supplies the concrete realizations needed for the BIT theorem in the cosmology section and is referenced by the DESI Y3 forecast script.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.