delta_w0_max_pos
plain-language theorem explainer
delta_w0_max is shown positive by unfolding its definition as phi minus 3/2 and invoking the bound phi greater than 1.5. Cosmologists building w(z) forecasts with BIT kernel families cite the result to confirm the amplitude interval begins above zero. The term proof applies linear arithmetic after the phi inequality lemma.
Claim. $0 < phi - 3/2$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The BITKernelFamilies module defines three kernels for the cosmic-Z-aging amplitude δw(z) = δw_0 · K(z): constant, 1/(1+z), and exponential, each bounded in [0,1] for z ≥ 0. The maximum amplitude is introduced as the definition delta_w0_max := phi - 3/2, identified with J(φ) from the BIT theorem and required to lie in [0, J(φ)]. The module imports Constants to access the phi definition and the lemma phi_gt_onePointFive.
proof idea
The term proof unfolds delta_w0_max to obtain phi - 3/2. It then applies the upstream lemma phi_gt_onePointFive, which establishes 1.5 < phi, and finishes with linarith to conclude the strict inequality.
why it matters
The theorem supplies the positivity field required by the BITKernelFamiliesCert structure and the bitKernelFamiliesCert definition that certifies the kernel families for DESI Y3 w(z) forecasting. It closes the lower end of the amplitude range [0, J(φ)] demanded by the BIT theorem in the Recognition Science cosmology setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.