inv_one_plus_z_pos
plain-language theorem explainer
The 1/(1+z) kernel is strictly positive for every real redshift z exceeding -1. Cosmologists forecasting the BIT cosmic-Z-aging amplitude δw(z) = δw_0 · K(z) would cite this fact to keep the amplitude sign-definite on the physical domain z ≥ 0. The proof is a one-line wrapper that unfolds the kernel definition and invokes positivity of division under the given hypothesis.
Claim. For every real number $z$ satisfying $z > -1$, the kernel function $K(z) = 1/(1+z)$ satisfies $K(z) > 0$.
background
The BIT kernel families module supplies three explicit models for the cosmic-Z-aging amplitude δw(z) = δw_0 · K(z). The second model is the inverse kernel K(z) = 1/(1+z), described as the canonical RS arc-11 kernel and required to lie in [0,1] for z ≥ 0. The kernel function itself is defined by case analysis on the KernelFamily tag, returning exactly 1/(1+z) for the inv_one_plus_z case.
proof idea
The proof is a one-line wrapper. It unfolds the kernel definition to substitute the inv_one_plus_z case, yielding the expression 1/(1+z). Positivity then follows at once from the fact that the numerator 1 is positive and the denominator 1+z is positive whenever -1 < z, via the linarith tactic.
why it matters
This result secures the sign-definiteness of the inverse kernel inside the BIT framework for w(z) forecasting. It directly supports the module claim that each kernel remains bounded in [0,1] on z ≥ 0, with maximum amplitude δw_0 drawn from the BIT theorem. The positivity is a prerequisite for the amplitude to respect the Recognition Composition Law without introducing sign changes on the physical redshift domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.