kernel_at_zero
plain-language theorem explainer
All three BIT kernel families evaluate to one at redshift zero. Forecasters using the BIT cosmic-Z-aging amplitude for DESI Y3 w(z) predictions cite this normalization property. The proof is a one-line case split on the kernel inductive type followed by simplification against the kernel definition.
Claim. For any kernel family $k$ and real $z_0$, the BIT kernel function satisfies $K(k,0,z_0)=1$.
background
The module defines three kernel families for the BIT cosmic-Z-aging amplitude: constant kernel $K(z)=1$, inverse kernel $K(z)=1/(1+z)$, and exponential kernel $K(z)=e^{-z/z_0}$. Each is bounded in $[0,1]$ for $z>=0$, with maximum amplitude drawn from the BIT theorem. The kernel function is defined by pattern-matching on the KernelFamily inductive type (constant_kernel, inv_one_plus_z, exponential) and returns the corresponding expression, defaulting $z_0=1$.
proof idea
The proof performs case analysis on the KernelFamily inductive type and simplifies using the kernel definition, which returns 1 for the constant case and evaluates to 1 at argument zero for the remaining two cases.
why it matters
This result populates the BITKernelFamiliesCert structure, the master certificate for the kernel families. It is invoked directly in the proof of w_eff_at_zero to obtain $w_eff(k,0,delta_w0,z0)=-1+delta_w0$. The normalization anchors the BIT amplitude bound $delta_w0 in [0,J(phi)]$ inside the cosmology forecasting pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.