constant_kernel_eq_one
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.