delta_w0_max_lt_one
plain-language theorem explainer
delta_w0_max_lt_one establishes that the maximum BIT amplitude is strictly less than one. Cosmology forecasts employing BIT kernels for the equation of state cite this result to enforce the amplitude bound. The proof reduces the claim to phi less than two by unfolding the definition and closes with linear arithmetic.
Claim. $δw_0^{max} < 1$, where $δw_0^{max} := ϕ - 3/2$.
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 kernel K(z) = exp(-z / z_0). Each kernel is bounded in [0, 1] for z ≥ 0, and the amplitude satisfies 0 ≤ δw_0 ≤ J(ϕ) with the explicit definition delta_w0_max := phi - 3/2 ≈ 0.118. The local setting is w(z) forecasting for DESI Y3 using these kernels under the BIT theorem amplitude limit.
proof idea
The proof is a term-mode wrapper. It unfolds delta_w0_max to obtain phi - 3/2, invokes the upstream lemma phi_lt_two to obtain phi < 2, and closes with linarith.
why it matters
The result supplies the delta_w0_max_lt_one field required by the BITKernelFamiliesCert structure, which also records kernel_at_zero_one, delta_w0_max_pos, and w_eff_at_zero. This certificate validates the kernel families for cosmology forecasts in the Recognition Science framework, consistent with the J-cost definition and the phi-forcing chain. It closes the strict upper bound needed for physical consistency with the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.