exp_kernel_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish positivity for the constant or inverse-linear kernels.
- Does not prove that the kernel is bounded above by 1.
- Does not constrain the choice of z0.
- Does not connect to the underlying J(φ) amplitude bound.
formal statement (Lean)
68theorem exp_kernel_pos (z z0 : ℝ) :
69 0 < kernel KernelFamily.exponential z z0 := by
proof body
Term-mode proof.
70 unfold kernel
71 exact Real.exp_pos _
72
73/-- The maximum BIT amplitude is `J(φ) = φ - 3/2 ≈ 0.118`. -/