w_eff
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 in Recognition Science
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.
scope and limits
- Does not enforce the bound δw_0 ≤ J(φ).
- Does not derive the kernel forms from the Recognition Composition Law.
- Does not include redshift-dependent corrections beyond the three families.
- Does not connect to spatial dimension D=3 or the eight-tick octave.
formal statement (Lean)
87def w_eff (k : KernelFamily) (z delta_w0 : ℝ) (z0 : ℝ := 1) : ℝ :=
proof body
Definition body.
88 -1 + delta_w0 * kernel k z z0
89
90/-- At `z = 0`, `w_eff = -1 + δw_0` for any kernel. -/