exp_kernel_pos
plain-language theorem explainer
The declaration proves that the exponential member of the BIT kernel family is strictly positive for every real input pair. Analysts forecasting the dark-energy equation-of-state evolution w(z) with the three-kernel model cite this fact to guarantee non-negative amplitudes in the DESI Y3 pipeline. The argument is a direct term reduction: the kernel definition is expanded to the real exponential, whose positivity is a standard library fact.
Claim. For all real numbers $z$ and $z_0$, $0 < e^{-z/z_0}$.
background
The BITKernelFamilies module supplies three kernel shapes for the cosmic aging amplitude δw(z) = δw_0 · K(z), where δw_0 is bounded by the BIT maximum J(φ) ≈ 0.118. KernelFamily is an inductive tag distinguishing the constant, inverse-linear, and exponential forms. The kernel function itself is defined by case analysis on the tag, yielding 1, 1/(1+z), or exp(-z/z0) respectively. This positivity result for the exponential case is a prerequisite for keeping the forecasted δw(z) non-negative on z ≥ 0.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the kernel definition, which matches on the exponential tag to produce Real.exp(-z/z0), then applies the library fact that the real exponential is always positive.
why it matters
The result supports the boundedness claim for the exponential kernel on the non-negative redshift axis, feeding the w_eff and delta_w0_max lemmas in the same module. It directly implements the requirement that each kernel family remain in [0,1] for z ≥ 0, as stated in the module documentation for DESI Y3 forecasting. No open questions are attached; the fact is a routine positivity check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.