bitKernelFamiliesCert
plain-language theorem explainer
The declaration constructs an explicit inhabitant of the BITKernelFamiliesCert structure that bundles normalization at zero redshift, strict bounds on the maximum BIT amplitude, and the effective equation of state at z=0 for the three kernel families. Cosmologists running DESI Y3 w(z) forecasts would cite this certificate to confirm the kernels remain bounded before Monte Carlo sampling. The construction is a direct structure literal that wires four sibling theorems into the certificate fields.
Claim. The BIT kernel families certificate asserts that for every kernel family $K$ and every $z_0$, $K(0,z_0)=1$, that the maximum amplitude satisfies $0 < δw_0^max < 1$, and that the effective equation of state at redshift zero obeys $w_eff(K,0,δw_0,z_0)=-1+δw_0$.
background
The module introduces three kernel families for the BIT cosmic-Z-aging amplitude $δw(z)=δw_0·K(z)$: the constant kernel $K(z)=1$, the canonical RS arc-11 kernel $K(z)=1/(1+z)$, and the exponential $K(z)=exp(-z/z_0)$. Each kernel is required to lie in $[0,1]$ for $z≥0$, with the amplitude $δw_0$ bounded above by $J(φ)$ from the BIT theorem. The master certificate BITKernelFamiliesCert packages four properties: normalization at zero redshift for any kernel, positivity and upper bound less than one on the maximum amplitude, and the value of the effective equation of state at $z=0$. This certificate is assembled from the supporting results kernel_at_zero (all three kernels equal 1 at $z=0$), delta_w0_max_pos, delta_w0_max_lt_one, and w_eff_at_zero (at $z=0$, $w_eff=-1+δw_0$ for any kernel).
proof idea
The definition is a one-line structure constructor that supplies the four fields of BITKernelFamiliesCert directly from the sibling theorems kernel_at_zero, delta_w0_max_pos, delta_w0_max_lt_one, and w_eff_at_zero.
why it matters
This definition supplies the inhabited master certificate required by any downstream analysis that invokes the BIT kernel families for w(z) forecasting. It closes the interface defined in the module documentation for the DESI Y3 forecast script. Within the Recognition framework it confirms that the kernel models respect the J-cost bounds and the phi-ladder amplitude limits from the BIT theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.