delta_w0_max_pos
The theorem shows that the maximum BIT amplitude δw_0 is strictly positive. Cosmologists building w(z) forecasts with BIT kernel families for surveys such as DESI Y3 would cite it to confirm the allowed amplitude interval begins above zero. The proof is a one-line wrapper that unfolds the definition δw_0,max = φ - 3/2, invokes the lemma φ > 1.5, and closes with linear arithmetic.
claim$0 < δw_{0,max}$ where $δw_{0,max} := φ - 3/2$.
background
The BITKernelFamilies module defines three kernels for the cosmic-Z-aging amplitude δw(z) = δw_0 · K(z): the constant kernel, the canonical 1/(1+z) kernel, and the exponential kernel. Each kernel lies in [0,1] for z ≥ 0, and the amplitude δw_0 is taken from the interval [0, J(φ)] supplied by the BIT theorem. The definition sets δw_0,max = φ - 3/2 ≈ 0.118. This result rests on the upstream lemma that φ > 1.5, obtained from √5 > 2 and the closed form of the golden ratio.
proof idea
The proof unfolds the definition of δw_0,max to obtain the expression φ - 3/2. It then applies the lemma establishing φ > 1.5 and finishes with linarith to deduce strict positivity.
why it matters in Recognition Science
The theorem supplies the positivity field required by the BITKernelFamiliesCert structure, the master certificate that packages the kernel properties for downstream forecasting scripts. It thereby anchors the positive range of δw_0 inside the Recognition Science cosmology setting that links the J-uniqueness fixed point to observable w(z) evolution.
scope and limits
- Does not compute the numerical value of δw_0,max beyond the inequality.
- Does not address kernel behavior at nonzero redshift.
- Does not incorporate observational bounds from DESI or other surveys.
Lean usage
delta_w0_max_posformal statement (Lean)
76theorem delta_w0_max_pos : 0 < delta_w0_max := by
proof body
Term-mode proof.
77 unfold delta_w0_max
78 have := phi_gt_onePointFive
79 linarith
80