w_eff_at_zero
plain-language theorem explainer
The declaration establishes that the effective equation of state equals -1 plus the amplitude delta_w0 at redshift zero for every kernel family. Cosmologists running BIT-based w(z) forecasts for DESI Y3 data would cite the result to anchor present-epoch calibration. The proof is a direct algebraic reduction that substitutes the kernel value at zero into the w_eff definition and simplifies.
Claim. For any kernel family $k$, $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=1, the inverse (1+z) kernel, and the exponential kernel exp(-z/z_0). The effective equation of state is defined by w_eff(k,z,δw_0,z0):=-1+δw_0·kernel(k,z,z0). An upstream lemma states that every kernel evaluates to 1 at z=0.
proof idea
The proof unfolds the definition of w_eff, rewrites the kernel factor via the kernel_at_zero lemma, and closes with the ring tactic.
why it matters
The result populates one field of the BITKernelFamiliesCert structure that certifies the kernel families for DESI Y3 forecasting scripts. It confirms the z=0 limit recovers the base value -1+δw_0 required by the BIT amplitude bounds. In the Recognition Science setting it anchors the cosmology layer that rests on J-uniqueness and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.