BITKernelFamiliesCert
plain-language theorem explainer
BITKernelFamiliesCert packages the normalization at zero, positivity and upper bound on the amplitude, and zero-redshift evaluation of the effective equation of state for the three BIT kernel families into one structure. Cosmologists running DESI Y3 w(z) forecasts would cite the certificate to confirm that kernels equal 1 at z=0, that delta_w0_max lies in (0,1), and that w_eff(0) equals -1 plus delta_w0. The definition assembles these facts directly from the kernel case definition, the phi-derived bounds, and the w_eff formula without further t
Claim. The BIT kernel families certificate asserts that for every kernel family $K$ and every $z_0$, the kernel function satisfies $K(0,z_0)=1$, that the maximum amplitude obeys $0<δw_{0, max}<1$, and that the effective equation of state satisfies $w_{eff}(K,0,δw_0,z_0)=-1+δw_0$.
background
The module introduces three kernel families for the BIT amplitude $δw(z)=δw_0·K(z)$: the constant kernel $K=1$, the inverse kernel $K=1/(1+z)$, and the exponential kernel $K=exp(-z/z_0)$. The amplitude bound is defined as $δw_{0,max}=φ-3/2$, where $φ$ is the golden ratio fixed by the Recognition Science forcing chain. The effective equation of state is given by the definition $w_{eff}(k,z,δw_0,z_0)=-1+δw_0·kernel(k,z,z_0)$. Upstream lemmas establish positivity of $δw_{0,max}$ from $φ>1.5$ and the strict inequality $δw_{0,max}<1$ from $φ<2$.
proof idea
The structure is a direct bundling of four facts already proved in the module. Kernel normalization at zero follows by case analysis on the KernelFamily inductive type. The two inequalities on $δw_{0,max}$ are obtained by unfolding its definition and applying the phi bounds via linarith. The zero-redshift identity for $w_{eff}$ is immediate from the definition of $w_{eff}$ itself.
why it matters
The certificate is instantiated by bitKernelFamiliesCert to supply a single inhabited object for the kernel properties. It supports the BIT theorem application in cosmology by guaranteeing that amplitude deviations from $w=-1$ remain bounded and that kernels normalize at $z=0$. The construction closes the module scaffolding for DESI Y3 forecasts while relying on the phi value from the Recognition Science T5-T6 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.