w_eff
plain-language theorem explainer
The definition supplies the effective equation of state w_eff(z) = -1 + δw_0 · K(z) for each BIT kernel family. Cosmologists running DESI Y3 w(z) forecasts cite it to implement the three kernel models under the BIT amplitude bound. It is realized as a direct one-line combination of the kernel match and the scaling parameter.
Claim. $w_{eff}(k, z, δw_0, z_0) := -1 + δw_0 · K(k, z, z_0)$, where $K$ is the kernel function for family $k$.
background
The module defines KernelFamily as an inductive type with constructors constant_kernel, inv_one_plus_z, and exponential. The kernel definition matches on the tag to return 1, 1/(1+z), or exp(-z/z0) respectively. Local setting is the BIT cosmic-Z-aging amplitude δw(z) = δw_0 · K(z) with δw_0 bounded in [0, J(φ)] from the BIT theorem, used for DESI Y3 forecasting. Upstream results include the kernel definition and the separate ILG kernel construction.
proof idea
The definition is a one-line wrapper that applies the kernel function to the family, redshift, and z0 arguments, then computes the linear combination with delta_w0.
why it matters
It feeds the BITKernelFamiliesCert structure and the w_eff_at_zero theorem that confirms w_eff(0) = -1 + δw_0. The module implements the BIT amplitude for cosmology forecasting, linking to the Recognition Science forcing chain via J-uniqueness and the phi fixed point. It touches the open question of matching the kernel families to full observational data sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.