constant_kernel_eq_one
The constant kernel in the BIT family returns exactly one for any real redshift z and reference scale z0. Modelers of dark-energy evolution via the BIT amplitude δw(z) = δw0 · K(z) invoke this identity when choosing the flat option for DESI Y3 forecasts. The equality follows at once by substitution into the kernel definition.
claimFor the constant kernel family the function satisfies $K(z, z_0) = 1$ for all real $z, z_0$.
background
The module defines three kernel families for the BIT cosmic-Z-aging amplitude δw(z) = δw0 · K(z), with the constant option K(z) = 1, the canonical 1/(1+z) option, and the exponential option. The kernel function is defined by case analysis on the KernelFamily inductive type, returning the literal value 1 on the constant case. The module states that each kernel lies in [0,1] for z ≥ 0 and that the amplitude bound δw0 ∈ [0, J(φ)] comes from the BIT theorem.
proof idea
The proof is a one-line term that applies reflexivity directly to the kernel definition on the constant_kernel constructor.
why it matters in Recognition Science
This identity supplies the base case for the constant option inside the BIT kernel families used by the DESI Y3 forecast script. It anchors the flat-kernel choice in the module that implements the three families for w(z) modeling. The construction sits downstream of the BIT amplitude bound and upstream of any concrete forecast calculation.
scope and limits
- Does not prove positivity or bounds for the inverse or exponential kernels.
- Does not derive the kernel form from the Recognition forcing chain.
- Does not constrain the numerical range of δw0.
- Does not address observational calibration of the constant option.
formal statement (Lean)
58theorem constant_kernel_eq_one (z z0 : ℝ) :
59 kernel KernelFamily.constant_kernel z z0 = 1 := rfl
proof body
Term-mode proof.
60
61/-- The 1/(1+z) kernel is positive for `z > -1`. -/